eval auto on mathlib

leanprover-community · Jan 7, 2025 · 2e43ab8 · 2e43ab8
1 parent 25c8f25
commit 2e43ab8
Show file tree

Hide file tree

Showing 5 changed files with 99 additions and 15 deletions.
diff --git a/Auto/EvaluateAuto/OS.lean b/Auto/EvaluateAuto/OS.lean
@@ -0,0 +1,4 @@
+abbrev EvalProc := IO.Process.Child ⟨.piped, .piped, .piped⟩
+
+def EvalProc.create (path : String) (args : Array String) : IO EvalProc :=
+  IO.Process.spawn {stdin := .piped, stdout := .piped, stderr := .piped, cmd := path, args := args}
diff --git a/Auto/EvaluateAuto/TestAuto.lean b/Auto/EvaluateAuto/TestAuto.lean
@@ -1,4 +1,5 @@
 import Lean
+import Auto.EvaluateAuto.OS
 import Auto.EvaluateAuto.Result
 import Auto.EvaluateAuto.ConstAnalysis
 import Auto.EvaluateAuto.EnvAnalysis
@@ -18,6 +19,7 @@ inductive SolverConfig where
   | leanSmt
   | smt (solverName : Solver.SMT.SolverName)
   | tptp (solverName : Solver.TPTP.SolverName) (path : String)
+  deriving Repr
 
 instance : ToString SolverConfig where
   toString : SolverConfig → String
@@ -178,4 +180,88 @@ def runAutoOnNamesFile (cfg : EvalAutoConfig) (fname : String) : CoreM Unit := d
   let names ← NameArray.load fname
   runAutoOnConsts cfg names
 
+structure EvalAutoOnMathlibConfig where
+  /-- Timeout for Lean code (Lean-auto + native provers) -/
+  maxHeartbeats : Nat           := 65536
+  /-- Timeout for external provers, i.e. TPTP solvers and SMT solvers -/
+  timeout       : Nat           := 10
+  /-- Solver configuration -/
+  solverConfig  : SolverConfig
+  /-- Folder for saving the result of the evaluation -/
+  resultFolder  : String
+  /-- Number of threads to use -/
+  nthreads      : Nat
+  /-- Batch size -/
+  batchSize     : Nat
+
+def Array.groupBySize (xs : Array α) (size : Nat) : Option (Array (Array α)) :=
+  if size == 0 then
+    .none
+  else
+    let n := (xs.size + size - 1) / size
+    let ret := Array.mk <| (List.range n).map (fun i => Array.mk <| (xs.toList.drop (size * i)).take size)
+    some ret
+
+def evalAutoAtMathlibHumanTheorems (config : EvalAutoOnMathlibConfig) : CoreM Unit := do
+  if !(← System.FilePath.isDir config.resultFolder) then
+    IO.FS.createDir config.resultFolder
+  let evaluateFilesHandle ← IO.FS.Handle.mk (config.resultFolder ++ "/evaluateFiles.txt") .write
+  let all ← allHumanTheorems
+  let .some batches := Array.groupBySize all config.batchSize
+    | throwError "Batch size must be nonzero"
+  let mut running := #[]
+  for (batch, idx) in batches.zipWithIndex do
+    evaluateFilesHandle.putStrLn (toString idx)
+    evaluateFilesHandle.flush
+    let evalProc ← EvalProc.create "lake" #["env", "lean", "--stdin"]
+    let logPath := config.resultFolder ++ toString idx
+    evalProc.stdin.putStr (evalFile batch logPath)
+    let (_, evalProc) ← evalProc.takeStdin
+    running := running.push (idx, evalProc)
+    while running.size >= config.nthreads do
+      running ← tryWaitOn evaluateFilesHandle running
+  while running.size != 0 do
+    running ← tryWaitOn evaluateFilesHandle running
+where
+  tryWaitOn (evaluateFilesHandle : IO.FS.Handle) (running : Array (Nat × _)) : CoreM (Array (Nat × _)) := do
+    let mut running' := #[]
+    for (idx, proc) in running do
+      let retCode? ← proc.tryWait
+      match retCode? with
+      | .some retCode =>
+        evaluateFilesHandle.putStrLn s!"{idx} : {retCode}"
+        evaluateFilesHandle.flush
+      | .none => running' := running'.push (idx, proc)
+    return running'
+  evalFile
+    (thms : Array Name) (logPath : String) : String :=
+    let lb := "{"
+    let rb := "}"
+    let thmsStrs : List String :=
+      match thms.toList.getLast? with
+      | .some last =>
+        thms.toList.dropLast.map (fun n => s!"  {repr n},") ++ [s!"  {repr last}"]
+      | .none => []
+    let lines := [
+        s!"import Mathlib",
+        "import Auto.EvaluateAuto.TestAuto",
+        "import Auto.Tactic",
+        "open Lean EvalAuto",
+        "",
+        "def thms : Std.HashSet Name := Std.HashSet.ofList ["
+      ] ++ thmsStrs ++ [
+        "]",
+        "",
+        "def action : CoreM Unit := do",
+        "  let p ← initSrcSearchPath",
+        s!"  let _ ← runAutoOnConsts",
+        s!"    {lb} maxHeartbeats := {config.maxHeartbeats}, timeout := {config.timeout},",
+        s!"      solverConfig := {repr config.solverConfig},",
+        s!"      logFile := Option.some ({repr (logPath ++ ".log")}), resultFile := Option.some ({repr (logPath ++ ".result")}){rb}",
+        "    thms",
+        "",
+        "#eval action"
+      ]
+    String.intercalate "\n" lines
+
 end EvalAuto
diff --git a/Auto/EvaluateAuto/TestTactics.lean b/Auto/EvaluateAuto/TestTactics.lean
@@ -1,4 +1,5 @@
 import Lean
+import Auto.EvaluateAuto.OS
 import Auto.EvaluateAuto.Result
 import Auto.EvaluateAuto.ConstAnalysis
 import Auto.EvaluateAuto.EnvAnalysis
@@ -252,16 +253,9 @@ structure EvalTacticOnMathlibConfig where
     recorded here and avoided (throw error immediately) during evaluation.
   -/
   nonterminates : Array (RegisteredTactic × Name)
-  /--
-    Number of threads to use
-  -/
+  /-- Number of threads to use -/
   nthreads      : Nat
 
-abbrev EvalProc := IO.Process.Child ⟨.piped, .piped, .piped⟩
-
-def EvalProc.create (path : String) (args : Array String) : IO EvalProc :=
-  IO.Process.spawn {stdin := .piped, stdout := .piped, stderr := .piped, cmd := path, args := args}
-
 /--
   This should be run after `import Mathlib`, and should be run with a `cwd` where
     `lake env` creates an environment in which `Mathlib` and `lean-auto` are available
@@ -290,7 +284,7 @@ def evalTacticsAtMathlibHumanTheorems (config : EvalTacticOnMathlibConfig) : Cor
     let evalProc ← EvalProc.create "lake" #["env", "lean", "--stdin"]
     let logPath := config.resultFolder ++ extraLogPath
     let validThms := (allTally.get? mm).getD #[]
-    evalProc.stdin.putStr (evalFile mm validThms logPath config.tactics)
+    evalProc.stdin.putStr (evalFile mm validThms logPath config)
     let (_, evalProc) ← evalProc.takeStdin
     running := running.push (mm, evalProc)
     while running.size >= config.nthreads do
@@ -310,15 +304,15 @@ where
     return running'
   evalFile
     (mm : Name) (validThms : Array Name)
-    (logPath : String) (tacs : Array RegisteredTactic) : String :=
+    (logPath : String) (config : EvalTacticOnMathlibConfig) : String :=
     let lb := "{"
     let rb := "}"
     let thmsStrs : List String :=
       match validThms.toList.getLast? with
       | .some last =>
         validThms.toList.dropLast.map (fun n => s!"  {repr n},") ++ [s!"  {repr last}"]
       | .none => []
-    let tacsStr := String.intercalate ", " (tacs.map (fun tac => "." ++ toString tac)).toList
+    let tacsStr := String.intercalate ", " (config.tactics.map (fun tac => "." ++ toString tac)).toList
     let lines := [
         s!"import {mm}",
         "import Auto.EvaluateAuto.TestTactics",
@@ -332,7 +326,7 @@ where
         "def action : CoreM Unit := do",
         "  let p ← initSrcSearchPath",
         s!"  let _ ← evalAtModule ({repr mm}) p (fun ci => humanThms.contains ci.name)",
-        s!"    {lb} tactics := #[{tacsStr}],",
+        s!"    {lb} maxHeartbeats := {config.maxHeartbeats}, tactics := #[{tacsStr}],",
         s!"      logFile := {repr (logPath ++ ".log")}, resultFile := {repr (logPath ++ ".result")},",
         s!"      nonterminates := #[] {rb}",
         "",

diff --git a/Auto/Solver/SMT.lean b/Auto/Solver/SMT.lean
@@ -62,7 +62,7 @@ inductive SolverName where
   | z3
   | cvc4
   | cvc5
-deriving BEq, Hashable, Inhabited
+deriving BEq, Hashable, Inhabited, Repr
 
 instance : ToString SolverName where
   toString : SolverName → String

diff --git a/Auto/Solver/TPTP.lean b/Auto/Solver/TPTP.lean
@@ -43,7 +43,7 @@ namespace Solver.TPTP
 inductive ZEPortType where
   | fo
   | lams
-deriving BEq, Hashable, Inhabited
+deriving BEq, Hashable, Inhabited, Repr
 
 inductive SolverName where
   -- Disable TPTP prover
@@ -53,7 +53,7 @@ inductive SolverName where
   -- E prover, higher-order version
   | eproverHo
   | vampire
-deriving BEq, Hashable, Inhabited
+deriving BEq, Hashable, Inhabited, Repr
 
 instance : ToString SolverName where
   toString : SolverName → String