diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index d220389..e49f23b 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -16,7 +16,7 @@ def getLakePath : IO FilePath := do match (← IO.getEnv "LAKE") with | some path => pure $ System.FilePath.mk path | none => - let lakePath := (←findSysroot?) / "bin" / "lake" + let lakePath := (←findSysroot) / "bin" / "lake" pure $ lakePath.withExtension System.FilePath.exeExtension -- Modified from the LSP Server @@ -37,7 +37,7 @@ def lakeSetupSearchPath (lakePath : System.FilePath) (imports : List String) : I let stdout := stdout.split (· == '\n') |>.getLast! let Except.ok (paths : LeanPaths) ← pure (Json.parse stdout >>= fromJson?) | throw $ userError s!"invalid output from `{cmdStr}`:\n{stdout}\nstderr:\n{stderr}" - initSearchPath (← findSysroot?) paths.oleanPath + initSearchPath (← findSysroot) paths.oleanPath paths.oleanPath.mapM realPathNormalized | 2 => pure [] -- no lakefile.lean | _ => throw $ userError s!"`{cmdStr}` failed:\n{stdout}\nstderr:\n{stderr}" diff --git a/lean-toolchain b/lean-toolchain index abadd14..8e380ba 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2022-02-27 +leanprover/lean4:nightly-2022-03-06