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) (header : ModuleHeader) (handleStderr : String → IO Unit) : IO LakeSetupFileOutput

Equations

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

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.

• setup : ModuleSetup

  Configuration from a successful setup, or else the default.

def Lean.Server.FileWorker.FileSetupResult.ofSuccess (setup : ModuleSetup) : IO FileSetupResult

Equations

• Lean.Server.FileWorker.FileSetupResult.ofSuccess setup = pure { kind := Lean.Server.FileWorker.FileSetupResultKind.success, setup := setup }

def Lean.Server.FileWorker.FileSetupResult.ofNoLakefile (m : DocumentMeta) (header : ModuleHeader) : IO FileSetupResult

Equations

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

def Lean.Server.FileWorker.FileSetupResult.ofImportsOutOfDate (m : DocumentMeta) (header : ModuleHeader) : IO FileSetupResult

Equations

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

def Lean.Server.FileWorker.FileSetupResult.ofError (m : DocumentMeta) (header : ModuleHeader) (msg : String) : IO FileSetupResult

Equations

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

def Lean.Server.FileWorker.setupFile (m : DocumentMeta) (header : ModuleHeader) (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.

Equations

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