structure Lean.Server.FileWorker.LakeSetupFileOutput : Type

• spawnArgs : IO.Process.SpawnArgs
• exitCode : UInt32
• stdout : String
• stderr : String

def Lean.Server.FileWorker.runLakeSetupFile (m : DocumentMeta) (lakePath filePath : System.FilePath) (imports : Array Import) (handleStderr : String → IO Unit) : IO LakeSetupFileOutput

Equations

• One or more equations did not get rendered due to their size.

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) : IO String

inductive Lean.Server.FileWorker.FileSetupResultKind : Type

Categorizes possible outcomes of running lake setup-file.

• success : FileSetupResultKind

  File configuration loaded and dependencies updated successfully.

• noLakefile : FileSetupResultKind

  No Lake project found, no setup was done.

• importsOutOfDate : FileSetupResultKind

  Imports must be rebuilt but --no-build was specified.

• error (msg : String) : FileSetupResultKind

  Other error during Lake invocation.

structure Lean.Server.FileWorker.FileSetupResult : Type

Result of running lake setup-file.

• kind : FileSetupResultKind

  Kind of outcome.

• srcSearchPath : SearchPath

  Search path from successful setup, or else empty.

• fileOptions : Options

  Additional options from successful setup, or else empty.

def Lean.Server.FileWorker.FileSetupResult.ofSuccess (pkgSearchPath : SearchPath) (fileOptions : Options) : IO FileSetupResult

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.FileWorker.FileSetupResult.ofNoLakefile : IO FileSetupResult

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.FileWorker.FileSetupResult.ofImportsOutOfDate : IO FileSetupResult

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.FileWorker.FileSetupResult.ofError (msg : String) : IO FileSetupResult

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.FileWorker.setupFile (m : DocumentMeta) (imports : Array Import) (handleStderr : String → IO Unit) : IO FileSetupResult

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.