max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/lean/environment): use findOLean implemented in Lean

Browse source 
TODO: cleanup `path.lean`
This commit is contained in:
Leonardo de Moura 2019-07-26 17:55:00 -07:00
parent 8a27a5e164
commit bf5afbc289
2 changed files with 8 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/lean/environment.lean
View file

@ -9,6 +9,7 @@ import init.util
import init.data.bytearray
import init.lean.declaration
import init.lean.smap
import init.lean.path
namespace Lean
/- Opaque environment extension state. It is essentially the Lean version of a C `void *`
@ -409,9 +410,6 @@ serialized := bytes
def writeModule (env : Environment) (fname : String) : IO Unit :=
do modData ← mkModuleData env; saveModuleData fname modData
@[extern 2 "lean_find_olean"]
constant findOLeanOld (modName : Name) : IO String := default _
partial def importModulesAux : List Name → (NameSet × Array ModuleData) → IO (NameSet × Array ModuleData)
| [] r := pure r
| (m::ms) (s, mods) :=
@ -419,7 +417,7 @@ partial def importModulesAux : List Name → (NameSet × Array ModuleData) → I
importModulesAux ms (s, mods)
else do
let s := s.insert m;
mFile ← findOLeanOld m;
mFile ← findOLean m;
mod ← readModuleData mFile;
(s, mods) ← importModulesAux mod.imports.toList (s, mods);
let mods := mods.push mod;

11
library/init/lean/path.lean
View file

@ -68,7 +68,6 @@ do paths ← searchPathRef.get;
paths.mfind $ fun path => do
let path := path ++ pathSep;
let curr := path ++ fname;
IO.println ("trying " ++ curr);
ex ← IO.fileExists curr;
if ex then pure (some (path, curr)) else pure none
@ -97,12 +96,13 @@ match rel with
fname ← IO.realPath fname;
pure (path, fname)
def findOLean (rel : Option Nat) (modName : Name) : IO (String × String) :=
findLeanFile rel modName "olean"
def findOLean (modName : Name) : IO String :=
Prod.snd <$> findLeanFile none modName "olean"
def findLean (rel : Option Nat) (modName : Name) : IO (String × String) :=
findLeanFile rel modName "lean"
def findLean (rel : Option Nat) (modName : Name) : IO String :=
Prod.snd <$> findLeanFile rel modName "lean"
/-
def absolutizeModuleName (rel : Option Nat) (modName : Name) : IO Name :=
match rel with
| none => pure modName
@ -112,5 +112,6 @@ match rel with
let fname := fname.take (fname.length - "olean".length - 1 /- path separator -/);
let comps := fname.split pathSep;
pure $ comps.foldl Name.mkString Name.anonymous
-/
end Lean