structure Lean.Server.FileWorker.LakeSetupFileOutput : Type

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

def Lean.Server.FileWorker.runLakeSetupFile (m : Lean.Server.DocumentMeta) (lakePath filePath : System.FilePath) (imports : Array Lean.Import) (handleStderr : String → IO Unit) : IO Lean.Server.FileWorker.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: 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.

structure Lean.Server.FileWorker.FileSetupResult : Type

Result of running lake setup-file.

• kind : Lean.Server.FileWorker.FileSetupResultKind

  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.

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Server.FileWorker.setupFile (m : Lean.Server.DocumentMeta) (imports : Array Lean.Import) (handleStderr : String → IO Unit) : IO Lean.Server.FileWorker.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.