Merge branch 'dev' into frontend/refactor

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 => ((),
+  modifyThe Core.State ({ · with nextMacroScope, ngen })
-    { st 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,34 +475,29 @@ 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
+    let newMessages ← dumpMessageLog
-    if hasError then
+    let hasErrors := newMessages.any (·.severity == .error)
+    if hasErrors then
       return .failure newMessages.toArray
     else
       return .success state newMessages.toArray
   catch exception =>
-    match exception with
+    let messages ← dumpMessageLog
-    | .internal _ =>
-      let (_, messages) ← dumpMessageLog
-      return .failure messages.toArray
-    | _ =>
-      let (_, messages) ← dumpMessageLog
     let message := {
       fileName := ← getFileName,
       pos := ← getRefPosition,

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

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
+  let .failure #[_head, message] ← state1.tacticOn 0 tactic
-    | addTest $ assertUnreachable s!"{tactic} should fail"
+    | 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"
 

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

flake.lock

@@ -5,11 +5,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1749398372,
+        "lastModified": 1751413152,
-        "narHash": "sha256-tYBdgS56eXYaWVW3fsnPQ/nFlgWi/Z2Ymhyu21zVM98=",
+        "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,
+        "lastModified": 1751390929,
-        "narHash": "sha256-KFFTVbciXUaHgeGN1yiaUtY88OLGU0gElXx5SfICDKg=",
+        "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,
+        "lastModified": 1751159883,
-        "narHash": "sha256-rQaysilft1aVMwF14xIdGS3sj1yHlI6oKQNBRTF40cc=",
+        "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,
+        "lastModified": 1751943650,
-        "narHash": "sha256-MYbotu4UjWpTsq01wglhN5xDRfZYLFtNk7SBY0BcjkU=",
+        "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"
       }

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 = {

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