Update to Lean nightly 06-13

Lake/Build.lean

@@ -93,8 +93,8 @@ partial def buildModule (mod : Name) : BuildM BuildResult := do
       throw e
     try
       let cFile := modToFilePath tempBuildPath mod "c"
-      IO.createDirAll oleanFile.parent.get!
-      IO.createDirAll cFile.parent.get!
+      IO.FS.createDirAll oleanFile.parent.get!
+      IO.FS.createDirAll cFile.parent.get!
       execCmd {
         cmd := "lean"
         args := ctx.leanArgs.toArray ++ #["-o", oleanFile.toString, "-c", cFile.toString, leanFile.toString]

Lake/Make.lean

@@ -17,21 +17,21 @@ partial def withLockFile (x : IO α) : IO α := do
   try
     x
   finally
-    IO.removeFile lockfile
+    IO.FS.removeFile lockfile
   where
     acquire (firstTime := true) := do
-      IO.createDirAll lockfile.parent.get!
+      IO.FS.createDirAll lockfile.parent.get!
       try
         -- TODO: lock file should ideally contain PID
         if !Platform.isWindows then
-          discard <| IO.Prim.Handle.mk lockfile "wx"
+          discard <| IO.FS.Handle.mkPrim lockfile "wx"
         else
           -- `x` mode doesn't seem to work on Windows even though it's listed at
           -- https://docs.microsoft.com/en-us/cpp/c-runtime-library/reference/fopen-wfopen?view=msvc-160
           -- ...? Let's use the slightly racy approach then.
           if ← lockfile.pathExists then
             throw <| IO.Error.alreadyExists 0 ""
-          discard <| IO.Prim.Handle.mk lockfile "w"
+          discard <| IO.FS.Handle.mk lockfile IO.FS.Mode.write
       catch
         | IO.Error.alreadyExists _ _ => do
           if firstTime then

Lake/SearchPath.lean

@@ -9,20 +9,16 @@ open System
 
 namespace Lake
 
-def getLeanPath? : IO (Option FilePath) := do
+def getLeanHome? : IO (Option FilePath) := do
   let out ← IO.Process.output {
-    cmd := "sh",
-    args := #["-c", "echo \"#eval IO.appPath >>= IO.println\" | lean --stdin"]
+    cmd := "lean",
+    args := #["--print-prefix"]
   }
   if out.exitCode == 0 then
     some <| FilePath.mk <| out.stdout.trim
   else
     none
 
-def getLeanHome? : IO (Option FilePath) := do
-  let leanPath? ← getLeanPath?
-  OptionM.run do (← (← leanPath?).parent).parent
-
 def getLakeHome? : IO (Option FilePath) := do
   (← IO.appPath).parent.bind FilePath.parent
 
@@ -51,4 +47,5 @@ def setupLeanSearchPath : IO Unit := do
     sp := lakeHome :: sp
   if let some leanHome ← getLeanHome? then
     sp := leanHome / "lib" / "lean" :: sp
-  Lean.searchPathRef.set (← Lean.addSearchPathFromEnv sp)
+  sp ← Lean.addSearchPathFromEnv sp
+  Lean.searchPathRef.set sp

leanpkg.toml

@@ -1,3 +1,4 @@
 [package]
 name = "lake"
 version = "1.0-pre"
+lean_version = "leanprover/lean4:nightly-2021-06-13"