From af256123f39990bb4cadd6f8d3333f3bb044a69a Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 15 Nov 2024 23:29:37 -0800 Subject: [PATCH 01/19] doc: Update icon --- doc/icon.svg | 184 +++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 134 insertions(+), 50 deletions(-) diff --git a/doc/icon.svg b/doc/icon.svg index 394b412..eb26a19 100644 --- a/doc/icon.svg +++ b/doc/icon.svg @@ -4,17 +4,17 @@ + + + + + + + + + + + + + + + id="layer4" + inkscape:label="bg" /> + + + + + + + + + + + From ce3af887be2594e9b5a80532982fd6cc9c652909 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 15 Nov 2024 23:36:28 -0800 Subject: [PATCH 02/19] doc: Rationale document --- README.md | 2 ++ doc/rationale.md | 30 ++++++++++++++++++++++++++++++ 2 files changed, 32 insertions(+) create mode 100644 doc/rationale.md diff --git a/README.md b/README.md index 04213ae..7b5060f 100644 --- a/README.md +++ b/README.md @@ -7,6 +7,8 @@ A Machine-to-Machine interaction system for Lean 4. Pantograph provides interfaces to execute proofs, construct expressions, and examine the symbol list of a Lean project for machine learning. +See [documentations][doc/] for design rationale and references. + ## Installation For Nix users, run diff --git a/doc/rationale.md b/doc/rationale.md new file mode 100644 index 0000000..87c1606 --- /dev/null +++ b/doc/rationale.md @@ -0,0 +1,30 @@ +# Design Rationale + +A great problem in machine learning is to use ML agents to automatically prove +mathematical theorems. This sort of proof necessarily involves *search*. +Compatibility for search is the main reason for creating Pantograph. The Lean 4 +LSP interface is not conducive to search. Pantograph is designed with this in +mind. It emphasizes the difference between 3 views of a proof: + +- **Presentation View**: The view of a written, polished proof. e.g. Mathlib and + math papers are almost always written in this form. +- **Search View**: The view of a proof exploration trajectory. This is not + explicitly supported by Lean LSP. +- **Kernel View**: The proof viewed as a set of metavariables. + +Pantograph enables proof agents to operate on the search view. + +## Name + +The name Pantograph is a pun. It means two things +- A pantograph is an instrument for copying down writing. As an agent explores + the vast proof search space, Pantograph records the current state to ensure + the proof is sound. +- A pantograph is also an equipment for an electric train. It supplies power to + a locomotive. In comparison the (relatively) simple Pantograph software powers + theorem proving projects. + +## References + +* [Pantograph Paper](https://arxiv.org/abs/2410.16429) + From 5d676154f1ba1c0cdb542c9feb8d583c89643fcb Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 16 Nov 2024 21:27:40 -0800 Subject: [PATCH 03/19] doc: Fix documentation link --- README.md | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 7b5060f..bfd391b 100644 --- a/README.md +++ b/README.md @@ -7,7 +7,7 @@ A Machine-to-Machine interaction system for Lean 4. Pantograph provides interfaces to execute proofs, construct expressions, and examine the symbol list of a Lean project for machine learning. -See [documentations][doc/] for design rationale and references. +See [documentations](doc/) for design rationale and references. ## Installation @@ -17,7 +17,9 @@ nix build .#{sharedLib,executable} ``` to build either the shared library or executable. -Install `elan` and `lake`, and run +Install `lake` and `lean` fixed to the version of the `lean-toolchain` file, and +run + ``` sh lake build ``` @@ -26,9 +28,12 @@ This builds the executable in `.lake/build/bin/pantograph-repl`. ## Executable Usage ``` sh -pantograph MODULES|LEAN_OPTIONS +pantograph-repl MODULES|LEAN_OPTIONS ``` +The `pantograph-repl` executable must be run with a list of modules to import. +It can also accept lean options of the form `--key=value` e.g. `--pp.raw=true`. + The REPL loop accepts commands as single-line JSON inputs and outputs either an `Error:` (indicating malformed command) or a JSON return value indicating the result of a command execution. The command can be passed in one of two formats @@ -39,8 +44,6 @@ command { ... } The list of available commands can be found in `Pantograph/Protocol.lean` and below. An empty command aborts the REPL. -The `pantograph` executable must be run with a list of modules to import. It can -also accept lean options of the form `--key=value` e.g. `--pp.raw=true`. Example: (~5k symbols) ``` From a8e7a1a726c7fe5595c92e5c5b8ff4228628ab65 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 26 Nov 2024 12:34:52 -0800 Subject: [PATCH 04/19] feat: Erase macro scopes in sexp --- Pantograph/Delate.lean | 6 +++--- Test/Delate.lean | 2 +- Test/Library.lean | 2 +- Test/Proofs.lean | 6 +++--- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index be17729..141abd9 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -346,20 +346,20 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM let args := " ".intercalate args pure s!"({fn'} {args})" | .lam binderName binderType body binderInfo => do - let binderName' := ofName binderName + let binderName' := binderName.eraseMacroScopes let binderType' ← self binderType let body' ← self body let binderInfo' := binderInfoSexp binderInfo pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})" | .forallE binderName binderType body binderInfo => do - let binderName' := ofName binderName + let binderName' := binderName.eraseMacroScopes let binderType' ← self binderType let body' ← self body let binderInfo' := binderInfoSexp binderInfo pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})" | .letE name type value body _ => do -- Dependent boolean flag diacarded - let name' := serializeName name + let name' := name.eraseMacroScopes let type' ← self type let value' ← self value let body' ← self body diff --git a/Test/Delate.lean b/Test/Delate.lean index 227ab24..d918dc8 100644 --- a/Test/Delate.lean +++ b/Test/Delate.lean @@ -32,7 +32,7 @@ def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do let entries: List (String × String) := [ -- This one contains unhygienic variable names which must be suppressed - ("Nat.add", "(:forall _ (:c Nat) (:forall _ (:c Nat) (:c Nat)))"), + ("Nat.add", "(:forall a (:c Nat) (:forall a (:c Nat) (:c Nat)))"), -- These ones are normal and easy ("Nat.add_one", "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))"), ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h ((:c LE.le) (:c Nat) (:c instLENat) ((:c Nat.succ) 1) 0) ((:c LE.le) (:c Nat) (:c instLENat) 2 1)) :implicit) :implicit)"), diff --git a/Test/Library.lean b/Test/Library.lean index d995374..df1ba4d 100644 --- a/Test/Library.lean +++ b/Test/Library.lean @@ -24,7 +24,7 @@ def test_expr_echo (env: Environment): IO LSpec.TestSeq := do }, expr := { pp? := "⟨∀ (x : Prop), x → x, fun x h => h⟩", - sexp? := "((:c PSigma.mk) (:sort 0) (:lambda p (:sort 0) 0) (:forall x (:sort 0) (:forall _ 0 1)) (:lambda x (:sort 0) (:lambda h 0 0)))", + sexp? := "((:c PSigma.mk) (:sort 0) (:lambda p (:sort 0) 0) (:forall x (:sort 0) (:forall a 0 1)) (:lambda x (:sort 0) (:lambda h 0 0)))", } })) return tests diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 8e3e2a2..02c1bf6 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -282,9 +282,9 @@ def test_or_comm: TestM Unit := do serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false) let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))" let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))" - let motive := s!"(:lambda t._@._hyg.26 {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))" - let caseL := s!"(:lambda h._@._hyg.27 (:fv {fvP}) (:lambda h._@._hyg.28 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseL}) (:fv {fvP}) (:fv {fvQ}) 1)))" - let caseR := s!"(:lambda h._@._hyg.29 (:fv {fvQ}) (:lambda h._@._hyg.30 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseR}) (:fv {fvP}) (:fv {fvQ}) 1)))" + let motive := s!"(:lambda t {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))" + let caseL := s!"(:lambda h (:fv {fvP}) (:lambda h ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseL}) (:fv {fvP}) (:fv {fvQ}) 1)))" + let caseR := s!"(:lambda h (:fv {fvQ}) (:lambda h ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseR}) (:fv {fvP}) (:fv {fvQ}) 1)))" let conduit := s!"((:c Eq.refl) {orPQ} (:fv {fvH}))" addTest $ LSpec.test "(2 parent)" (state2parent == s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) {motive} (:fv {fvH}) {caseL} {caseR} {conduit})") From 44aef76a10a9638caecef46326130ffd7c9fad29 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 26 Nov 2024 12:57:19 -0800 Subject: [PATCH 05/19] refactor: Remove sanitization for mvarId/fvarId --- Pantograph/Delate.lean | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index 141abd9..4b3bd51 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -327,11 +327,11 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM -- Lean these are handled using a `#` prefix. pure s!"{deBruijnIndex}" | .fvar fvarId => - let name := ofName fvarId.name + let name := fvarId.name pure s!"(:fv {name})" | .mvar mvarId => do let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv" - let name := ofName mvarId.name + let name := mvarId.name pure s!"(:{pref} {name})" | .sort level => let level := serializeSortLevel level sanitize @@ -387,7 +387,6 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM | .implicit => " :implicit" | .strictImplicit => " :strictImplicit" | .instImplicit => " :instImplicit" - ofName (name: Name) := serializeName name sanitize def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do let pp?: Option String ← match options.printExprPretty with @@ -420,13 +419,13 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava match localDecl with | .cdecl _ fvarId userName _ _ _ => return { - name := ofName fvarId.name, + name := fvarId.name.toString, userName:= ofName userName.simpMacroScopes, isInaccessible := userName.isInaccessibleUserName } | .ldecl _ fvarId userName _ _ _ _ => do return { - name := ofName fvarId.name, + name := fvarId.name.toString, userName := toString userName.simpMacroScopes, isInaccessible := userName.isInaccessibleUserName } @@ -436,7 +435,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava let userName := userName.simpMacroScopes let type ← instantiate type return { - name := ofName fvarId.name, + name := fvarId.name.toString, userName:= ofName userName, isInaccessible := userName.isInaccessibleUserName type? := .some (← serializeExpression options type) @@ -450,7 +449,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava else pure $ .none return { - name := ofName fvarId.name, + name := fvarId.name.toString, userName:= ofName userName, isInaccessible := userName.isInaccessibleUserName type? := .some (← serializeExpression options type) @@ -469,7 +468,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava | false => ppVar localDecl return var::acc return { - name := ofName goal.name, + name := goal.name.toString, userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName), isConversion := isLHSGoal? mvarDecl.type |>.isSome, target := (← serializeExpression options (← instantiate mvarDecl.type)), From 7c9b092200ffc3365060cf7e0d6d0db1c809aeb4 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 30 Nov 2024 23:21:16 -0800 Subject: [PATCH 06/19] test: Dual monad testing stub --- Test/Common.lean | 2 ++ Test/Main.lean | 4 +++- Test/Serial.lean | 56 ++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 61 insertions(+), 1 deletion(-) create mode 100644 Test/Serial.lean diff --git a/Test/Common.lean b/Test/Common.lean index 3998293..ce21ce8 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -130,6 +130,8 @@ def addTest [Monad m] (test: LSpec.TestSeq): TestT m Unit := do def runTest [Monad m] (t: TestT m Unit): m LSpec.TestSeq := Prod.snd <$> t.run LSpec.TestSeq.done +def runTestWithResult { α } [Monad m] (t: TestT m α): m (α × LSpec.TestSeq) := + t.run LSpec.TestSeq.done def runTestTermElabM (env: Environment) (t: TestT Elab.TermElabM Unit): IO LSpec.TestSeq := diff --git a/Test/Main.lean b/Test/Main.lean index 25bb0d9..6bf410e 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -1,11 +1,12 @@ import LSpec +import Test.Delate import Test.Environment import Test.Frontend import Test.Integration import Test.Library import Test.Metavar import Test.Proofs -import Test.Delate +import Test.Serial import Test.Tactic -- Test running infrastructure @@ -51,6 +52,7 @@ def main (args: List String) := do ("Metavar", Metavar.suite env_default), ("Proofs", Proofs.suite env_default), ("Delate", Delate.suite env_default), + ("Serial", Serial.suite env_default), ("Tactic/Congruence", Tactic.Congruence.suite env_default), ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default), ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default), diff --git a/Test/Serial.lean b/Test/Serial.lean new file mode 100644 index 0000000..4cca464 --- /dev/null +++ b/Test/Serial.lean @@ -0,0 +1,56 @@ +import LSpec +import Test.Common +import Lean +import Pantograph.Library + +open Lean + +namespace Pantograph.Test.Serial + +structure MultiState where + coreContext : Core.Context + coreStates : Array Core.State + +abbrev TestM := StateRefT MultiState $ TestT $ EIO LSpec.TestSeq + +def runCoreM { α } (id : Nat) (testCoreM: TestT CoreM α) : TestM α := do + let multiState ← get + let state ← match multiState.coreStates[id]? with + | .some state => pure state + | .none => + let test := LSpec.test "Invalid index" (id < multiState.coreStates.size) + throw test + let coreM := runTestWithResult testCoreM + match ← (coreM.run' multiState.coreContext state).toBaseIO with + | .error _ => do + let test := LSpec.test "Exception" false + throw test + | .ok (a, tests) => do + set $ (← getThe LSpec.TestSeq) ++ tests + return a + +def simple : TestM Unit := do + return + +structure Test where + name : String + nInstances : Nat + routine: TestM Unit + +protected def Test.run (test: Test) (env: Lean.Environment) : IO LSpec.TestSeq := do + -- Create the state + let state : MultiState := { + coreContext := ← createCoreContext #[], + coreStates := Array.range test.nInstances |>.map λ _ => { env }, + } + match ← (runTest $ test.routine.run' state).toBaseIO with + | .ok e => return e + | .error e => return e + +def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) := + let tests: List Test := [ + { name := "simple", nInstances := 2, routine := simple } + ] + tests.map (fun test => (test.name, test.run env)) + +end Pantograph.Test.Serial From 0f946880ae87a5b746b188dcc946ee8c2cbefa8b Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 4 Dec 2024 10:44:33 -0800 Subject: [PATCH 07/19] test: Environment pickling --- Pantograph/Serial.lean | 4 +-- Repl.lean | 4 +-- Test/Common.lean | 9 +++++- Test/Serial.lean | 73 ++++++++++++++++++++++++++++++------------ 4 files changed, 64 insertions(+), 26 deletions(-) diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 2f04bdb..e60fc54 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -55,7 +55,7 @@ and when unpickling, we build a fresh `Environment` from the imports, and then add the new constants. -/ @[export pantograph_env_pickle_m] -def env_pickle (env : Environment) (path : System.FilePath) : IO Unit := +def environmentPickle (env : Environment) (path : System.FilePath) : IO Unit := Pantograph.pickle path (env.header.imports, env.constants.map₂) /-- @@ -65,7 +65,7 @@ We construct a fresh `Environment` with the relevant imports, and then replace the new constants. -/ @[export pantograph_env_unpickle_m] -def env_unpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do +def environmentUnpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do let ((imports, map₂), region) ← Pantograph.unpickle (Array Import × PHashMap Name ConstantInfo) path let env ← importModules imports {} 0 return (← env.replay (Std.HashMap.ofList map₂.toList), region) diff --git a/Repl.lean b/Repl.lean index e162f05..f0572a1 100644 --- a/Repl.lean +++ b/Repl.lean @@ -90,10 +90,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do Environment.addDecl args env_save (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do let env ← Lean.MonadEnv.getEnv - env_pickle env args.path + environmentPickle env args.path return .ok {} env_load (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do - let (env, _) ← env_unpickle args.path + let (env, _) ← environmentUnpickle args.path Lean.setEnv env return .ok {} expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do diff --git a/Test/Common.lean b/Test/Common.lean index ce21ce8..0a0b44c 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -125,9 +125,16 @@ def mvarUserNameAndType (mvarId: MVarId): MetaM (Name × String) := do abbrev TestT := StateT LSpec.TestSeq -def addTest [Monad m] (test: LSpec.TestSeq): TestT m Unit := do +def addTest [Monad m] (test: LSpec.TestSeq) : TestT m Unit := do set $ (← get) ++ test +def checkEq [Monad m] [DecidableEq α] (desc : String) (lhs rhs : α) : TestT m Unit := do + addTest $ LSpec.check desc (lhs == rhs) +def checkTrue [Monad m] (desc : String) (flag : Bool) : TestT m Unit := do + addTest $ LSpec.check desc flag +def fail [Monad m] (desc : String) : TestT m Unit := do + addTest $ LSpec.check desc false + def runTest [Monad m] (t: TestT m Unit): m LSpec.TestSeq := Prod.snd <$> t.run LSpec.TestSeq.done def runTestWithResult { α } [Monad m] (t: TestT m α): m (α × LSpec.TestSeq) := diff --git a/Test/Serial.lean b/Test/Serial.lean index 4cca464..d1ce661 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -7,30 +7,60 @@ open Lean namespace Pantograph.Test.Serial +def tempPath : IO System.FilePath := do + Prod.snd <$> IO.FS.createTempFile + structure MultiState where coreContext : Core.Context - coreStates : Array Core.State + env: Environment -abbrev TestM := StateRefT MultiState $ TestT $ EIO LSpec.TestSeq +abbrev TestM := TestT $ StateRefT MultiState $ IO -def runCoreM { α } (id : Nat) (testCoreM: TestT CoreM α) : TestM α := do - let multiState ← get - let state ← match multiState.coreStates[id]? with - | .some state => pure state - | .none => - let test := LSpec.test "Invalid index" (id < multiState.coreStates.size) - throw test +instance : MonadEnv TestM where + getEnv := return (← getThe MultiState).env + modifyEnv f := do modifyThe MultiState fun s => { s with env := f s.env } + +def runCoreM { α } (state : Core.State) (testCoreM : TestT CoreM α) : TestM (α × Core.State) := do + let multiState ← getThe MultiState let coreM := runTestWithResult testCoreM - match ← (coreM.run' multiState.coreContext state).toBaseIO with - | .error _ => do - let test := LSpec.test "Exception" false - throw test - | .ok (a, tests) => do + match ← (coreM.run multiState.coreContext state).toBaseIO with + | .error e => do + throw $ .userError $ ← e.toMessageData.toString + | .ok ((a, tests), state') => do set $ (← getThe LSpec.TestSeq) ++ tests - return a + return (a, state') -def simple : TestM Unit := do - return +def test_environment_pickling : TestM Unit := do + let stateSrc: Core.State := { env := ← getEnv } + let stateDst: Core.State := { env := ← getEnv } + + let name := `mystery + let envPicklePath ← tempPath + let ((), _) ← runCoreM stateSrc do + let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default + let value: Expr := .lam `p (.sort 0) (.lam `h (.bvar 0) (.bvar 0) .default) .default + let c := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx + (name := name) + (levelParams := []) + (type := type) + (value := value) + (hints := Lean.mkReducibilityHintsRegularEx 1) + (safety := Lean.DefinitionSafety.safe) + (all := []) + let env' ← match (← getEnv).addDecl (← getOptions) c with + | .error e => do + let error ← (e.toMessageData (← getOptions)).toString + throwError error + | .ok env' => pure env' + environmentPickle env' envPicklePath + + let _ ← runCoreM stateDst do + let (env', _) ← environmentUnpickle envPicklePath + checkTrue s!"Has symbol {name}" (env'.find? name).isSome + let anotherName := `mystery2 + checkTrue s!"Doesn't have symbol {anotherName}" (env'.find? anotherName).isNone + + IO.FS.removeFile envPicklePath structure Test where name : String @@ -41,15 +71,16 @@ protected def Test.run (test: Test) (env: Lean.Environment) : IO LSpec.TestSeq : -- Create the state let state : MultiState := { coreContext := ← createCoreContext #[], - coreStates := Array.range test.nInstances |>.map λ _ => { env }, + env, } - match ← (runTest $ test.routine.run' state).toBaseIO with + match ← ((runTest $ test.routine).run' state).toBaseIO with | .ok e => return e - | .error e => return e + | .error e => + return LSpec.check "Emitted exception" (e.toString == "") def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) := let tests: List Test := [ - { name := "simple", nInstances := 2, routine := simple } + { name := "environment_pickling", nInstances := 2, routine := test_environment_pickling }, ] tests.map (fun test => (test.name, test.run env)) From 105fb7af4bed8da4969ef1265106c239861dece9 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 14:23:55 -0800 Subject: [PATCH 08/19] feat: Goal state pickling --- Pantograph/Serial.lean | 89 ++++++++++++++++++++++++++++++++++++++++++ Test/Serial.lean | 36 +++++++++++++---- 2 files changed, 118 insertions(+), 7 deletions(-) diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index e60fc54..bd01169 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -2,6 +2,7 @@ import Lean.Environment import Lean.Replay import Init.System.IOError import Std.Data.HashMap +import Pantograph.Goal /-! Input/Output functions @@ -70,4 +71,92 @@ def environmentUnpickle (path : System.FilePath) : IO (Environment × CompactedR let env ← importModules imports {} 0 return (← env.replay (Std.HashMap.ofList map₂.toList), region) + +open Lean.Core in +structure CompactCoreState where + -- env : Environment + nextMacroScope : MacroScope := firstFrontendMacroScope + 1 + ngen : NameGenerator := {} + -- traceState : TraceState := {} + -- cache : Cache := {} + -- messages : MessageLog := {} + -- infoState : Elab.InfoState := {} + +@[export pantograph_goal_state_pickle_m] +def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit := + let { + savedState := { + term := { + meta := { + core, + meta, + } + «elab», + }, + tactic + } + root, + parentMVar?, + convMVar?, + calcPrevRhs?, + } := goalState + --let env := core.env + Pantograph.pickle path ( + ({ core with } : CompactCoreState), + meta, + «elab», + tactic, + + root, + parentMVar?, + convMVar?, + calcPrevRhs?, + ) + +@[export pantograph_goal_state_unpickle_m] +def goalStateUnpickle (path : System.FilePath) (env : Environment) + : IO (GoalState × CompactedRegion) := unsafe do + let (( + compactCore, + meta, + «elab», + tactic, + + root, + parentMVar?, + convMVar?, + calcPrevRhs?, + ), region) ← Pantograph.unpickle ( + CompactCoreState × + Meta.State × + Elab.Term.State × + Elab.Tactic.State × + + MVarId × + Option MVarId × + Option (MVarId × MVarId × List MVarId) × + Option (MVarId × Expr) + ) path + let goalState := { + savedState := { + term := { + meta := { + core := { + compactCore with + passedHeartbeats := 0, + env, + }, + meta, + }, + «elab», + }, + tactic, + }, + root, + parentMVar?, + convMVar?, + calcPrevRhs?, + } + return (goalState, region) + end Pantograph diff --git a/Test/Serial.lean b/Test/Serial.lean index d1ce661..fcdc155 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -31,12 +31,12 @@ def runCoreM { α } (state : Core.State) (testCoreM : TestT CoreM α) : TestM ( return (a, state') def test_environment_pickling : TestM Unit := do - let stateSrc: Core.State := { env := ← getEnv } - let stateDst: Core.State := { env := ← getEnv } + let coreSrc : Core.State := { env := ← getEnv } + let coreDst : Core.State := { env := ← getEnv } let name := `mystery let envPicklePath ← tempPath - let ((), _) ← runCoreM stateSrc do + let ((), _) ← runCoreM coreSrc do let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default let value: Expr := .lam `p (.sort 0) (.lam `h (.bvar 0) (.bvar 0) .default) .default let c := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx @@ -54,7 +54,7 @@ def test_environment_pickling : TestM Unit := do | .ok env' => pure env' environmentPickle env' envPicklePath - let _ ← runCoreM stateDst do + let _ ← runCoreM coreDst do let (env', _) ← environmentUnpickle envPicklePath checkTrue s!"Has symbol {name}" (env'.find? name).isSome let anotherName := `mystery2 @@ -62,9 +62,30 @@ def test_environment_pickling : TestM Unit := do IO.FS.removeFile envPicklePath +def test_goal_state_pickling_simple : TestM Unit := do + let coreSrc : Core.State := { env := ← getEnv } + let coreDst : Core.State := { env := ← getEnv } + let statePath ← tempPath + + let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default + let stateGenerate : MetaM GoalState := runTermElabMInMeta do + GoalState.create type + + let ((), _) ← runCoreM coreSrc do + let state ← stateGenerate.run' + goalStatePickle state statePath + + let ((), _) ← runCoreM coreDst do + let (goalState, _) ← goalStateUnpickle statePath (← getEnv) + let metaM : MetaM (List Expr) := do + goalState.goals.mapM λ goal => goalState.withContext goal goal.getType + let types ← metaM.run' + checkTrue "Goals" $ types[0]!.equal type + + IO.FS.removeFile statePath + structure Test where name : String - nInstances : Nat routine: TestM Unit protected def Test.run (test: Test) (env: Lean.Environment) : IO LSpec.TestSeq := do @@ -76,11 +97,12 @@ protected def Test.run (test: Test) (env: Lean.Environment) : IO LSpec.TestSeq : match ← ((runTest $ test.routine).run' state).toBaseIO with | .ok e => return e | .error e => - return LSpec.check "Emitted exception" (e.toString == "") + return LSpec.check s!"Emitted exception: {e.toString}" (e.toString == "") def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) := let tests: List Test := [ - { name := "environment_pickling", nInstances := 2, routine := test_environment_pickling }, + { name := "environment_pickling", routine := test_environment_pickling, }, + { name := "goal_state_pickling_simple", routine := test_goal_state_pickling_simple, }, ] tests.map (fun test => (test.name, test.run env)) From c54ce93ef5eb745a3db7668886f35ed034f42afb Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 14:31:43 -0800 Subject: [PATCH 09/19] feat: Goal State IO in REPL --- Pantograph/Protocol.lean | 13 +++++++++++++ Repl.lean | 36 +++++++++++++++++++++++------------- 2 files changed, 36 insertions(+), 13 deletions(-) diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index fcd5ebe..0cb6cac 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -289,6 +289,19 @@ structure GoalDiag where instantiate: Bool := true printSexp: Bool := false +structure GoalSave where + id: Nat + path: System.FilePath + deriving Lean.FromJson +structure GoalSaveResult where + deriving Lean.ToJson +structure GoalLoad where + path: System.FilePath + deriving Lean.FromJson +structure GoalLoadResult where + id: Nat + deriving Lean.ToJson + /-- Executes the Lean compiler on a single file -/ structure FrontendProcess where diff --git a/Repl.lean b/Repl.lean index f0572a1..3f8a3c6 100644 --- a/Repl.lean +++ b/Repl.lean @@ -15,6 +15,16 @@ structure State where /-- Main state monad for executing commands -/ abbrev MainM := ReaderT Context (StateT State Lean.CoreM) +def newGoalState (goalState: GoalState) : MainM Nat := do + let state ← get + let stateId := state.nextId + set { state with + goalStates := state.goalStates.insert stateId goalState, + nextId := state.nextId + 1 + } + return stateId + + -- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables -- certain monadic features in `MainM` abbrev CR α := Except Protocol.InteractionError α @@ -50,6 +60,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | "goal.continue" => run goal_continue | "goal.delete" => run goal_delete | "goal.print" => run goal_print + | "goal.save" => run goal_save + | "goal.load" => run goal_load | "frontend.process" => run frontend_process | cmd => let error: Protocol.InteractionError := @@ -62,14 +74,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do errorCommand := errorI "command" errorIndex := errorI "index" errorIO := errorI "io" - newGoalState (goalState: GoalState) : MainM Nat := do - let state ← get - let stateId := state.nextId - set { state with - goalStates := state.goalStates.insert stateId goalState, - nextId := state.nextId + 1 - } - return stateId -- Command Functions reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do let state ← get @@ -203,11 +207,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do match nextState? with | .error error => return .error <| errorI "structure" error | .ok nextGoalState => - let nextStateId := state.nextId - set { state with - goalStates := state.goalStates.insert nextStateId nextGoalState, - nextId := state.nextId + 1 - } + let nextStateId ← newGoalState nextGoalState let goals ← goalSerialize nextGoalState (options := state.options) return .ok { nextStateId, @@ -224,6 +224,16 @@ def execute (command: Protocol.Command): MainM Lean.Json := do return .error $ errorIndex s!"Invalid state index {args.stateId}" let result ← runMetaInMainM <| goalPrint goalState state.options return .ok result + goal_save (args: Protocol.GoalSave): MainM (CR Protocol.GoalSaveResult) := do + let state ← get + let .some goalState := state.goalStates[args.id]? | + return .error $ errorIndex s!"Invalid state index {args.id}" + goalStatePickle goalState args.path + return .ok {} + goal_load (args: Protocol.GoalLoad): MainM (CR Protocol.GoalLoadResult) := do + let (goalState, _) ← goalStateUnpickle args.path (← Lean.MonadEnv.getEnv) + let id ← newGoalState goalState + return .ok { id } frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do let options := (← get).options try From 3da85b7f04fda00d98222f4f988d05461cd03dc1 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 16:00:46 -0800 Subject: [PATCH 10/19] doc: Documentation for save/load --- README.md | 57 +----------------------------------------------- doc/repl.md | 63 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 64 insertions(+), 56 deletions(-) create mode 100644 doc/repl.md diff --git a/README.md b/README.md index 04213ae..5fec564 100644 --- a/README.md +++ b/README.md @@ -64,62 +64,7 @@ stat ``` where the application of `assumption` should lead to a failure. -### Commands - -See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON. -* `reset`: Delete all cached expressions and proof trees -* `stat`: Display resource usage -* `expr.echo {"expr": , "type": , ["levels": []]}`: Determine the - type of an expression and format it. -* `env.catalog`: Display a list of all safe Lean symbols in the current environment -* `env.inspect {"name": , "value": }`: Show the type and package of a - given symbol; If value flag is set, the value is printed or hidden. By default - only the values of definitions are printed. -* `options.set { key: value, ... }`: Set one or more options (not Lean options; those - have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean` - - One particular option for interest for machine learning researchers is the - automatic mode (flag: `"automaticMode"`). By default it is turned on, with - all goals automatically resuming. This makes Pantograph act like a gym, - with no resumption necessary to manage your goals. -* `options.print`: Display the current set of options -* `goal.start {["name": ], ["expr": ], ["levels": []], ["copyFrom": ]}`: - Start a new proof from a given expression or symbol -* `goal.tactic {"stateId": , "goalId": , ...}`: Execute a tactic string on a - given goal. The tactic is supplied as additional key-value pairs in one of the following formats: - - `{ "tactic": }`: Execute an ordinary tactic - - `{ "expr": }`: Assign the given proof term to the current goal - - `{ "have": , "binderName": }`: Execute `have` and creates a branch goal - - `{ "calc": }`: Execute one step of a `calc` tactic. Each step must - be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set - to the previous `rhs`. - - `{ "conv": }`: Enter or exit conversion tactic mode. In the case of - exit, the goal id is ignored. -* `goal.continue {"stateId": , ["branch": ], ["goals": ]}`: - Execute continuation/resumption - - `{ "branch": }`: Continue on branch state. The current state must have no goals. - - `{ "goals": }`: Resume the given goals -* `goal.remove {"stateIds": []}"`: Drop the goal states specified in the list -* `goal.print {"stateId": }"`: Print a goal state -* `frontend.process { ["fileName": ",] ["file": ], invocations: - , sorrys: }`: Executes the Lean frontend on a file, collecting - either the tactic invocations (`"invocations": true`) or the sorrys into goal - states (`"sorrys": true`) - -### Errors - -When an error pertaining to the execution of a command happens, the returning JSON structure is - -``` json -{ "error": "type", "desc": "description" } -``` -Common error forms: -* `command`: Indicates malformed command structure which results from either - invalid command or a malformed JSON structure that cannot be fed to an - individual command. -* `index`: Indicates an invariant maintained by the output of one command and - input of another is broken. For example, attempting to query a symbol not - existing in the library or indexing into a non-existent proof state. +For a list of commands, see [REPL Documentation](doc/repl.md). ### Project Environment diff --git a/doc/repl.md b/doc/repl.md new file mode 100644 index 0000000..a31db4f --- /dev/null +++ b/doc/repl.md @@ -0,0 +1,63 @@ +# REPL + +## Commands + +See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON. +* `reset`: Delete all cached expressions and proof trees +* `stat`: Display resource usage +* `expr.echo {"expr": , "type": , ["levels": []]}`: Determine the + type of an expression and format it. +* `env.catalog`: Display a list of all safe Lean symbols in the current environment +* `env.inspect {"name": , "value": }`: Show the type and package of a + given symbol; If value flag is set, the value is printed or hidden. By default + only the values of definitions are printed. +* `env.save { path }`, `env.load { path }`: Save/Load the current environment + to/from a file +* `options.set { key: value, ... }`: Set one or more options (not Lean options; those + have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean` + + One particular option for interest for machine learning researchers is the + automatic mode (flag: `"automaticMode"`). By default it is turned on, with + all goals automatically resuming. This makes Pantograph act like a gym, + with no resumption necessary to manage your goals. +* `options.print`: Display the current set of options +* `goal.start {["name": ], ["expr": ], ["levels": []], ["copyFrom": ]}`: + Start a new proof from a given expression or symbol +* `goal.tactic {"stateId": , "goalId": , ...}`: Execute a tactic string on a + given goal. The tactic is supplied as additional key-value pairs in one of the following formats: + - `{ "tactic": }`: Execute an ordinary tactic + - `{ "expr": }`: Assign the given proof term to the current goal + - `{ "have": , "binderName": }`: Execute `have` and creates a branch goal + - `{ "calc": }`: Execute one step of a `calc` tactic. Each step must + be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set + to the previous `rhs`. + - `{ "conv": }`: Enter or exit conversion tactic mode. In the case of + exit, the goal id is ignored. +* `goal.continue {"stateId": , ["branch": ], ["goals": ]}`: + Execute continuation/resumption + - `{ "branch": }`: Continue on branch state. The current state must have no goals. + - `{ "goals": }`: Resume the given goals +* `goal.remove {"stateIds": []}"`: Drop the goal states specified in the list +* `goal.print {"stateId": }"`: Print a goal state +* `goal.save`{ id, path }, `env.load { path }`: Save/Load a goal state to/from a + file. The environment is not carried with the state. The user is responsible + to ensure the sender/receiver instances share the same environment. +* `frontend.process { ["fileName": ",] ["file": ], invocations: + , sorrys: }`: Executes the Lean frontend on a file, collecting + either the tactic invocations (`"invocations": true`) or the sorrys into goal + states (`"sorrys": true`) + +## Errors + +When an error pertaining to the execution of a command happens, the returning JSON structure is + +``` json +{ "error": "type", "desc": "description" } +``` +Common error forms: +* `command`: Indicates malformed command structure which results from either + invalid command or a malformed JSON structure that cannot be fed to an + individual command. +* `index`: Indicates an invariant maintained by the output of one command and + input of another is broken. For example, attempting to query a symbol not + existing in the library or indexing into a non-existent proof state. From bfdc7dd39ee008506dafb010725fc192ccbe5287 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 16:02:00 -0800 Subject: [PATCH 11/19] doc: Fix code environment --- doc/repl.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/repl.md b/doc/repl.md index a31db4f..978bad2 100644 --- a/doc/repl.md +++ b/doc/repl.md @@ -39,7 +39,7 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va - `{ "goals": }`: Resume the given goals * `goal.remove {"stateIds": []}"`: Drop the goal states specified in the list * `goal.print {"stateId": }"`: Print a goal state -* `goal.save`{ id, path }, `env.load { path }`: Save/Load a goal state to/from a +* `goal.save{ id, path }`, `goal.load { path }`: Save/Load a goal state to/from a file. The environment is not carried with the state. The user is responsible to ensure the sender/receiver instances share the same environment. * `frontend.process { ["fileName": ",] ["file": ], invocations: From d00e3769430c1fe5df0c2528768738617a29efd2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 17:18:35 -0800 Subject: [PATCH 12/19] doc: Remove outdated documentation --- .gitignore | 6 ++---- README.md | 2 +- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/.gitignore b/.gitignore index 21bcd46..53ec3bb 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,4 @@ .* !.gitignore - -*.olean -/build -/lake-packages +*.[io]lean +/result diff --git a/README.md b/README.md index 5fec564..47456ea 100644 --- a/README.md +++ b/README.md @@ -75,7 +75,7 @@ the environment might be setup like this: ``` sh LIB="../lib" -LIB_MATHLIB="$LIB/mathlib4/lake-packages" +LIB_MATHLIB="$LIB/mathlib4/.lake" export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib" LEAN_PATH=$LEAN_PATH build/bin/pantograph $@ From 95408d1d523aa679b544568112da8535506d14e2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 17:21:06 -0800 Subject: [PATCH 13/19] doc: Unify types --- doc/repl.md | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/doc/repl.md b/doc/repl.md index 978bad2..464c7cc 100644 --- a/doc/repl.md +++ b/doc/repl.md @@ -11,8 +11,8 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va * `env.inspect {"name": , "value": }`: Show the type and package of a given symbol; If value flag is set, the value is printed or hidden. By default only the values of definitions are printed. -* `env.save { path }`, `env.load { path }`: Save/Load the current environment - to/from a file +* `env.save { "path": }`, `env.load { "path": }`: Save/Load the + current environment to/from a file * `options.set { key: value, ... }`: Set one or more options (not Lean options; those have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean` @@ -39,10 +39,11 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va - `{ "goals": }`: Resume the given goals * `goal.remove {"stateIds": []}"`: Drop the goal states specified in the list * `goal.print {"stateId": }"`: Print a goal state -* `goal.save{ id, path }`, `goal.load { path }`: Save/Load a goal state to/from a - file. The environment is not carried with the state. The user is responsible - to ensure the sender/receiver instances share the same environment. -* `frontend.process { ["fileName": ",] ["file": ], invocations: +* `goal.save { "id": , "path": }`, `goal.load { "path": }`: + Save/Load a goal state to/from a file. The environment is not carried with the + state. The user is responsible to ensure the sender/receiver instances share + the same environment. +* `frontend.process { ["fileName": ,] ["file": ], invocations: , sorrys: }`: Executes the Lean frontend on a file, collecting either the tactic invocations (`"invocations": true`) or the sorrys into goal states (`"sorrys": true`) From 2e2658bde79aa02c6593371e098a924488ba98bf Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 21:35:37 -0800 Subject: [PATCH 14/19] test: Add test case for composite tactic --- Test/Proofs.lean | 25 +++++++++++++++++++++---- 1 file changed, 21 insertions(+), 4 deletions(-) diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 02c1bf6..8db8f19 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -14,10 +14,7 @@ inductive Start where | copy (name: String) -- Start from some name in the environment | expr (expr: String) -- Start from some expression -abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM) - -def addTest (test: LSpec.TestSeq): TestM Unit := do - set $ (← get) ++ test +abbrev TestM := TestT $ ReaderT Protocol.Options $ Elab.TermElabM def startProof (start: Start): TestM (Option GoalState) := do let env ← Lean.MonadEnv.getEnv @@ -704,6 +701,25 @@ def test_nat_zero_add_alt: TestM Unit := do } ]) +def test_composite_tactic_failure: TestM Unit := do + let state? ← startProof (.expr "∀ (p : Prop), ∃ (x : Nat), p") + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + + let tactic := "intro p" + let state1 ← match ← state0.tacticOn 0 tactic with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + + let tactic := "exact ⟨0, by simp⟩" + let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail" + checkEq tactic messages #["placeholder"] + def suite (env: Environment): List (String × IO LSpec.TestSeq) := let tests := [ ("identity", test_identity), @@ -716,6 +732,7 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) := ("calc", test_calc), ("Nat.zero_add", test_nat_zero_add), ("Nat.zero_add alt", test_nat_zero_add_alt), + ("composite tactic failure", test_composite_tactic_failure), ] tests.map (fun (name, test) => (name, proofRunner env test)) From 7aafd6956fe71770a356f3d852edc4e91cd5696a Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 22:07:21 -0800 Subject: [PATCH 15/19] fix: Capture composite tactic failure --- Pantograph/Goal.lean | 5 +++++ Test/Common.lean | 22 ++++++++++++++-------- Test/Proofs.lean | 4 ++-- 3 files changed, 21 insertions(+), 10 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 79e3004..be745f4 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -73,6 +73,8 @@ protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): O return { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances } protected def GoalState.metaState (state: GoalState): Meta.State := state.savedState.term.meta.meta +protected def GoalState.coreState (state: GoalState): Core.SavedState := + state.savedState.term.meta.core protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do mvarId.withContext m |>.run' (← read) state.metaState @@ -207,6 +209,9 @@ protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: E Elab.TermElabM TacticResult := do try let nextState ← state.step goal tacticM + let newMessages ← (← getThe Core.State).messages.toList.drop (state.coreState.messages.toList.length) |>.mapM λ m => m.toString + if ¬ newMessages.isEmpty then + return .failure newMessages.toArray return .success nextState catch exception => return .failure #[← exception.toMessageData.toString] diff --git a/Test/Common.lean b/Test/Common.lean index 0a0b44c..212e164 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -123,23 +123,29 @@ def mvarUserNameAndType (mvarId: MVarId): MetaM (Name × String) := do -- Monadic testing -abbrev TestT := StateT LSpec.TestSeq +abbrev TestT := StateRefT' IO.RealWorld LSpec.TestSeq -def addTest [Monad m] (test: LSpec.TestSeq) : TestT m Unit := do +section Monadic + +variable [Monad m] [MonadLiftT (ST IO.RealWorld) m] + +def addTest (test: LSpec.TestSeq) : TestT m Unit := do set $ (← get) ++ test -def checkEq [Monad m] [DecidableEq α] (desc : String) (lhs rhs : α) : TestT m Unit := do - addTest $ LSpec.check desc (lhs == rhs) -def checkTrue [Monad m] (desc : String) (flag : Bool) : TestT m Unit := do +def checkEq [DecidableEq α] [Repr α] (desc : String) (lhs rhs : α) : TestT m Unit := do + addTest $ LSpec.check desc (lhs = rhs) +def checkTrue (desc : String) (flag : Bool) : TestT m Unit := do addTest $ LSpec.check desc flag -def fail [Monad m] (desc : String) : TestT m Unit := do +def fail (desc : String) : TestT m Unit := do addTest $ LSpec.check desc false -def runTest [Monad m] (t: TestT m Unit): m LSpec.TestSeq := +def runTest (t: TestT m Unit): m LSpec.TestSeq := Prod.snd <$> t.run LSpec.TestSeq.done -def runTestWithResult { α } [Monad m] (t: TestT m α): m (α × LSpec.TestSeq) := +def runTestWithResult { α } (t: TestT m α): m (α × LSpec.TestSeq) := t.run LSpec.TestSeq.done +end Monadic + def runTestTermElabM (env: Environment) (t: TestT Elab.TermElabM Unit): IO LSpec.TestSeq := runTermElabMSeq env $ runTest t diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 8db8f19..65f099f 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -702,7 +702,7 @@ def test_nat_zero_add_alt: TestM Unit := do ]) def test_composite_tactic_failure: TestM Unit := do - let state? ← startProof (.expr "∀ (p : Prop), ∃ (x : Nat), p") + let state? ← startProof (.expr "∀ (p : Nat → Prop), ∃ (x : Nat), p (0 + x + 0)") let state0 ← match state? with | .some state => pure state | .none => do @@ -718,7 +718,7 @@ def test_composite_tactic_failure: TestM Unit := do let tactic := "exact ⟨0, by simp⟩" let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail" - checkEq tactic messages #["placeholder"] + checkEq s!"{tactic} fails" messages #[s!"{← getFileName}:0:12: error: unsolved goals\np : Nat → Prop\n⊢ p 0\n"] def suite (env: Environment): List (String × IO LSpec.TestSeq) := let tests := [ From a62ac51c37ad5dde6c3e850aaaf1e9b9265ec652 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 22:11:37 -0800 Subject: [PATCH 16/19] chore: Remove all redundant filenames --- Pantograph/Goal.lean | 10 ++++------ Test/Common.lean | 6 +++--- Test/Tactic/MotivatedApply.lean | 6 +++--- Test/Tactic/NoConfuse.lean | 6 +++--- Test/Tactic/Prograde.lean | 2 +- 5 files changed, 14 insertions(+), 16 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index be745f4..8d29aa8 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -10,8 +10,6 @@ import Lean namespace Pantograph open Lean -def filename: String := "" - /-- Represents an interconnected set of metavariables, or a state in proof search -/ @@ -224,7 +222,7 @@ protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: Str (env := ← MonadEnv.getEnv) (catName := if state.isConv then `conv else `tactic) (input := tactic) - (fileName := filename) with + (fileName := ← getFileName) with | .ok stx => pure $ stx | .error error => return .parseError error state.tryTacticM goal $ Elab.Tactic.evalTactic tactic @@ -236,7 +234,7 @@ protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: Strin (env := ← MonadEnv.getEnv) (catName := `term) (input := expr) - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => return .parseError error state.tryTacticM goal $ Tactic.evalAssign expr @@ -250,7 +248,7 @@ protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: St (env := ← MonadEnv.getEnv) (catName := `term) (input := type) - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => return .parseError error state.tryTacticM goal $ Tactic.evalLet binderName.toName type @@ -337,7 +335,7 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String) (env := state.env) (catName := `term) (input := pred) - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => return .parseError error goal.checkNotAssigned `GoalState.tryCalc diff --git a/Test/Common.lean b/Test/Common.lean index 212e164..53adaa0 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -95,19 +95,19 @@ def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq) def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e -def strToTermSyntax [Monad m] [MonadEnv m] (s: String): m Syntax := do +def strToTermSyntax (s: String): CoreM Syntax := do let .ok stx := Parser.runParserCategory (env := ← MonadEnv.getEnv) (catName := `term) (input := s) - (fileName := filename) | panic! s!"Failed to parse {s}" + (fileName := ← getFileName) | panic! s!"Failed to parse {s}" return stx def parseSentence (s: String): Elab.TermElabM Expr := do let stx ← match Parser.runParserCategory (env := ← MonadEnv.getEnv) (catName := `term) (input := s) - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" Elab.Term.elabTerm (stx := stx) .none diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean index 4fb05e3..61d7d6c 100644 --- a/Test/Tactic/MotivatedApply.lean +++ b/Test/Tactic/MotivatedApply.lean @@ -28,7 +28,7 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "@Nat.brecOn") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic @@ -52,7 +52,7 @@ def test_list_brec_on : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "@List.brecOn") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic @@ -74,7 +74,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "@Nat.brecOn") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" let expr ← parseSentence expr diff --git a/Test/Tactic/NoConfuse.lean b/Test/Tactic/NoConfuse.lean index ac277e2..93f0606 100644 --- a/Test/Tactic/NoConfuse.lean +++ b/Test/Tactic/NoConfuse.lean @@ -15,7 +15,7 @@ def test_nat : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "h") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic @@ -32,7 +32,7 @@ def test_nat_fail : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "h") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic @@ -52,7 +52,7 @@ def test_list : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "h") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean index 132718a..b3347cb 100644 --- a/Test/Tactic/Prograde.lean +++ b/Test/Tactic/Prograde.lean @@ -15,7 +15,7 @@ def test_define : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "Or.inl h") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic From 34a4bf5b7321f413e12c1c1cd814d0b0e1a52e29 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 22:12:04 -0800 Subject: [PATCH 17/19] feat: Export GoalState.tryTactic --- Pantograph/Goal.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 8d29aa8..ac09109 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -215,6 +215,7 @@ protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: E return .failure #[← exception.toMessageData.toString] /-- Execute a string tactic on given state. Restores TermElabM -/ +@[export pantograph_goal_state_try_tactic_m] protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: String): Elab.TermElabM TacticResult := do state.restoreElabM From 0415baaaff3a55475cd532749c1fe9724a16fb43 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 22:16:20 -0800 Subject: [PATCH 18/19] chore: Cleanup old `TestM` --- Test/Metavar.lean | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/Test/Metavar.lean b/Test/Metavar.lean index 506e963..c6fc4f0 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -8,10 +8,7 @@ namespace Pantograph.Test.Metavar open Pantograph open Lean -abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM) - -def addTest (test: LSpec.TestSeq): TestM Unit := do - set $ (← get) ++ test +abbrev TestM := TestT $ ReaderT Protocol.Options Elab.TermElabM -- Tests that all delay assigned mvars are instantiated def test_instantiate_mvar: TestM Unit := do @@ -32,8 +29,6 @@ def test_instantiate_mvar: TestM Unit := do "((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))") return () - - def startProof (expr: String): TestM (Option GoalState) := do let env ← Lean.MonadEnv.getEnv let syn? := parseTerm env expr From 929311a0429c2fafb5533c8f44e326c6d66b4d9c Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 6 Dec 2024 00:08:20 -0800 Subject: [PATCH 19/19] fix: Only signal failure when there is error --- Pantograph/Goal.lean | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index ac09109..e190d5d 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -202,12 +202,19 @@ inductive TacticResult where -- The given action cannot be executed in the state | invalidAction (message: String) -/-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/ +/-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/ protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit): Elab.TermElabM TacticResult := do try let nextState ← state.step goal tacticM - let newMessages ← (← getThe Core.State).messages.toList.drop (state.coreState.messages.toList.length) |>.mapM λ m => m.toString + + -- Check if error messages have been generated in the core. + let newMessages ← (← Core.getMessageLog).toList.drop state.coreState.messages.toList.length + |>.filterMapM λ m => do + if m.severity == .error then + return .some $ ← m.toString + else + return .none if ¬ newMessages.isEmpty then return .failure newMessages.toArray return .success nextState @@ -357,7 +364,7 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String) throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr step}" if let some prevRhs := calcPrevRhs? then unless ← Meta.isDefEqGuarded lhs prevRhs do - throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}" -- " + throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}" -- Creates a mvar to represent the proof that the calc tactic solves the -- current branch