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 : Lake.FilePath) (filePath : Lake.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 : Lake.FilePath) (handleStderr : String → IO Unit) (args : Array String) (lakeProc : IO.Process.Child { toStdioConfig := { 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

• success: Lean.Server.FileWorker.FileSetupResultKind
• noLakefile: Lean.Server.FileWorker.FileSetupResultKind
• importsOutOfDate: Lean.Server.FileWorker.FileSetupResultKind
• error: String → Lean.Server.FileWorker.FileSetupResultKind

structure Lean.Server.FileWorker.FileSetupResult : Type

• kind : Lean.Server.FileWorker.FileSetupResultKind
• srcSearchPath : Lean.SearchPath
• fileOptions : Lean.Options

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.FileSetupResult.addGlobalOptions (result : Lean.Server.FileWorker.FileSetupResult) (globalOptions : Lean.Options) : 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.

Equations

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