From 5a1380ec6aac12609864eaeb5ab58fed46b856da Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 25 Jul 2019 19:28:22 -0700
Subject: [PATCH] feat(library/init/lean): add lean/path.lean

---
 library/init/lean/default.lean          |  1 +
 library/init/lean/elaborator/basic.lean |  4 +-
 library/init/lean/path.lean             | 68 +++++++++++++++++++++++++
 3 files changed, 71 insertions(+), 2 deletions(-)
 create mode 100644 library/init/lean/path.lean

diff --git a/library/init/lean/default.lean b/library/init/lean/default.lean
index 68f4b74127..8d2a7c4935 100644
--- a/library/init/lean/default.lean
+++ b/library/init/lean/default.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import init.lean.path
 import init.lean.compiler
 import init.lean.environment
 import init.lean.modifiers
diff --git a/library/init/lean/elaborator/basic.lean b/library/init/lean/elaborator/basic.lean
index eb5cff7574..c20a39ee3d 100644
--- a/library/init/lean/elaborator/basic.lean
+++ b/library/init/lean/elaborator/basic.lean
@@ -343,10 +343,10 @@ catch
 
 /- TODO: support for non-standard search path for web interface -/
 @[extern 1 "lean_set_search_path"]
-constant setSearchPath : IO Unit := default _
+constant setSearchPathOld : IO Unit := default _
 
 def testFrontend (input : String) (fileName : Option String := none) : IO (Environment × MessageLog) :=
-do setSearchPath;
+do setSearchPathOld;
    env ← mkEmptyEnvironment;
    let fileName := fileName.getOrElse "<input>";
    let ctx := Parser.mkParserContextCore env input fileName;
diff --git a/library/init/lean/path.lean b/library/init/lean/path.lean
new file mode 100644
index 0000000000..ac3bcdbab2
--- /dev/null
+++ b/library/init/lean/path.lean
@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.system.io
+import init.system.filepath
+import init.data.array
+
+namespace Lean
+open System.FilePath (pathSeparator searchPathSeparator)
+private def pathSep : String := toString pathSeparator
+private def searchPathSep : String := toString searchPathSeparator
+
+def mkSearchPathRef : IO (IO.Ref (Array String)) :=
+do curr ← IO.realPath ".";
+   IO.mkRef (Array.singleton curr)
+
+@[init mkSearchPathRef]
+constant searchPathRef : IO.Ref (Array String) := default _
+
+def setSearchPath (s : String) : IO Unit :=
+searchPathRef.set (s.split searchPathSep).toArray
+
+def getBuiltinSearchPath : IO String :=
+do appDir ← IO.appDir;
+   let libDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "library";
+   IO.println libDir;
+   libDirExists ← IO.isDir libDir;
+   if libDirExists then
+     IO.realPath libDir
+   else do
+     let installedLibDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "lib" ++ pathSep ++ "lean" ++ pathSep ++ "library";
+     installedLibDirExists ← IO.isDir installedLibDir;
+     IO.println installedLibDir;
+     if installedLibDirExists then do
+       IO.realPath installedLibDir
+     else
+       throw (IO.userError "failed to locate builtin search path, please set LEAN_PATH")
+
+def getSearchPathFromEnv : IO (Option (List String)) :=
+do val ← IO.getEnv "LEAN_PATH";
+   match val with
+   | none     => pure none
+   | some val =>
+     pure $ val.split searchPathSep
+
+def initSearchPath (path : Option String := "") : IO Unit :=
+match path with
+| some path => setSearchPath path
+| none      => do
+  path ← getSearchPathFromEnv;
+  match path with
+  | some path => searchPathRef.set path.toArray
+  | none => do
+    path ← getBuiltinSearchPath;
+    curr ← IO.realPath ".";
+    searchPathRef.set [path, curr].toArray
+
+def findFile (fname : String) : IO (Option String) :=
+do paths ← searchPathRef.get;
+   paths.mfind $ fun path => do
+     let curr := path ++ pathSep ++ fname;
+     ex ← IO.fileExists curr;
+     if ex then pure (some curr) else pure none
+
+end Lean