From 6a1897302b2caae7d5f1fcfa4a8a8b2fb8902a55 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 7 Oct 2021 19:13:49 +0200 Subject: [PATCH] chore: server: use exit code to communicate absence of package --- src/Lean/Server/FileWorker.lean | 36 ++++++++++++++++----------------- src/Leanpkg.lean | 22 ++++++++++---------- 2 files changed, 29 insertions(+), 29 deletions(-) diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 43b91624c4..fe22532014 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -121,12 +121,14 @@ section Initialization Compilation progress is reported to `hOut` via LSP notifications. Return the search path for source files. -/ partial def lakeSetupSearchPath (lakePath : System.FilePath) (m : DocumentMeta) (imports : Array Import) (hOut : FS.Stream) : IO SearchPath := do + let args := #["print-paths"] ++ imports.map (toString ·.module) + let cmdStr := " ".intercalate (toString lakePath :: args.toList) let lakeProc ← Process.spawn { stdin := Process.Stdio.null stdout := Process.Stdio.piped stderr := Process.Stdio.piped cmd := lakePath.toString - args := #["print-paths"] ++ imports.map (toString ·.module) + args } -- progress notification: report latest stderr line let rec processStderr (acc : String) : IO String := do @@ -139,23 +141,21 @@ section Initialization let stderr ← IO.asTask (processStderr "") Task.Priority.dedicated let stdout := String.trim (← lakeProc.stdout.readToEnd) let stderr ← IO.ofExcept stderr.get - if (← lakeProc.wait) == 0 then - if stdout.isEmpty then - pure [] -- e.g. no lakefile.lean - else - -- ignore any output up to the last line - -- TODO: leanpkg should instead redirect nested stdout output to stderr - let stdout := stdout.split (· == '\n') |>.getLast! - let Except.ok paths ← pure (Json.parse stdout >>= fromJson?) - | throwServerError s!"invalid output from `leanpkg print-paths`:\n{stdout}\nstderr:\n{stderr}" - let paths : LeanPaths ← IO.ofExcept <| fromJson? paths - let sp ← getBuiltinSearchPath - let sp ← addSearchPathFromEnv sp - let sp := paths.oleanPath ++ sp - searchPathRef.set sp - paths.srcPath.mapM realPathNormalized - else - throwServerError s!"`{lakePath} print-paths` failed:\n{stdout}\nstderr:\n{stderr}" + match (← lakeProc.wait) with + | 0 => + -- ignore any output up to the last line + -- TODO: leanpkg should instead redirect nested stdout output to stderr + let stdout := stdout.split (· == '\n') |>.getLast! + let Except.ok paths ← pure (Json.parse stdout >>= fromJson?) + | throwServerError s!"invalid output from `{cmdStr}`:\n{stdout}\nstderr:\n{stderr}" + let paths : LeanPaths ← IO.ofExcept <| fromJson? paths + let sp ← getBuiltinSearchPath + let sp ← addSearchPathFromEnv sp + let sp := paths.oleanPath ++ sp + searchPathRef.set sp + paths.srcPath.mapM realPathNormalized + | 2 => pure [] -- no lakefile.lean + | _ => throwServerError s!"`{cmdStr}` failed:\n{stdout}\nstderr:\n{stderr}" def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) : IO (Snapshot × SearchPath) := do let inputCtx := Parser.mkInputContext m.text.source "" diff --git a/src/Leanpkg.lean b/src/Leanpkg.lean index 18c42325f4..df86545e6d 100644 --- a/src/Leanpkg.lean +++ b/src/Leanpkg.lean @@ -93,9 +93,9 @@ def execMake (makeArgs : List String) (cfg : Build.Config) : IO Unit := withLock } execCmd spawnArgs -def buildImports (imports : List String) (leanArgs : List String) : IO Unit := do +def buildImports (imports : List String) (leanArgs : List String) : IO UInt32 := do unless ← leanpkgTomlFn.pathExists do - return + return 2 let manifest ← readManifest let cfg ← configure let imports := imports.map (·.toName) @@ -109,6 +109,7 @@ def buildImports (imports : List String) (leanArgs : List String) : IO Unit := d else Build.buildModules buildCfg localImports IO.println <| Lean.Json.compress <| Lean.toJson cfg.toLeanPaths + return 0 def build (makeArgs leanArgs : List String) : IO Unit := do let cfg ← configure @@ -154,11 +155,11 @@ build [] configure and build *.olean files See `leanpkg help ` for more information on a specific command." -def main : (cmd : String) → (leanpkgArgs leanArgs : List String) → IO Unit - | "init", [Name], [] => init Name - | "configure", [], [] => discard <| configure +def main : (cmd : String) → (leanpkgArgs leanArgs : List String) → IO UInt32 + | "init", [Name], [] => init Name *> pure 0 + | "configure", [], [] => configure *> pure 0 | "print-paths", leanpkgArgs, leanArgs => buildImports leanpkgArgs leanArgs - | "build", makeArgs, leanArgs => build makeArgs leanArgs + | "build", makeArgs, leanArgs => build makeArgs leanArgs *> pure 0 | "help", ["configure"], [] => IO.println "Download dependencies Usage: @@ -169,7 +170,7 @@ This command sets up the `build/deps` directory. For each (transitive) git dependency, the specified commit is checked out into a sub-directory of `build/deps`. If there are dependencies on multiple versions of the same package, the version materialized is undefined. No copy -is made of local dependencies." +is made of local dependencies." *> pure 0 | "help", ["build"], [] => IO.println "download dependencies and build *.olean files Usage: @@ -187,15 +188,15 @@ NOTE: building and linking dependent libraries currently has to be done manually ``` $ (cd a; leanpkg build lib) $ (cd b; leanpkg build bin LINK_OPTS=../a/build/lib/libA.a) -```" +```" *> pure 0 | "help", ["init"], [] => IO.println "Create a new Lean package in the current directory Usage: leanpkg init This command creates a new Lean package with the given name in the current -directory." - | "help", _, [] => IO.println usage +directory." *> pure 0 + | "help", _, [] => IO.println usage *> pure 0 | _, _, _ => throw <| IO.userError usage private def splitCmdlineArgsCore : List String → List String × List String @@ -221,7 +222,6 @@ def main (args : List String) : IO UInt32 := do Lean.initSearchPath none -- HACK let (cmd, outerArgs, innerArgs) ← Leanpkg.splitCmdlineArgs args Leanpkg.main cmd outerArgs innerArgs - pure 0 catch e => IO.eprintln e -- avoid "uncaught exception: ..." pure 1