structure EvalAuto.EvalAutoConfig : Type

• maxHeartbeats : Nat

  Timeout for Lean code (Lean-auto + native provers)

• timeout : Nat

  Timeout for external provers, i.e. TPTP solvers and SMT solvers

• solverConfig : SolverConfig

  Solver configuration

• logFile : Option String

  Optional file for saving the log of the evaluation

• resultFile : Option String

  Optional file for saving the result of the evaluation

• nonterminates : Array Lean.Name

  On some problems, certain tactics may go into infinite loops not guarded by Core.checkMaxHeartbeats. These instances should be recorded here and avoided (throw error immediately) during evaluation.

instance EvalAuto.instToStringEvalAutoConfig : ToString EvalAutoConfig

Equations

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

def EvalAuto.runProverOnConst (name : Lean.Name) (prover : Array Auto.Lemma → Array Auto.Lemma → Lean.MetaM Lean.Expr) : Lean.CoreM Result

Run prover on the type of name, using premises collected from the proof of name Premises which only contain logic constants are filtered because they are assumed to be known by the prover

Equations

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

def EvalAuto.runAutoOnConsts (config : EvalAutoConfig) (names : Array Lean.Name) : Lean.CoreM Unit

Run lean-auto on all the constants listed in names

For the i-th theorem name in names, its entry in the result file has the following form: <i> <result> <time> <heartbeats> <name>

Equations

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

def EvalAuto.readRunAutoOnConstsResult (resultFile : String) : Lean.CoreM (Array (Lean.Name × Result × Nat × Nat))

Read the .result file generated by runAutoOnConsts

Equations

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

def EvalAuto.readRunAutoOnConstsResult.analyzeLine (fileName line : String) : Lean.CoreM (Lean.Name × Result × Nat × Nat)

Equations

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

def EvalAuto.runAutoOnNamesFile (cfg : EvalAutoConfig) (fname : String) : Lean.CoreM Unit

Equations

• EvalAuto.runAutoOnNamesFile cfg fname = do let names ← liftM (EvalAuto.NameArray.load fname) EvalAuto.runAutoOnConsts cfg names

structure EvalAuto.EvalAutoAsyncConfig : Type

• maxHeartbeats : Nat

  Timeout for Lean code (Lean-auto + native provers)

• timeout : Nat

  Timeout for external provers, i.e. TPTP solvers and SMT solvers

• solverConfig : SolverConfig

  Solver configuration

• resultFolder : String

  Folder for saving the result of the evaluation

• nprocs : Nat

  Number of processes to use

• batchSize : Nat

  Batch size

• memoryLimitKb : Option Nat

  Memory limit for each evaluation process, in kb

• timeLimitS : Option Nat

  Total time limit for each evaluation process, in seconds

• nonterminates : Array Lean.Name

def EvalAuto.Array.groupBySize {α : Type u_1} (xs : Array α) (size : Nat) : Option (Array (Array α))

Equations

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

def EvalAuto.leanFileLinesCallingRunAutoOnConsts (config : EvalAutoConfig) (names : Array Lean.Name) (evalModifiers : Array String) : Array String

Equations

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

def EvalAuto.evalAutoAtTheoremsAsync (config : EvalAutoAsyncConfig) (names imports : Array Lean.Name) (evalModifiers : Array String) : Lean.CoreM Unit

This should be run after import Mathlib, import Auto.EvaluateAuto.TestAuto, and should be run with a cwd where lake env creates an environment in which Mathlib, lean-auto and duper are available

The evaluation splits all theorems in Mathlib into batches of size config.batchSize, and uses config.nprocs parallel threads to run lean-auto on these theorems. For each thread, three files are created: · path.log: Detailed log · path.result: Concise result of evaluation · path.names: Names of all the theorems in this batch

Equations

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

def EvalAuto.evalAutoAtTheoremsAsync.tryWaitOn (evaluateFilesHandle : IO.FS.Handle) (running : Array (Nat × EvalTakenProc)) : Lean.CoreM (Array (Nat × EvalTakenProc))

Equations

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

def EvalAuto.evalAutoAtTheoremsAsync.evalFile (imports : Array Lean.Name) (evalModifiers : Array String) (names : Array Lean.Name) (config : EvalAutoConfig) : String

Equations

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

def EvalAuto.readEATAResult (config : EvalAutoAsyncConfig) : Lean.CoreM (Array (Lean.Name × Result × Nat × Nat))

Read results generated by evalAutoAtTheoremsAsync

Equations

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

def EvalAuto.readEATAEvaluateFiles (config : EvalAutoAsyncConfig) : Lean.CoreM (Array Nat × Array (Nat × Nat))

Read evaluateFiles.txt generated by evalAutoAtTheoremsAsync

Equations

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

def EvalAuto.evalAutoAtMathlibHumanTheorems (config : EvalAutoAsyncConfig) : Lean.CoreM Unit

Equations

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