From bf5afbc289f038ba7f773fc98ec09ee67018aeb2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 26 Jul 2019 17:55:00 -0700
Subject: [PATCH] feat(library/init/lean/environment): use `findOLean`
 implemented in Lean

TODO: cleanup `path.lean`
---
 library/init/lean/environment.lean |  6 ++----
 library/init/lean/path.lean        | 11 ++++++-----
 2 files changed, 8 insertions(+), 9 deletions(-)

diff --git a/library/init/lean/environment.lean b/library/init/lean/environment.lean
index 02ba1aff8b..cc20e4f95f 100644
--- a/library/init/lean/environment.lean
+++ b/library/init/lean/environment.lean
@@ -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;
diff --git a/library/init/lean/path.lean b/library/init/lean/path.lean
index 7becc92578..bb5427d6f1 100644
--- a/library/init/lean/path.lean
+++ b/library/init/lean/path.lean
@@ -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