diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 0642ac9..0f552e2 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -6,7 +6,6 @@ All the functions starting with `try` resume their inner monadic state. import Pantograph.Tactic import Lean - namespace Pantograph open Lean @@ -141,8 +140,7 @@ protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n] private def restoreCoreMExtra (state : Core.SavedState) : CoreM Unit := let { nextMacroScope, ngen, .. } := state - modifyGetThe Core.State (fun st => ((), - { st with nextMacroScope, ngen })) + modifyThe Core.State ({ · with nextMacroScope, ngen }) -- Restore the name generator and macro scopes of the core state protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit := restoreCoreMExtra state.coreState @@ -152,9 +150,6 @@ protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit := do protected def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit := do state.restoreCoreMExtra state.savedState.term.restore -private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tactic.TacticM Unit := do - state.restoreElabM - Elab.Tactic.setGoals [goal] /-- Brings into scope a list of goals. User must ensure `goals` are distinct. @@ -469,7 +464,7 @@ protected def GoalState.step (state : GoalState) (site : Site) (tacticM : Elab.T : Elab.TermElabM GoalState := Prod.snd <$> GoalState.step' state site tacticM guardMVarErrors -/-- Response for executing a tactic -/ +/-- Result for executing a tactic, capturing errors in the process -/ inductive TacticResult where -- Goes to next state | success (state : GoalState) (messages : Array Message) @@ -480,40 +475,35 @@ inductive TacticResult where -- The given action cannot be executed in the state | invalidAction (message : String) -private def dumpMessageLog (prevMessageLength : Nat := 0) : CoreM (Bool × List Message) := do +private def dumpMessageLog (prevMessageLength : Nat := 0) : CoreM (List Message) := do let newMessages := (← Core.getMessageLog).toList.drop prevMessageLength - let hasErrors := newMessages.any (·.severity == .error) Core.resetMessageLog - return (hasErrors, newMessages) + return newMessages /-- Execute a `TermElabM` producing a goal state, capturing the error and turn it into a `TacticResult` -/ def withCapturingError (elabM : Elab.Term.TermElabM GoalState) : Elab.TermElabM TacticResult := do let messageLog ← Core.getMessageLog unless messageLog.toList.isEmpty do IO.eprintln s!"{← messageLog.toList.mapM (·.toString)}" - assert! messageLog.toList.isEmpty + throwError "Message log must be empty at the beginning." try let state ← elabM -- Check if error messages have been generated in the core. - let (hasError, newMessages) ← dumpMessageLog - if hasError then + let newMessages ← dumpMessageLog + let hasErrors := newMessages.any (·.severity == .error) + if hasErrors then return .failure newMessages.toArray else return .success state newMessages.toArray catch exception => - match exception with - | .internal _ => - let (_, messages) ← dumpMessageLog - return .failure messages.toArray - | _ => - let (_, messages) ← dumpMessageLog - let message := { - fileName := ← getFileName, - pos := ← getRefPosition, - data := exception.toMessageData, - } - return .failure (message :: messages).toArray + let messages ← dumpMessageLog + let message := { + fileName := ← getFileName, + pos := ← getRefPosition, + data := exception.toMessageData, + } + return .failure (message :: messages).toArray /-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/ protected def GoalState.tryTacticM diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 086fe92..a003e8d 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -257,13 +257,16 @@ structure GoalTactic where autoResume?: Option Bool := .none -- One of the fields here must be filled tactic?: Option String := .none - mode?: Option String := .none -- Changes the current category to {"tactic", "calc", "conv"} + -- Changes the current category to {"tactic", "calc", "conv"} + mode?: Option String := .none + -- Assigns an expression to the current goal expr?: Option String := .none have?: Option String := .none let?: Option String := .none draft?: Option String := .none - -- In case of the `have` tactic, the new free variable name is provided here + -- In case of the `have` and `let` tactics, the new free variable name is + -- provided here binderName?: Option String := .none deriving Lean.FromJson diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 2df2594..2442243 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -352,8 +352,8 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do -- buildGoal [("p", "Prop"), ("q", "Prop"), ("r", "Prop"), ("h", "p → q")] "p ∧ r" --] - let .failure #[message] ← state1.tacticOn 0 tactic - | addTest $ assertUnreachable s!"{tactic} should fail" + let .failure #[_head, message] ← state1.tacticOn 0 tactic + | addTest $ assertUnreachable s!"{tactic} should fail with 2 messages" checkEq s!"{tactic} fails" (← message.toString) s!"{← getFileName}:0:31: error: don't know how to synthesize placeholder\ncontext:\np q r : Prop\nh : p → q\n⊢ p ∧ r\n" diff --git a/Tomograph.lean b/Tomograph.lean index 9847d49..469ee53 100644 --- a/Tomograph.lean +++ b/Tomograph.lean @@ -14,14 +14,14 @@ def dissect (args : List String) : IO UInt32 := do let fileName :: _args := args | fail s!"Must supply a file name" let file ← IO.FS.readFile fileName let (context, state) ← do Frontend.createContextStateFromFile file fileName (env? := .none) {} - let frontendM: Elab.Frontend.FrontendM _ := + let frontendM: Frontend.FrontendM _ := Frontend.mapCompilationSteps λ step => do IO.println s!"🐈 {step.stx.getKind.toString}" for (tree, i) in step.trees.zipIdx do IO.println s!"🌲[{i}] {← tree.toString}" for (msg, i) in step.msgs.zipIdx do IO.println s!"🔈[{i}] {← msg.toString}" - let (_, _) ← frontendM.run context |>.run state + let (_, _) ← frontendM.run {} |>.run context |>.run state return 0 end Pantograph diff --git a/flake.lock b/flake.lock index 7b8b772..0a9364c 100644 --- a/flake.lock +++ b/flake.lock @@ -5,11 +5,11 @@ "nixpkgs-lib": "nixpkgs-lib" }, "locked": { - "lastModified": 1749398372, - "narHash": "sha256-tYBdgS56eXYaWVW3fsnPQ/nFlgWi/Z2Ymhyu21zVM98=", + "lastModified": 1751413152, + "narHash": "sha256-Tyw1RjYEsp5scoigs1384gIg6e0GoBVjms4aXFfRssQ=", "owner": "hercules-ci", "repo": "flake-parts", - "rev": "9305fe4e5c2a6fcf5ba6a3ff155720fbe4076569", + "rev": "77826244401ea9de6e3bac47c2db46005e1f30b5", "type": "github" }, "original": { @@ -42,11 +42,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1750369222, - "narHash": "sha256-KFFTVbciXUaHgeGN1yiaUtY88OLGU0gElXx5SfICDKg=", + "lastModified": 1751390929, + "narHash": "sha256-Wl2miy8PhNF6ue3R1ssQbsVK3foJ37tYtznNq/i14YM=", "owner": "lenianiva", "repo": "lean4-nix", - "rev": "015ecd25206734d582a1b15dd11eb10be35ca555", + "rev": "68a07e4af5e2e56276056b172e046a2276d21aee", "type": "github" }, "original": { @@ -73,11 +73,11 @@ }, "nixpkgs-lib": { "locked": { - "lastModified": 1748740939, - "narHash": "sha256-rQaysilft1aVMwF14xIdGS3sj1yHlI6oKQNBRTF40cc=", + "lastModified": 1751159883, + "narHash": "sha256-urW/Ylk9FIfvXfliA1ywh75yszAbiTEVgpPeinFyVZo=", "owner": "nix-community", "repo": "nixpkgs.lib", - "rev": "656a64127e9d791a334452c6b6606d17539476e2", + "rev": "14a40a1d7fb9afa4739275ac642ed7301a9ba1ab", "type": "github" }, "original": { @@ -100,16 +100,16 @@ }, "nixpkgs_2": { "locked": { - "lastModified": 1751048012, - "narHash": "sha256-MYbotu4UjWpTsq01wglhN5xDRfZYLFtNk7SBY0BcjkU=", + "lastModified": 1751943650, + "narHash": "sha256-7orTnNqkGGru8Je6Un6mq1T8YVVU/O5kyW4+f9C1mZQ=", "owner": "nixos", "repo": "nixpkgs", - "rev": "a684c58d46ebbede49f280b653b9e56100aa3877", + "rev": "88983d4b665fb491861005137ce2b11a9f89f203", "type": "github" }, "original": { "owner": "nixos", - "ref": "nixos-24.11", + "ref": "nixos-25.05", "repo": "nixpkgs", "type": "github" } diff --git a/flake.nix b/flake.nix index 808c2bf..713a4cb 100644 --- a/flake.nix +++ b/flake.nix @@ -2,7 +2,7 @@ description = "Pantograph"; inputs = { - nixpkgs.url = "github:nixos/nixpkgs/nixos-24.11"; + nixpkgs.url = "github:nixos/nixpkgs/nixos-25.05"; flake-parts.url = "github:hercules-ci/flake-parts"; lean4-nix.url = "github:lenianiva/lean4-nix"; }; @@ -45,10 +45,6 @@ ./Pantograph.lean (fileFilter (file: file.hasExt "lean") ./Pantograph) ]; - set-repl = unions [ - ./Main.lean - ./Repl.lean - ]; set-test = unions [ (fileFilter (file: file.hasExt "lean") ./Test) ]; @@ -62,14 +58,22 @@ root = src; fileset = unions [ set-project - set-repl + ./Main.lean + ./Repl.lean + ]; + }; + src-tomograph = toSource { + root = src; + fileset = unions [ + set-project + ./Tomograph.lean ]; }; src-test = toSource { root = src; fileset = unions [ set-project - set-repl + ./Repl.lean set-test ]; }; @@ -84,6 +88,12 @@ deps = [project]; src = src-repl; }; + tomograph = pkgs.lean.buildLeanPackage { + name = "tomograph"; + roots = ["Tomograph"]; + deps = [project]; + src = src-tomograph; + }; test = pkgs.lean.buildLeanPackage { name = "Test"; # NOTE: The src directory must be ./. since that is where the import @@ -98,6 +108,7 @@ inherit (pkgs.lean) lean lean-all; inherit (project) sharedLib iTree; inherit (repl) executable; + tomograph = tomograph.executable; default = repl.executable; }; legacyPackages = { diff --git a/lakefile.lean b/lakefile.lean index 194fbfc..8ab791f 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -18,7 +18,6 @@ lean_exe repl { supportInterpreter := true } -@[default_target] lean_exe tomograph { root := `Tomograph -- Solves the native symbol not found problem