def EvalAuto.rawProblemSizeOfAutoLemma (lem : Auto.Lemma) : Lean.CoreM Nat

Compute the size of the problem associated with lem

The goal of the problem is lem.type, and the premises of the problem are theorems that are used in lem.proof

Equations

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

def EvalAuto.rawProblemSizeOfConst (name : Lean.Name) : Lean.CoreM Nat

Compute the size of the problem associated with the constant name

The goal of the problem is the type of name, and the premises of the problem are theorems that are used in the proof of name

Equations

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

def EvalAuto.monomorphizedProblemOfAutoLemma (lem : Auto.Lemma) : Lean.CoreM (Option (Array Auto.Embedding.Lam.LamTerm))

Compute the monomorphized problem associated with lem

The goal of the problem is lem.type, and the premises of the problem are theorems that are used in lem.proof

Equations

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

def EvalAuto.monomorphizedProblemOfConst (name : Lean.Name) : Lean.CoreM (Option (Array Auto.Embedding.Lam.LamTerm))

Compute the monomorphized problem associated with the constant name

The goal of the problem is the type of name, and the premises of the problem are theorems that are used in the proof of name

Equations

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

def EvalAuto.monomorphizedProblemSizeOfConst (name : Lean.Name) : Lean.CoreM (Option Nat)

Equations

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

def EvalAuto.evalMonoSize (names : Array Lean.Name) (resultFile : String) (maxHeartbeats : Nat) : Lean.CoreM Unit

Equations

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

def EvalAuto.readEvalMonoSizeResult (resultFile : String) : Lean.CoreM (Array (Lean.Name × Nat × Option Nat))

Equations

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

def EvalAuto.readEvalMonoSizeResult.analyzeLine (line : String) : Lean.CoreM (Lean.Name × Nat × Option Nat)

Equations

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

def EvalAuto.testReduce (name : Lean.Name) : Lean.MetaM Nat

Run Meta.reduceAll on the type of name and the type of all theorems used in the proof of `name. Return the sum of sizes of the reduced theorem

Equations

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

def EvalAuto.testReduceWriteResult (mode : Lean.Meta.TransparencyMode) (path : String) (name : Lean.Name) : Lean.MetaM Unit

Equations

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

def EvalAuto.evalReduceSize (names : Array Lean.Name) (mode : Lean.Meta.TransparencyMode) (resultFolder : String) (nprocs memoryLimitKb timeLimitS : Nat) : Lean.CoreM Unit

Run testReduceWriteResult on each name in names. A new Lean 4 process is created for each name (this is because we want to pose time and memory limit on each of them)

Equations

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

def EvalAuto.evalReduceSize.tryWaitOn (evaluateNamesHandle : 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.readEvalReduceSizeResult (resultFolder : String) : Lean.CoreM (Array (Lean.Name × Except Nat Nat))

Return: Except.ok <size_of_reduced_expr> Except.error <ret_code>

Equations

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