def EvalAuto.testUnknownConstant (ci : Lean.ConstantInfo) : Lean.Elab.Tactic.TacticM Unit

Solves the goal using sorry if ci does not contain unknown constants, and throws and error if ci contains unknown constants

When we evaluate tactics on a theorem T, we replay the file that defines T and calls the tactic on the environment env just before the declaration of T. Since there are commands that define multiple constants simultaneously, it is possible that the proof or type of T contains constants not present in env. We run testUnknownConstant to detect such situations.

Equations

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

def EvalAuto.useRfl : Lean.Elab.Tactic.TacticM Unit

Equations

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

def EvalAuto.useSimp : Lean.Elab.Tactic.TacticM Unit

Equations

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

def EvalAuto.useSimpAll : Lean.Elab.Tactic.TacticM Unit

Equations

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

def EvalAuto.useSimpAllWithPremises (ci : Lean.ConstantInfo) : Lean.Elab.Tactic.TacticM Unit

Equations

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

def EvalAuto.useAesop (subHeartbeats : Nat) : Lean.Elab.Tactic.TacticM Unit

Tactic sequence: intros; aesop Only guaranteed to work for aesop @ Lean v4.14.0

Equations

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

def EvalAuto.useAesopWithPremises (subHeartbeats : Nat) (ci : Lean.ConstantInfo) : Lean.Elab.Tactic.TacticM Unit

Tactic sequence: intros; aesop (add unsafe premise₁) ⋯ (add unsafe premiseₙ) Only guaranteed to work for aesop @ Lean v4.14.0

Equations

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

def EvalAuto.useAesopWithPremises.synth : Lean.SourceInfo

Equations

• EvalAuto.useAesopWithPremises.synth = Lean.SourceInfo.synthetic default default

def EvalAuto.useAesopWithPremises.mkAddIdentStx (ident : Lean.Ident) : Lean.Syntax

Equations

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

def EvalAuto.useDuper (ci : Lean.ConstantInfo) : Lean.Elab.Tactic.TacticM Unit

Equations

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

def EvalAuto.useDuper.mkDuperStx (idents : Array Lean.Ident) : Lean.Syntax

Equations

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

def EvalAuto.useAuto (ignoreNonQuasiHigherOrder : Bool) (config : SolverConfig) (timeout : Nat) (ci : Lean.ConstantInfo) : Lean.Elab.Tactic.TacticM Unit

Equations

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

inductive EvalAuto.RegisteredTactic : Type

• testUnknownConstant : RegisteredTactic
• useRfl : RegisteredTactic
• useSimp : RegisteredTactic
• useSimpAll : RegisteredTactic
• useSimpAllWithPremises : RegisteredTactic
• useAesop (subHeartbeats : Nat) : RegisteredTactic
• useAesopWithPremises (subHeartbeats : Nat) : RegisteredTactic
• useDuper : RegisteredTactic
• useAuto (ignoreNonQuasiHigherOrder : Bool) (config : SolverConfig) (timeout : Nat) : RegisteredTactic

def EvalAuto.instBEqRegisteredTactic.beq : RegisteredTactic → RegisteredTactic → Bool

Equations

• EvalAuto.instBEqRegisteredTactic.beq EvalAuto.RegisteredTactic.testUnknownConstant EvalAuto.RegisteredTactic.testUnknownConstant = true
• EvalAuto.instBEqRegisteredTactic.beq EvalAuto.RegisteredTactic.useRfl EvalAuto.RegisteredTactic.useRfl = true
• EvalAuto.instBEqRegisteredTactic.beq EvalAuto.RegisteredTactic.useSimp EvalAuto.RegisteredTactic.useSimp = true
• EvalAuto.instBEqRegisteredTactic.beq EvalAuto.RegisteredTactic.useSimpAll EvalAuto.RegisteredTactic.useSimpAll = true
• EvalAuto.instBEqRegisteredTactic.beq EvalAuto.RegisteredTactic.useSimpAllWithPremises EvalAuto.RegisteredTactic.useSimpAllWithPremises = true
• EvalAuto.instBEqRegisteredTactic.beq (EvalAuto.RegisteredTactic.useAesop a) (EvalAuto.RegisteredTactic.useAesop b) = (a == b)
• EvalAuto.instBEqRegisteredTactic.beq (EvalAuto.RegisteredTactic.useAesopWithPremises a) (EvalAuto.RegisteredTactic.useAesopWithPremises b) = (a == b)
• EvalAuto.instBEqRegisteredTactic.beq EvalAuto.RegisteredTactic.useDuper EvalAuto.RegisteredTactic.useDuper = true
• EvalAuto.instBEqRegisteredTactic.beq (EvalAuto.RegisteredTactic.useAuto a a_1 a_2) (EvalAuto.RegisteredTactic.useAuto b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• EvalAuto.instBEqRegisteredTactic.beq x✝¹ x✝ = false

instance EvalAuto.instBEqRegisteredTactic : BEq RegisteredTactic

Equations

• EvalAuto.instBEqRegisteredTactic = { beq := EvalAuto.instBEqRegisteredTactic.beq }

instance EvalAuto.instHashableRegisteredTactic : Hashable RegisteredTactic

Equations

• EvalAuto.instHashableRegisteredTactic = { hash := EvalAuto.instHashableRegisteredTactic.hash }

def EvalAuto.instHashableRegisteredTactic.hash : RegisteredTactic → UInt64

Equations

• EvalAuto.instHashableRegisteredTactic.hash EvalAuto.RegisteredTactic.testUnknownConstant = 0
• EvalAuto.instHashableRegisteredTactic.hash EvalAuto.RegisteredTactic.useRfl = 1
• EvalAuto.instHashableRegisteredTactic.hash EvalAuto.RegisteredTactic.useSimp = 2
• EvalAuto.instHashableRegisteredTactic.hash EvalAuto.RegisteredTactic.useSimpAll = 3
• EvalAuto.instHashableRegisteredTactic.hash EvalAuto.RegisteredTactic.useSimpAllWithPremises = 4
• EvalAuto.instHashableRegisteredTactic.hash (EvalAuto.RegisteredTactic.useAesop a) = mixHash 5 (hash a)
• EvalAuto.instHashableRegisteredTactic.hash (EvalAuto.RegisteredTactic.useAesopWithPremises a) = mixHash 6 (hash a)
• EvalAuto.instHashableRegisteredTactic.hash EvalAuto.RegisteredTactic.useDuper = 7
• EvalAuto.instHashableRegisteredTactic.hash (EvalAuto.RegisteredTactic.useAuto a a_1 a_2) = mixHash (mixHash (mixHash 8 (hash a)) (hash a_1)) (hash a_2)

def EvalAuto.instReprRegisteredTactic.repr : RegisteredTactic → Nat → Std.Format

Equations

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

instance EvalAuto.instReprRegisteredTactic : Repr RegisteredTactic

Equations

• EvalAuto.instReprRegisteredTactic = { reprPrec := EvalAuto.instReprRegisteredTactic.repr }

instance EvalAuto.instToStringRegisteredTactic : ToString RegisteredTactic

Equations

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

def EvalAuto.RegisteredTactic.toCiTactic : RegisteredTactic → Lean.ConstantInfo → Lean.Elab.Tactic.TacticM Unit

Equations

• EvalAuto.RegisteredTactic.testUnknownConstant.toCiTactic = EvalAuto.testUnknownConstant
• EvalAuto.RegisteredTactic.useRfl.toCiTactic = fun (x : Lean.ConstantInfo) => EvalAuto.useRfl
• EvalAuto.RegisteredTactic.useSimp.toCiTactic = fun (x : Lean.ConstantInfo) => EvalAuto.useSimp
• EvalAuto.RegisteredTactic.useSimpAll.toCiTactic = fun (x : Lean.ConstantInfo) => EvalAuto.useSimpAll
• EvalAuto.RegisteredTactic.useSimpAllWithPremises.toCiTactic = EvalAuto.useSimpAllWithPremises
• (EvalAuto.RegisteredTactic.useAesop a).toCiTactic = fun (x : Lean.ConstantInfo) => EvalAuto.useAesop a
• (EvalAuto.RegisteredTactic.useAesopWithPremises a).toCiTactic = EvalAuto.useAesopWithPremises a
• EvalAuto.RegisteredTactic.useDuper.toCiTactic = EvalAuto.useDuper
• (EvalAuto.RegisteredTactic.useAuto a a_1 a_2).toCiTactic = EvalAuto.useAuto a a_1 a_2

def EvalAuto.runTacticsAtConstantDeclaration (name : Lean.Name) (tactics : Array (Lean.ConstantInfo → Lean.Elab.Tactic.TacticM Unit)) : Lean.CoreM (Array Result)

Use runWithEffectOfCommands to run tactics at the place just before the command that created the constant name

Equations

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

structure EvalAuto.EvalTacticConfig : Type

• maxHeartbeats : Nat

  Timeout for each tactic

• tactics : Array RegisteredTactic

  Tactics to run at each constant declaration

• 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 (RegisteredTactic × 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.instToStringEvalTacticConfig : ToString EvalTacticConfig

Equations

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

def EvalAuto.evalTacticsAtModule (modName : Lean.Name) (filter : Lean.ConstantInfo → Bool) (config : EvalTacticConfig) : Lean.CoreM Unit

Effectively runTacticsAtConstantDeclaration at each constant in modName which satisfies filter\

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

Equations

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

def EvalAuto.evalTacticsAtModule.evalAction (context : Lean.Core.Context) (state : Lean.Core.State) (ci : Lean.ConstantInfo) (logFileHandle? : Option IO.FS.Handle) (config : EvalTacticConfig) (nonterms : Std.HashSet (RegisteredTactic × Lean.Name)) : IO (Array (Result × Nat × Nat))

Equations

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

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

Equations

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

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

Equations

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

structure EvalAuto.EvalTacticOnMathlibConfig : Type

• maxHeartbeats : Nat

  Timeout for each tactic

• tactics : Array RegisteredTactic

  Tactics to run at each constant declaration

• resultFolder : String

  Folder for saving the result of the evaluation

• nprocs : Nat

  Number of processes to use

• memoryLimitKb : Option Nat

  Memory limit for each evaluation process, in kb

• timeLimitS : Option Nat

  Total time limit for each evaluation process, in seconds

• moduleFilter : Lean.Name → Bool

  Specify modules to run tactics on

• nonterminates : Array (RegisteredTactic × 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.

def EvalAuto.evalTacticsAtMathlibHumanTheorems (config : EvalTacticOnMathlibConfig) : Lean.CoreM Unit

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

Equations

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

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

Equations

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

def EvalAuto.evalTacticsAtMathlibHumanTheorems.evalFile (mm : Lean.Name) (validThms : Array Lean.Name) (logPath : String) (config : EvalTacticOnMathlibConfig) : Lean.CoreM String

Equations

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

def EvalAuto.readETMHTResult (config : EvalTacticOnMathlibConfig) : Lean.CoreM (Array (Lean.Name × Array (Lean.Name × Array (Result × Nat × Nat))))

Read results generated by evalTacticsAtMathlibHumanTheorems

Equations

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

def EvalAuto.readETMHTResultAllowNonRet (config : EvalTacticOnMathlibConfig) : Lean.CoreM (Array String × Array (Lean.Name × Array (Lean.Name × Array (Result × Nat × Nat))))

Similar to readETMHTResult, but will not throw error if a .result file is empty. Instead, its return value contains all the paths to the .result files that are empty.

Equations

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

def EvalAuto.gatherETMHTResult (config : EvalTacticOnMathlibConfig) : Lean.CoreM Unit

Read results generated by evalTacticsAtMathlibHumanTheorems and store them in a single file gatheredResult in config.resultFolder

Equations

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

def EvalAuto.gatherETMHTResultAllowNonRet (config : EvalTacticOnMathlibConfig) : Lean.CoreM Unit

Similar to gatherETMHTResult, but will not throw error if a .result file is empty. Instead, its saves ⟨all the paths to the .result files that are empty⟩ in nonRetPaths.

Equations

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

def EvalAuto.readETMHTEvaluateFiles (config : EvalTacticOnMathlibConfig) : Lean.CoreM (Array Lean.Name × Array (Lean.Name × Nat))

Read evaluateFiles.txt generated by evalTacticsAtMathlibHumanTheorems

Equations

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