diff --git a/library/Init/Lean/Elaborator/Basic.lean b/library/Init/Lean/Elaborator/Basic.lean index 2623af501e..e7026aa719 100644 --- a/library/Init/Lean/Elaborator/Basic.lean +++ b/library/Init/Lean/Elaborator/Basic.lean @@ -336,18 +336,7 @@ partial def processCommandsAux : Unit → Frontend Unit def processCommands : Frontend Unit := processCommandsAux () -@[export lean_absolutize_module_name] -def absolutizeModuleName (baseDir : Option String) (m : Name) (k : Option Nat) : IO Name := -match k, baseDir with -| none, _ => pure m -| some k, none => throw (IO.userError ("invalid use of relative import, file name of main file is not available")) -| some k, some baseDir => do - let dir := addRel baseDir k; - let pathSep := toString System.FilePath.pathSeparator; - let oleanFName := dir ++ pathSep ++ modNameToFileName m ++ toString System.FilePath.extSeparator ++ "olean"; - moduleNameOfFileName oleanFName - -def processHeaderAux (baseDir : Option String) (header : Syntax) (trustLevel : UInt32) : IO Environment := +def processHeaderAux (baseMod : Option Name) (header : Syntax) (trustLevel : UInt32) : IO Environment := do let header := header.asNode; let imports := if (header.getArg 0).isNone then [`init.default] else []; let modImports := (header.getArg 1).getArgs; @@ -360,16 +349,16 @@ do let header := header.asNode; let rel := stx.getArg 0; let k := if rel.isNone then none else some (rel.getNumArgs - 1); let id := stx.getIdAt 1; - m ← absolutizeModuleName baseDir id k; + m ← moduleNameOfRelName baseMod id k; pure (m::imports)) imports) imports; let imports := imports.reverse; importModules imports trustLevel -def processHeader (baseDir : Option String) (header : Syntax) (messages : MessageLog) (ctx : Parser.ParserContextCore) (trustLevel : UInt32 := 0) : IO (Environment × MessageLog) := +def processHeader (baseMod : Option Name) (header : Syntax) (messages : MessageLog) (ctx : Parser.ParserContextCore) (trustLevel : UInt32 := 0) : IO (Environment × MessageLog) := catch - (do env ← processHeaderAux baseDir header trustLevel; + (do env ← processHeaderAux baseMod header trustLevel; pure (env, messages)) (fun e => do env ← mkEmptyEnvironment; @@ -386,12 +375,15 @@ match fileName with def testFrontend (input : String) (fileName : Option String := none) : IO (Environment × MessageLog) := do env ← mkEmptyEnvironment; - baseDir ← toBaseDir fileName; + baseMod ← match fileName with + -- TODO: (try to) resolve current working directory to support relative imports with --stdin + | none => pure none + | some f => moduleNameOfFileName f; let fileName := fileName.getD ""; let ctx := Parser.mkParserContextCore env input fileName; match Parser.parseHeader env ctx with | (header, parserState, messages) => do - (env, messages) ← processHeader baseDir header messages ctx; + (env, messages) ← processHeader baseMod header messages ctx; let elabState := { ElabState . env := env, messages := messages }; match (processCommands ctx).run { elabState := elabState, parserState := parserState } with | EStateM.Result.ok _ s => pure (s.elabState.env, s.elabState.messages) diff --git a/library/Init/Lean/Path.lean b/library/Init/Lean/Path.lean index e3a00bf1fb..1f4f021258 100644 --- a/library/Init/Lean/Path.lean +++ b/library/Init/Lean/Path.lean @@ -1,7 +1,14 @@ /- Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura +Authors: Leonardo de Moura, Sebastian Ullrich + +Management of the Lean search path (`LEAN_PATH`), which is a list of +`pkg=path` mappings from package name to root path. An import `A.B.C` +given an `A=path` entry resolves to `path/B/C.olean`. A package-only +import `A` is normalized to `A.Default`. For the input file, we also +need the reverse direction of finding a (unique) module path from a +file path. -/ prelude import Init.System.IO @@ -9,117 +16,132 @@ import Init.System.FilePath import Init.Data.Array import Init.Data.List.Control import Init.Lean.Name +import Init.Data.HashMap +import Init.Data.Nat.Control namespace Lean -open System.FilePath (pathSeparator splitSearchPath extSeparator) +open System.FilePath (pathSeparator extSeparator) private def pathSep : String := toString pathSeparator def realPathNormalized (fname : String) : IO String := do fname ← IO.realPath fname; pure (System.FilePath.normalizePath fname) -def mkSearchPathRef : IO (IO.Ref (Array String)) := -do curr ← realPathNormalized "."; - IO.mkRef #[curr] +abbrev SearchPath := HashMap String String + +def mkSearchPathRef : IO (IO.Ref SearchPath) := +IO.mkRef ∅ @[init mkSearchPathRef] -constant searchPathRef : IO.Ref (Array String) := arbitrary _ +constant searchPathRef : IO.Ref SearchPath := arbitrary _ -def setSearchPath (s : List String) : IO Unit := -do s ← s.mapM realPathNormalized; - searchPathRef.set s.toArray +def parseSearchPath (path : String) (sp : SearchPath := ∅) : IO SearchPath := do + let ps := System.FilePath.splitSearchPath path; + sp ← ps.foldlM (fun (sp : SearchPath) s => match s.splitOn "=" with + | [pkg, path] => pure $ sp.insert pkg path + | _ => throw $ IO.userError $ "ill-formed search path entry '" ++ s ++ "', should be of form 'pkg=path'") + sp; + pure sp -def getBuiltinSearchPath : IO (List String) := +def getBuiltinSearchPath : IO SearchPath := do appDir ← IO.appDir; - let libDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "library"; + let libDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "library" ++ pathSep ++ "Init"; libDirExists ← IO.isDir libDir; if libDirExists then do path ← realPathNormalized libDir; - pure [path] + pure $ HashMap.empty.insert "Init" path else do - let installedLibDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "lib" ++ pathSep ++ "lean" ++ pathSep ++ "library"; + let installedLibDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "lib" ++ pathSep ++ "lean" ++ pathSep ++ "library" ++ pathSep ++ "Init"; installedLibDirExists ← IO.isDir installedLibDir; if installedLibDirExists then do path ← realPathNormalized installedLibDir; - pure [path] + pure $ HashMap.empty.insert "Init" path else - pure [] + pure ∅ -def getSearchPathFromEnv : IO (List String) := +def addSearchPathFromEnv (sp : SearchPath) : IO SearchPath := do val ← IO.getEnv "LEAN_PATH"; match val with - | none => pure ["."] -- If LEAN_PATH is not defined, use current directory - | some val => pure (splitSearchPath val) + | none => pure sp + | some val => parseSearchPath val sp @[export lean_init_search_path] def initSearchPath (path : Option String := "") : IO Unit := match path with -| some path => setSearchPath (splitSearchPath path) +| some path => parseSearchPath path >>= searchPathRef.set | none => do - pathEnv ← getSearchPathFromEnv; - builtinPath ← getBuiltinSearchPath; - setSearchPath (pathEnv ++ builtinPath) + sp ← getBuiltinSearchPath; + sp ← addSearchPathFromEnv sp; + searchPathRef.set sp -def findFile (fname : String) (ext : String) : IO (Option String) := -let checkFile (curr : String) : IO (Option String) := do { - ex ← IO.fileExists curr; - if ex then pure (some curr) else pure none -}; -do let fname := System.FilePath.normalizePath fname; - paths ← searchPathRef.get; - paths.findM $ fun path => do - let curr := path ++ pathSep ++ fname; - result ← checkFile (curr ++ toString extSeparator ++ ext); - match result with - | none => checkFile (curr ++ pathSep ++ "Default" ++ toString extSeparator ++ ext) - | other => pure other - -def modNameToFileName : Name → String +def modPathToFilePath : Name → String | Name.str Name.anonymous h _ => h -| Name.str p h _ => modNameToFileName p ++ pathSep ++ h +| Name.str p h _ => modPathToFilePath p ++ pathSep ++ h | Name.anonymous => "" -| Name.num p _ _ => modNameToFileName p +| Name.num p _ _ => panic! "ill-formed import" -def addRel (baseDir : String) : Nat → String -| 0 => baseDir -| n+1 => addRel n ++ pathSep ++ ".." +/- Given `A.B.C, return ("A", `B.C). -/ +def splitAtRoot : Name → String × Name +| Name.str Name.anonymous s _ => (s, Name.anonymous) +| Name.str n s _ => + let (pkg, path) := splitAtRoot n; + (pkg, mkNameStr path s) +| _ => panic! "ill-formed import" -def findLeanFile (modName : Name) (ext : String) : IO String := -do let fname := modNameToFileName modName; - some fname ← findFile fname ext | throw (IO.userError ("module '" ++ toString modName ++ "' not found")); - realPathNormalized fname +@[export lean_find_olean] +def findOLean (mod : Name) : IO String := +do sp ← searchPathRef.get; + let (pkg, path) := splitAtRoot mod; + some root ← pure $ sp.find pkg + | throw $ IO.userError $ "unknown package '" ++ pkg ++ "'"; + let fname := root ++ pathSep ++ modPathToFilePath path ++ ".olean"; + pure fname -def findOLean (modName : Name) : IO String := -findLeanFile modName "olean" - -@[export lean_find_lean] -def findLean (modName : Name) : IO String := -findLeanFile modName "lean" - -def findAtSearchPath (fname : String) : IO String := +def findAtSearchPath (fname : String) : IO (Option (String × String)) := do fname ← realPathNormalized fname; - paths ← searchPathRef.get; - match paths.find? (fun path => if path.isPrefixOf fname then some path else none) with - | some r => pure r - | none => throw (IO.userError ("file '" ++ fname ++ "' not in the search path " ++ repr paths)) + sp ← searchPathRef.get; + results ← sp.foldM (fun results pkg path => do + path ← realPathNormalized path; + pure $ if String.isPrefixOf path fname then (pkg, path) :: results else results) []; + match results with + | [res] => pure res + | [] => pure none + | _ => throw (IO.userError ("file '" ++ fname ++ "' is contained in multiple packages: " ++ ", ".intercalate (results.map Prod.fst))) @[export lean_module_name_of_file] -def moduleNameOfFileName (fname : String) : IO Name := -do path ← findAtSearchPath fname; +def moduleNameOfFileName (fname : String) : IO (Option Name) := +do some (pkg, path) ← findAtSearchPath fname + | pure none; fname ← realPathNormalized fname; let fnameSuffix := fname.drop path.length; let fnameSuffix := if fnameSuffix.get 0 == pathSeparator then fnameSuffix.drop 1 else fnameSuffix; - if path ++ pathSep ++ fnameSuffix != fname then - throw (IO.userError ("failed to convert file '" ++ fname ++ "' to module name, path is not a prefix of the given file")) - else do - some extPos ← pure (fnameSuffix.revPosOf '.') - | throw (IO.userError ("failed to convert file '" ++ fname ++ "' to module name, extension is missing")); - let modNameStr := fnameSuffix.extract 0 extPos; - let extStr := fnameSuffix.extract (extPos + 1) fnameSuffix.bsize; - let parts := modNameStr.splitOn pathSep; - let modName := parts.foldl mkNameStr Name.anonymous; - fname' ← findLeanFile modName extStr; - unless (fname == fname') $ throw (IO.userError ("failed to convert file '" ++ fname ++ "' to module name, module name '" ++ toString modName ++ "' resolves to '" ++ fname' ++ "'")); - pure modName + some extPos ← pure (fnameSuffix.revPosOf '.') + | throw (IO.userError ("failed to convert file '" ++ fname ++ "' to module name, extension is missing")); + let modNameStr := fnameSuffix.extract 0 extPos; + let extStr := fnameSuffix.extract (extPos + 1) fnameSuffix.bsize; + let parts := modNameStr.splitOn pathSep; + let modName := parts.foldl mkNameStr pkg; + pure modName + +/-- Absolutize and normalize parsed import. -/ +@[export lean_module_name_of_rel_name] +def moduleNameOfRelName (baseMod : Option Name) (m : Name) (k : Option Nat) : IO Name := do + m ← match k, baseMod with + | none, _ => pure m + | some k, none => throw (IO.userError ("invalid use of relative import, module name of main file is not available")) + | some k, some baseMod => do { + -- split out package name so that we cannot leave package + let (pkg, path) := splitAtRoot baseMod; + -- +1 to go from main file module to surrounding directory + path ← (k + 1).foldM (fun _ path => match path with + | Name.str path _ _ => pure path + | Name.anonymous => throw $ IO.userError $ "invalid relative import, would leave package" + | Name.num _ _ _ => unreachable!) path; + pure $ pkg ++ path + }; + -- normalize `A` to `A.Default` + match m with + | Name.str Name.anonymous pkg _ => pure $ mkNameSimple pkg ++ "Default" + | _ => pure m end Lean diff --git a/src/library/module.cpp b/src/library/module.cpp index 2c7e540d62..fa2855f48e 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -19,7 +19,6 @@ Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich #include "runtime/io.h" #include "runtime/compact.h" #include "util/io.h" -#include "util/lean_path.h" #include "util/buffer.h" #include "util/name_map.h" #include "util/file_lock.h" diff --git a/src/library/module.h b/src/library/module.h index 4b42f51a2a..97a9059e13 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -13,9 +13,17 @@ Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich #include "runtime/optional.h" #include "library/io_state.h" #include "kernel/environment.h" -#include "util/lean_path.h" namespace lean { +using module_name = name; +struct rel_module_name { + optional m_updirs; + module_name m_name; + + rel_module_name(unsigned int const & updirs, module_name const & name) : m_updirs(some(updirs)), m_name(name) {} + explicit rel_module_name(module_name const & name) : m_name(name) {} +}; + /** \brief Return an environment where all modules in \c modules are imported. Modules included directly or indirectly by them are also imported. diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index f85ad093ba..1ead7d97d8 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -43,7 +43,7 @@ if(NOT STAGE0) set(NODE_JS "node --stack_size=8192") file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/lean_with_path - "#!/bin/sh\nLEAN_PATH=${CMAKE_CURRENT_SOURCE_DIR}/../../library ${NODE_JS} ${CMAKE_CURRENT_BINARY_DIR}/lean.js \"$@\"\n") + "#!/bin/sh\nLEAN_PATH=Init=${CMAKE_CURRENT_SOURCE_DIR}/../../library ${NODE_JS} ${CMAKE_CURRENT_BINARY_DIR}/lean.js \"$@\"\n") execute_process(COMMAND chmod +x ${CMAKE_CURRENT_BINARY_DIR}/lean_with_path) ADD_CUSTOM_TARGET(bin_lean ALL diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index ba33306e55..42b273cc9f 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -22,7 +22,6 @@ Author: Leonardo de Moura #include "util/timer.h" #include "util/macros.h" #include "util/io.h" -#include "util/lean_path.h" #include "util/file_lock.h" #include "util/options.h" #include "util/option_declarations.h" @@ -44,6 +43,7 @@ Author: Leonardo de Moura #include "init/init.h" #include "frontends/lean/simple_pos_info_provider.h" #include "library/compiler/ir_interpreter.h" +#include "util/path.h" #ifdef _MSC_VER #include #define STDOUT_FILENO 1 @@ -346,17 +346,32 @@ void init_search_path() { get_io_scalar_result(lean_init_search_path(mk_option_none(), io_mk_world())); } -extern "C" object* lean_find_lean(object* mod_name, object* w); +extern "C" object* lean_find_olean(object* mod_name, object* w); -std::string find_lean_file(name mod_name) { - string_ref fname = get_io_result(lean_find_lean(mod_name.to_obj_arg(), io_mk_world())); +std::string find_olean_file(name mod_name) { + string_ref fname = get_io_result(lean_find_olean(mod_name.to_obj_arg(), io_mk_world())); return fname.to_std_string(); } extern "C" object* lean_module_name_of_file(object* fname, object* w); -name module_name_of_file2(std::string const & fname) { - return get_io_result(lean_module_name_of_file(mk_string(fname), io_mk_world())); +optional module_name_of_file(std::string const & fname) { + return get_io_result>(lean_module_name_of_file(mk_string(fname), io_mk_world())).get(); +} + +extern "C" object* lean_module_name_of_rel_name(object* base_mod, object* m , object* k, object* w); + +name module_name_of_rel_name(optional const & base_mod, name m, optional const & k) { + object * k2 = k ? mk_option_some(box(*k)) : mk_option_none(); + return get_io_result(lean_module_name_of_rel_name(option_ref(base_mod).to_obj_arg(), m.to_obj_arg(), k2, io_mk_world())); +} + +std::string olean_of_lean(std::string const & lean_fn) { + if (lean_fn.size() > 5 && lean_fn.substr(lean_fn.size() - 5) == ".lean") { + return lean_fn.substr(0, lean_fn.size() - 5) + ".olean"; + } else { + throw exception(sstream() << "not a .lean file: " << lean_fn); + } } } @@ -408,8 +423,6 @@ int main(int argc, char ** argv) { init_search_path(); - search_path path = get_lean_path_from_env().value_or(get_builtin_search_path()); - options opts; optional server_in; std::string native_output; @@ -528,7 +541,7 @@ int main(int argc, char ** argv) { scope_global_ios scope_ios(ios); type_context_old trace_ctx(env, opts); scope_trace_env scope_trace(env, opts, trace_ctx); - name main_module_name; + optional main_module_name; std::string mod_fn = ""; std::string contents; @@ -542,7 +555,8 @@ int main(int argc, char ** argv) { std::stringstream buf; buf << std::cin.rdbuf(); contents = buf.str(); - main_module_name = name("_stdin"); + // if we are inside a package, we still want a correct module path to resolve relative imports + main_module_name = module_name_of_file("./stdin.lean"); } else { if (!run && argc - optind != 1) { std::cerr << "Expected exactly one file name\n"; @@ -551,7 +565,7 @@ int main(int argc, char ** argv) { } mod_fn = lrealpath(argv[optind++]); contents = read_file(mod_fn); - main_module_name = module_name_of_file2(mod_fn); + main_module_name = module_name_of_file(mod_fn); } try { @@ -572,17 +586,12 @@ int main(int argc, char ** argv) { p.parse_imports(rel_imports); std::vector imports; - auto dir = dirname(mod_fn); for (auto const & rel : rel_imports) - imports.push_back(absolutize_module_name(path, dir, rel)); + imports.push_back(module_name_of_rel_name(main_module_name, rel.m_name, rel.m_updirs)); if (only_deps) { for (auto const & import : imports) { - std::string m_name = find_lean_file(import); - auto last_idx = m_name.find_last_of("."); - std::string rawname = m_name.substr(0, last_idx); - std::string ext = m_name.substr(last_idx); - m_name = rawname + ".olean"; + std::string m_name = find_olean_file(import); std::cout << m_name << "\n"; } return 0; @@ -594,7 +603,11 @@ int main(int argc, char ** argv) { } else { env = import_modules(trust_lvl, imports); } - env.set_main_module(main_module_name); + if (main_module_name) { + env.set_main_module(*main_module_name); + } else { + env.set_main_module("_stdin"); + } p.set_env(env); p.parse_commands(); } catch (lean::throwable & ex) { @@ -634,13 +647,16 @@ int main(int argc, char ** argv) { display_cumulative_profiling_times(std::cerr); if (c_output && ok) { + if (!main_module_name) { + std::cerr << "cannot extract code, module name of input file is not known\n"; + return 1; + } std::ofstream out(*c_output); if (out.fail()) { std::cerr << "failed to create '" << *c_output << "'\n"; return 1; } - auto mod = module_name_of_file2(mod_fn); - out << lean::ir::emit_c(env, mod).data(); + out << lean::ir::emit_c(env, *main_module_name).data(); out.close(); } diff --git a/src/shell/test_standard.sh b/src/shell/test_standard.sh deleted file mode 100755 index 45b6708469..0000000000 --- a/src/shell/test_standard.sh +++ /dev/null @@ -1,5 +0,0 @@ -#!/bin/bash -LEAN=$1 -FILE=$2 -export LEAN_PATH=.:../../library/standard -$LEAN $2 diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 77936a42ba..5d833d4b29 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -1,6 +1,6 @@ add_library(util OBJECT object_ref.cpp name.cpp name_set.cpp fresh_name.cpp escaped.cpp bit_tricks.cpp ascii.cpp - path.cpp lean_path.cpp lbool.cpp bitap_fuzzy_search.cpp + path.cpp lbool.cpp bitap_fuzzy_search.cpp init_module.cpp list_fn.cpp file_lock.cpp timeit.cpp timer.cpp parser_exception.cpp name_generator.cpp kvmap.cpp map_foreach.cpp options.cpp format.cpp option_declarations.cpp) diff --git a/src/util/lean_path.cpp b/src/util/lean_path.cpp deleted file mode 100644 index 1e67ddf4ef..0000000000 --- a/src/util/lean_path.cpp +++ /dev/null @@ -1,193 +0,0 @@ -/* -Copyright (c) 2017 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura, Gabriel Ebner -*/ -#include "util/lean_path.h" -#include -#include -#include -#include -#include "runtime/sstream.h" - -#ifndef LEAN_DEFAULT_MODULE_FILE_NAME -#define LEAN_DEFAULT_MODULE_FILE_NAME "Default" -#endif - -namespace lean { -lean_file_not_found_exception::lean_file_not_found_exception(std::string const & fname): - exception(sstream() << "file '" << fname << "' not found in the LEAN_PATH"), - m_fname(fname) {} - -static char const * g_default_file_name = LEAN_DEFAULT_MODULE_FILE_NAME; - -static bool exists(std::string const & fn) { - return !!std::ifstream(fn); -} - -optional get_lean_path_from_env() { - if (auto r = getenv("LEAN_PATH")) { - auto lean_path = normalize_path(r); - unsigned i = 0; - unsigned j = 0; - unsigned sz = static_cast(lean_path.size()); - search_path path; - for (; j < sz; j++) { - if (is_path_sep(lean_path[j])) { - if (j > i) - path.push_back(lrealpath(lean_path.substr(i, j - i))); - i = j + 1; - } - } - if (j > i) - path.push_back(lrealpath(lean_path.substr(i, j - i))); - return optional(path); - } else { - return optional(); - } -} - -search_path get_builtin_search_path() { - search_path path; -#if !defined(LEAN_EMSCRIPTEN) - std::string exe_path = dirname(get_exe_location()); - auto lib_path = exe_path + get_dir_sep() + ".." + get_dir_sep() + "library"; - if (exists(lib_path)) - path.push_back(lrealpath(lib_path)); - auto installed_lib_path = exe_path + get_dir_sep() + ".." + get_dir_sep() + "lib" + get_dir_sep() + "lean" + get_dir_sep() + "library"; - if (exists(installed_lib_path)) - path.push_back(lrealpath(installed_lib_path)); -#endif - return path; -} - -bool is_lean_file(std::string const & fname) { - return has_file_ext(fname, ".lean"); -} - -bool is_olean_file(std::string const & fname) { - return has_file_ext(fname, ".olean"); -} - -bool is_known_file_ext(std::string const & fname) { - return is_lean_file(fname) || is_olean_file(fname); -} - -optional check_file_core(std::string file, char const * ext) { - if (ext) - file += ext; - std::ifstream ifile(file); - if (ifile) - return optional(lrealpath(file)); - else - return optional(); -} - -optional check_file(std::string const & path, std::string const & fname, char const * ext = nullptr) { - std::string file = path + get_dir_sep() + fname; - if (is_directory(file.c_str())) { - std::string default_file = file + get_dir_sep() + g_default_file_name; - if (auto r1 = check_file_core(default_file, ext)) { - if (auto r2 = check_file_core(file, ext)) - throw exception(sstream() << "ambiguous import, it can be '" << *r1 << "' or '" << *r2 << "'"); - return r1; - } - } - return check_file_core(file, ext); -} - -static std::string find_file(search_path const & paths, std::string fname, std::initializer_list const & extensions) { - bool is_known = is_known_file_ext(fname); - fname = normalize_path(fname); - buffer results; - for (auto & path : paths) { - if (is_known) { - if (auto r = check_file(path, fname)) - results.push_back(*r); - } else { - for (auto ext : extensions) { - if (auto r = check_file(path, fname, ext)) - results.push_back(*r); - } - } - } - if (results.size() == 0) - throw lean_file_not_found_exception(fname); - else if (results.size() > 1) - throw exception(sstream() << "ambiguous import, it can be '" << results[0] << "' or '" << results[1] << "'"); - else - return results[0]; -} - -std::string find_file(search_path const & paths, std::string const & base, optional const & rel, name const & fname, - std::initializer_list const & extensions) { - if (!rel) { - return find_file(paths, fname.to_string(get_dir_sep()), extensions); - } else { - auto path = base; - for (unsigned i = 0; i < *rel; i++) { - path += get_dir_sep(); - path += ".."; - } - for (auto ext : extensions) { - if (auto r = check_file(path, fname.to_string(get_dir_sep()), ext)) - return *r; - } - throw lean_file_not_found_exception(fname.to_string()); - } -} - -std::string find_file(search_path const & paths, - std::string const & base, optional const & k, name const & fname, char const * ext) { - return find_file(paths, base, k, fname, {ext}); -} - -std::string find_file(search_path const & paths, std::string fname) { - return find_file(paths, fname, {".olean", ".lean"}); -} - -std::string find_file(search_path const & paths, name const & fname) { - return find_file(paths, fname.to_string(get_dir_sep())); -} - -std::string find_file(search_path const & paths, name const & fname, std::initializer_list const & exts) { - return find_file(paths, fname.to_string(get_dir_sep()), exts); -} - -name module_name_of_file(search_path const & paths, std::string const & fname0) { - auto fname = normalize_path(fname0); - lean_assert(is_lean_file(fname)); - fname = fname.substr(0, fname.size() - std::string(".lean").size()); - for (auto & path : paths) { - if (path.size() < fname.size() && fname.substr(0, path.size()) == path) { - size_t pos = path.size(); - if (fname[pos] == get_dir_sep_ch()) - pos++; - name n; - while (pos < fname.size()) { - auto sep_pos = fname.find(get_dir_sep_ch(), pos); - n = name(n, fname.substr(pos, sep_pos - pos).c_str()); - pos = sep_pos; - if (pos != std::string::npos) - pos++; - } - return n; - } - } - throw exception(sstream() << "file '" << fname0 << "' is not part of any known Lean packages"); -} - -module_name absolutize_module_name(search_path const & path, std::string const & base, rel_module_name const & rel) { - // TODO(Sebastian): Should make sure that the result of `find_file` is still in the same package as `base` - return module_name_of_file(path, find_file(path, base, rel.m_updirs, rel.m_name, ".lean")); -} - -std::string olean_of_lean(std::string const & lean_fn) { - if (lean_fn.size() > 5 && lean_fn.substr(lean_fn.size() - 5) == ".lean") { - return lean_fn.substr(0, lean_fn.size() - 5) + ".olean"; - } else { - throw exception(sstream() << "not a .lean file: " << lean_fn); - } -} -} diff --git a/src/util/lean_path.h b/src/util/lean_path.h deleted file mode 100644 index 38806efbb5..0000000000 --- a/src/util/lean_path.h +++ /dev/null @@ -1,64 +0,0 @@ -/* -Copyright (c) 2017 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura, Gabriel Ebner -*/ -#pragma once -#include -#include -#include "runtime/exception.h" -#include "util/name.h" -#include "util/path.h" - -namespace lean { -class lean_file_not_found_exception : public exception { - std::string m_fname; -public: - lean_file_not_found_exception(std::string const & fname); -}; - -using search_path = std::vector; - -optional get_lean_path_from_env(); -search_path get_builtin_search_path(); - -#if !defined(LEAN_EMSCRIPTEN) -std::string get_exe_location(); -#endif - -/** \brief A module name is an absolute import path like 'init.lean.core'. We do not use actual absolute file paths - * because we store module names in .olean files, which should not be completely system-specific. - */ -using module_name = name; - -struct rel_module_name { - optional m_updirs; - module_name m_name; - - rel_module_name(unsigned int const & updirs, module_name const & name) : m_updirs(some(updirs)), m_name(name) {} - explicit rel_module_name(module_name const & name) : m_name(name) {} -}; - -/** \brief Hierarchical names are converted into paths using the path separator. Example: foo.bar is converted into 'foo/bar.lean' */ -std::string find_file(search_path const &, module_name const & mod_name); -std::string find_file(search_path const &, module_name const & mod_name, std::initializer_list const & exts); - -/** \brief \brief Similar to previous find_file, but if k is not none then search at the k-th parent of base. */ -std::string find_file(search_path const &, std::string const & base, optional const & rel, module_name const & mod_name, - std::initializer_list const & extensions); -std::string find_file(search_path const &, std::string const & base, optional const & k, module_name const & mod_name, char const * ext); - -/** \brief Inverse function of \c find_file */ -module_name module_name_of_file(search_path const &, std::string const & fname); - -/** \brief Resolve path like '.instances' in 'library/init/data/list' to 'init.data.list.instances' */ -module_name absolutize_module_name(search_path const &, std::string const & base, rel_module_name const & rel); - -/** \brief Return true iff fname ends with ".lean" */ -bool is_lean_file(std::string const & fname); -/** \brief Return true iff fname ends with ".olean" */ -bool is_olean_file(std::string const & fname); - -std::string olean_of_lean(std::string const & lean_fn); -} diff --git a/tests/bench/compile.sh b/tests/bench/compile.sh index 20edbeb804..e8080811f7 100755 --- a/tests/bench/compile.sh +++ b/tests/bench/compile.sh @@ -6,7 +6,7 @@ fi ulimit -s 8192 BIN_DIR=../../bin LEAN=$BIN_DIR/lean -export LEAN_PATH=../../library:. +export LEAN_PATH=Init=../../library/Init:Test=. ff=$1 if [[ "$OSTYPE" == "msys" ]]; then diff --git a/tests/compiler/test_single.sh b/tests/compiler/test_single.sh index 68091b9fcf..92978f5f6a 100755 --- a/tests/compiler/test_single.sh +++ b/tests/compiler/test_single.sh @@ -6,7 +6,7 @@ fi ulimit -s 8192 LEAN=$1 BIN_DIR=../../bin -export LEAN_PATH=../../library:. +export LEAN_PATH=Init=../../library/Init:Test=. if [ $# -ne 3 ]; then INTERACTIVE=no else diff --git a/tests/compiler/test_single_interpret.sh b/tests/compiler/test_single_interpret.sh index c867b875f3..1a6a83f1a7 100755 --- a/tests/compiler/test_single_interpret.sh +++ b/tests/compiler/test_single_interpret.sh @@ -6,7 +6,7 @@ fi ulimit -s 8192 LEAN=$1 BIN_DIR=../../bin -export LEAN_PATH=../../library:. +export LEAN_PATH=Init=../../library/Init:Test=. if [ $# -ne 3 ]; then INTERACTIVE=no else diff --git a/tests/lean/ctor_layout.lean b/tests/lean/ctor_layout.lean index 3de301dc9c..2fcb1b2008 100644 --- a/tests/lean/ctor_layout.lean +++ b/tests/lean/ctor_layout.lean @@ -3,7 +3,7 @@ open Lean open Lean.IR def tst : IO Unit := -do initSearchPath "../../library:."; +do initSearchPath "Init=../../library/Init"; env ← importModules [`Init.Lean.Compiler.IR.Basic]; ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.IR.Expr.reuse; ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo); diff --git a/tests/lean/fail/test_single.sh b/tests/lean/fail/test_single.sh index 484dc1e948..4ebd0ce30f 100644 --- a/tests/lean/fail/test_single.sh +++ b/tests/lean/fail/test_single.sh @@ -5,7 +5,7 @@ if [ $# -ne 2 ]; then fi ulimit -s 8192 LEAN=$1 -export LEAN_PATH=../../../library:. +export LEAN_PATH=Init=../../../library/Init:Test=. f=$2 echo "-- testing $f" "$LEAN" -j 0 "$f" diff --git a/tests/lean/run/test_single.sh b/tests/lean/run/test_single.sh index fff42176ae..7c4ddc4209 100755 --- a/tests/lean/run/test_single.sh +++ b/tests/lean/run/test_single.sh @@ -5,7 +5,7 @@ if [ $# -ne 2 ]; then fi ulimit -s 8192 LEAN=$1 -export LEAN_PATH=../../../library:. +export LEAN_PATH=Init=../../../library/Init:Test=. f=$2 echo "-- testing $f" "$LEAN" -j 0 "$f" diff --git a/tests/lean/test.sh b/tests/lean/test.sh index fa0988c814..253e4f2212 100755 --- a/tests/lean/test.sh +++ b/tests/lean/test.sh @@ -6,7 +6,7 @@ if [ $# -ne 2 -a $# -ne 1 ]; then fi ulimit -s 8192 LEAN=$1 -export LEAN_PATH=../../library:. +export LEAN_PATH=Init=../../library/Init:Test=. if [ $# -ne 2 ]; then INTERACTIVE=no else diff --git a/tests/lean/test_single.sh b/tests/lean/test_single.sh index 61ecad6b7d..e8a36ee7be 100755 --- a/tests/lean/test_single.sh +++ b/tests/lean/test_single.sh @@ -5,7 +5,7 @@ if [ $# -ne 3 -a $# -ne 2 ]; then fi ulimit -s 8192 LEAN=$1 -export LEAN_PATH=../../library:. +export LEAN_PATH=Init=../../library/Init:Test=. if [ $# -ne 3 ]; then INTERACTIVE=no else diff --git a/tests/lean/trust0/test_single.sh b/tests/lean/trust0/test_single.sh index c166aafdce..bb6c511258 100755 --- a/tests/lean/trust0/test_single.sh +++ b/tests/lean/trust0/test_single.sh @@ -5,7 +5,7 @@ if [ $# -lt 2 ]; then fi ulimit -s 8192 LEAN=$1 -export LEAN_PATH=../../../library:. +export LEAN_PATH=Init=../../../library/Init:Test=. f=$2 shift 2 echo "-- testing $f" diff --git a/tests/playground/compile.sh b/tests/playground/compile.sh index 2e43ba1f33..eae0ae29ee 100755 --- a/tests/playground/compile.sh +++ b/tests/playground/compile.sh @@ -6,7 +6,7 @@ fi ulimit -s 8192 BIN_DIR=../../bin LEAN=$BIN_DIR/lean -export LEAN_PATH=../../library:. +export LEAN_PATH=Init=../../library/Init:Test=. ff=$1 if [[ "$OSTYPE" == "msys" ]]; then diff --git a/tests/playground/oldcompile.sh b/tests/playground/oldcompile.sh index cfa20cda35..0f2431195c 100755 --- a/tests/playground/oldcompile.sh +++ b/tests/playground/oldcompile.sh @@ -6,7 +6,7 @@ fi ulimit -s 8192 BIN_DIR=../../bin LEAN=$BIN_DIR/lean -export LEAN_PATH=../../library:. +export LEAN_PATH=Init=../../library/Init:Test=. ff=$1 if [[ "$OSTYPE" == "msys" ]]; then diff --git a/tests/plugin/test_single.sh b/tests/plugin/test_single.sh index e4316057a8..d940040175 100755 --- a/tests/plugin/test_single.sh +++ b/tests/plugin/test_single.sh @@ -5,7 +5,7 @@ if [ $# -ne 2 -a $# -ne 1 ]; then fi ulimit -s 8192 BIN_DIR=../../bin -export LEAN_PATH=../../library:. +export LEAN_PATH=Init=../../library/Init:Test=. if [ $# -ne 2 ]; then INTERACTIVE=no else