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.FileSetupResult : Type

Result of running lake setup-file.

• success (setup : ModuleSetup) : FileSetupResult

  File configuration loaded and dependencies updated successfully.

• noLakefile : FileSetupResult

  No Lake project found, no setup was done.

• importsOutOfDate : FileSetupResult

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

• error (msg : String) : FileSetupResult

  Other error during Lake invocation.

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.