From 2e43ab8877899030a00b699a7c5492b5ea91998b Mon Sep 17 00:00:00 2001 From: PratherConid Date: Tue, 7 Jan 2025 14:30:41 -0800 Subject: [PATCH] eval auto on mathlib --- Auto/EvaluateAuto/OS.lean | 4 ++ Auto/EvaluateAuto/TestAuto.lean | 86 ++++++++++++++++++++++++++++++ Auto/EvaluateAuto/TestTactics.lean | 18 +++---- Auto/Solver/SMT.lean | 2 +- Auto/Solver/TPTP.lean | 4 +- 5 files changed, 99 insertions(+), 15 deletions(-) create mode 100644 Auto/EvaluateAuto/OS.lean diff --git a/Auto/EvaluateAuto/OS.lean b/Auto/EvaluateAuto/OS.lean new file mode 100644 index 0000000..aae9b8a --- /dev/null +++ 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 index 9985a19..5976ab7 100644 --- 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 index 4082192..32700df 100644 --- 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,7 +304,7 @@ 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 := @@ -318,7 +312,7 @@ where | .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 index 0b31907..8f7bb2e 100644 --- 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 index 478e815..8de7170 100644 --- 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