@[reducible, inline]

abbrev EvalAuto.EvalProc : Type

Equations

• EvalAuto.EvalProc = IO.Process.Child { stdin := IO.Process.Stdio.piped, stdout := IO.Process.Stdio.null, stderr := IO.Process.Stdio.null }

@[reducible, inline]

abbrev EvalAuto.EvalTakenProc : Type

Equations

• EvalAuto.EvalTakenProc = IO.Process.Child { stdin := IO.Process.Stdio.null, stdout := IO.Process.Stdio.null, stderr := IO.Process.Stdio.null }

def EvalAuto.EvalProc.create (path : String) (args : Array String) : IO EvalProc

Equations

• EvalAuto.EvalProc.create path args = IO.Process.spawn { stdin := IO.Process.Stdio.piped, stdout := IO.Process.Stdio.null, stderr := IO.Process.Stdio.null, cmd := path, args := args }

def EvalAuto.bashRepr (s : String) : String

Equations

• EvalAuto.bashRepr s = "\"" ++ String.join (List.map EvalAuto.bashRepr.go s.data) ++ "\""

def EvalAuto.bashRepr.go : Char → String

Equations

• EvalAuto.bashRepr.go '$' = "\\$"
• EvalAuto.bashRepr.go '`' = "\\`"
• EvalAuto.bashRepr.go '\"' = "\\\""
• EvalAuto.bashRepr.go '\\' = "\\\\"
• EvalAuto.bashRepr.go x✝ = { data := [x✝] }

def EvalAuto.runLeanFileUsingNewLeanProcess (leanFile : String) (memoryLimitKb timeLimitS : Nat) : Lean.CoreM EvalTakenProc

Equations

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

def EvalAuto.runFunctionOnConstsUsingNewLeanProcess (names : Array Lean.Name) (funName : Lean.Name) (funArgs : Array String) (memoryLimitKb timeLimitS : Nat) : Lean.CoreM EvalTakenProc

This function runs funName funArgs on all constants in names, using a new Lean process

This should be run importing all the modules associated with constants in names ++ #[funName], and should be run with a cwd where lake env creates an environment in which funName and all the constants in names are available

Equations

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

def EvalAuto.runFunctionOnConstsUsingNewLeanProcess.evalFile (imports names : Array Lean.Name) (funStr : String) : String

Equations

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

def EvalAuto.runFunctionOnConstsUsingNewLeanProcess.getModuleImports (names : Array Lean.Name) : Lean.CoreM (Array Lean.Name)

Equations

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