- spawnArgs : IO.Process.SpawnArgs
- exitCode : UInt32
- stdout : String
- stderr : String
Instances For
def
Lean.Server.FileWorker.runLakeSetupFile
(m : Lean.Server.DocumentMeta)
(lakePath filePath : System.FilePath)
(imports : Array Lean.Import)
(handleStderr : String → IO Unit)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
partial def
Lean.Server.FileWorker.runLakeSetupFile.processStderr
(lakePath : System.FilePath)
(handleStderr : String → IO Unit)
(args : Array String)
(lakeProc :
IO.Process.Child
{ stdin := IO.Process.Stdio.null, stdout := IO.Process.Stdio.piped, stderr := IO.Process.Stdio.piped,
cmd := lakePath.toString, args := args, cwd := none, env := #[], setsid := false }.toStdioConfig)
(acc : String)
:
Categorizes possible outcomes of running lake setup-file
.
- success: Lean.Server.FileWorker.FileSetupResultKind
File configuration loaded and dependencies updated successfully.
- noLakefile: Lean.Server.FileWorker.FileSetupResultKind
No Lake project found, no setup was done.
- importsOutOfDate: Lean.Server.FileWorker.FileSetupResultKind
Imports must be rebuilt but
--no-build
was specified. - error: String → Lean.Server.FileWorker.FileSetupResultKind
Other error during Lake invocation.
Instances For
Result of running lake setup-file
.
Kind of outcome.
- srcSearchPath : Lean.SearchPath
Search path from successful setup, or else empty.
- fileOptions : Lean.Options
Additional options from successful setup, or else empty.
Instances For
def
Lean.Server.FileWorker.FileSetupResult.ofSuccess
(pkgSearchPath : Lean.SearchPath)
(fileOptions : Lean.Options)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Server.FileWorker.setupFile
(m : Lean.Server.DocumentMeta)
(imports : Array Lean.Import)
(handleStderr : String → IO Unit)
:
Uses lake setup-file
to compile dependencies on the fly and add them to LEAN_PATH
.
Compilation progress is reported to handleStderr
. Returns the search path for
source files and the options for the file.