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

fix: serve + print-paths without lakefile

Browse source
This commit is contained in:
Sebastian Ullrich 2022-03-21 10:31:18 +01:00 • committed by Mac
parent 65d00098c7
commit bdd5185a7f
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
Lake/CLI/Main.lean
View file

@ -208,10 +208,10 @@ The `print-paths` command is used internally by Lean 4 server.
def printPaths (imports : List String := []) : CliStateM PUnit := do
let (lean, lake) ← getInstall
let configFile := (← getRootDir) / (← getConfigFile)
if (← IO.getEnv invalidConfigEnvVar) matches some .. then
IO.eprintln s!"Error parsing '{configFile}'. Please restart the lean server after fixing the Lake configuration file."
exit 1
else if (← configFile.pathExists) then
if (← configFile.pathExists) then
if (← IO.getEnv invalidConfigEnvVar) matches some .. then
IO.eprintln s!"Error parsing '{configFile}'. Please restart the lean server after fixing the Lake configuration file."
exit 1
let ws ← loadWorkspace (← getSubArgs)
let ctx ← mkBuildContext ws lean lake
ws.root.buildImportsAndDeps imports |>.run LogMethods.eio ctx