From 13dd11e9955dc12bf40208b22898c2942c844cce Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 5 Dec 2024 18:55:30 -0800
Subject: [PATCH 1/7] chore: Update Lean to v4.14

---
 Pantograph/Frontend/Basic.lean  |  2 +-
 Pantograph/Frontend/Elab.lean   | 15 ++++++++-------
 Test/Integration.lean           |  2 +-
 Test/Proofs.lean                | 24 ++++++++++++------------
 Test/Tactic/MotivatedApply.lean |  6 +++---
 lean-toolchain                  |  2 +-
 6 files changed, 26 insertions(+), 25 deletions(-)

diff --git a/Pantograph/Frontend/Basic.lean b/Pantograph/Frontend/Basic.lean
index 1074a94..51f3433 100644
--- a/Pantograph/Frontend/Basic.lean
+++ b/Pantograph/Frontend/Basic.lean
@@ -60,7 +60,7 @@ def processOneCommand: FrontendM (CompilationStep × Bool) := do
   let s := (← get).commandState
   let before := s.env
   let done ← Elab.Frontend.processCommand
-  let stx := (← get).commands.back
+  let stx := (← get).commands.back!
   let src := (← read).inputCtx.input.toSubstring.extract (← get).cmdPos (← get).parserState.pos
   let s' := (← get).commandState
   let after := s'.env
diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index ceecfae..57179c4 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -70,9 +70,9 @@ partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
   | .context ctx tree => tree.filter p m |>.map (.context ctx)
   | .node info children =>
     if p info then
-      [.node info (children.toList.map (filter p m)).join.toPArray']
+      [.node info (children.toList.map (filter p m)).flatten.toPArray']
     else
-      (children.toList.map (filter p m)).join
+      (children.toList.map (filter p m)).flatten
   | .hole mvar => if m mvar then [.hole mvar] else []
 
 end Lean.Elab.InfoTree
@@ -137,7 +137,8 @@ partial def findAllInfo (t : Elab.InfoTree) (context?: Option Elab.ContextInfo)
   match t with
   | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) pred
   | .node i children  =>
-      (if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred)
+      (if pred i then [(i, context?, children)] else []) ++
+        children.toList.flatMap (fun t => findAllInfo t context? pred)
   | _ => []
 
 /-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics,
@@ -155,10 +156,10 @@ def collectTactics (t : Elab.InfoTree) : List TacticInvocation :=
 
 @[export pantograph_frontend_collect_tactics_from_compilation_step_m]
 def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protocol.InvokedTactic) := do
-  let tacticInfoTrees := step.trees.bind λ tree => tree.filter λ
+  let tacticInfoTrees := step.trees.flatMap λ tree => tree.filter λ
     | info@(.ofTacticInfo _) => info.isOriginal
     | _ => false
-  let tactics := tacticInfoTrees.bind collectTactics
+  let tactics := tacticInfoTrees.flatMap collectTactics
   tactics.mapM λ invocation => do
     let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
     let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
@@ -191,7 +192,7 @@ private def collectSorrysInTree (t : Elab.InfoTree) : List InfoWithContext :=
 -- NOTE: Plural deliberately not spelled "sorries"
 @[export pantograph_frontend_collect_sorrys_m]
 def collectSorrys (step: CompilationStep) : List InfoWithContext :=
-  step.trees.bind collectSorrysInTree
+  step.trees.flatMap collectSorrysInTree
 
 
 
@@ -211,7 +212,7 @@ def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do
     | .ofTacticInfo tacticInfo => do
       MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
     | _ => panic! "Invalid info"
-  let goals := List.join (← goalsM.run {} |>.run' {})
+  let goals := List.flatten (← goalsM.run {} |>.run' {})
   let root := match goals with
     | [] => panic! "No MVars generated"
     | [g] => g
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 9fb86b7..60f011f 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -73,7 +73,7 @@ def test_tactic : Test :=
     step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
      ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
     step "goal.print" [("stateId", .num 1)]
-     ({ parent? := .some { pp? := .some "fun x => ?m.12 x" }, }: Protocol.GoalPrintResult),
+     ({ parent? := .some { pp? := .some "fun x => ?m.11" }, }: Protocol.GoalPrintResult),
     step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
      ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
   ]
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 02c1bf6..dfe3722 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -564,10 +564,10 @@ def test_nat_zero_add: TestM Unit := do
       return ()
   addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
     #[
-      buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
-      buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat",
-      buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
-      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
+      buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat → Prop" (.some "motive"),
+      buildNamedGoal "_uniq.72" [("n", "Nat")] "Nat",
+      buildNamedGoal "_uniq.73" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
+      buildNamedGoal "_uniq.74" [("n", "Nat")] "?motive ?m.72 = (n + 0 = n)" (.some "conduit")
     ])
 
   let tactic := "exact n"
@@ -650,13 +650,13 @@ def test_nat_zero_add_alt: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let major := "_uniq.68"
+  let major := "_uniq.72"
   addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
     #[
-      buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
+      buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat → Prop" (.some "motive"),
       buildNamedGoal major [("n", "Nat")] "Nat",
-      buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
-      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
+      buildNamedGoal "_uniq.73" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
+      buildNamedGoal "_uniq.74" [("n", "Nat")] "?motive ?m.72 = (n + 0 = n)" (.some "conduit")
     ])
 
   let tactic := "intro x"
@@ -673,7 +673,7 @@ def test_nat_zero_add_alt: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let (eqL, eqR, eqT) := ("_uniq.88", "_uniq.89", "_uniq.87")
+  let (eqL, eqR, eqT) := ("_uniq.92", "_uniq.93", "_uniq.91")
   addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = [eqL, eqR, eqT]
   let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict"
   let state2b ← match state3m2.resume [conduit] with
@@ -684,16 +684,16 @@ def test_nat_zero_add_alt: TestM Unit := do
 
   let cNatAdd := "(:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat))"
   let cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))"
-  let fvN := "_uniq.63"
+  let fvN := "_uniq.67"
   let conduitRight := s!"((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN}))"
   let substOf (mv: String) := s!"(:subst (:mv {mv}) (:fv {fvN}) (:mv {major}))"
   addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) =
     #[
       {
-        name := "_uniq.70",
+        name := "_uniq.74",
         userName? := .some "conduit",
         target := {
-          pp? := .some "(?m.92 ?m.68 = ?m.94 ?m.68) = (n + 0 = n)",
+          pp? := .some "(?m.96 ?m.72 = ?m.98 ?m.72) = (n + 0 = n)",
           sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) {substOf eqT} {substOf eqL} {substOf eqR}) {conduitRight})",
         },
         vars := #[{
diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean
index 4fb05e3..8c8fdad 100644
--- a/Test/Tactic/MotivatedApply.lean
+++ b/Test/Tactic/MotivatedApply.lean
@@ -40,7 +40,7 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do
         "Nat → Prop",
         "Nat",
         "∀ (t : Nat), Nat.below t → ?motive t",
-        "?motive ?m.67 = (n + 0 = n)",
+        "?motive ?m.71 = (n + 0 = n)",
       ])
     addTest test
 
@@ -83,7 +83,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
     let tactic := Tactic.evalMotivatedApply recursor
     let newGoals ← runTacticOnMVar tactic target.mvarId!
-    let majorId := 67
+    let majorId := 71
     addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
       [
         "Nat → Prop",
@@ -100,7 +100,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
 
     addTest $ ← conduit.withContext do
       let t := toString (← Meta.ppExpr $ ← conduit.getType)
-      return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.138 ?m.{majorId}) = (n + 0 = n)")
+      return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.146 ?m.{majorId}) = (n + 0 = n)")
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
diff --git a/lean-toolchain b/lean-toolchain
index 8998520..1e70935 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.12.0
+leanprover/lean4:v4.14.0

From fb3d36584fe7f5155669ab3227fc5213b8f3c3e6 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 5 Dec 2024 18:59:14 -0800
Subject: [PATCH 2/7] chore: Add formatter, update lean4-nix

---
 flake.lock |   7 ++-
 flake.nix  | 157 ++++++++++++++++++++++++++++-------------------------
 2 files changed, 87 insertions(+), 77 deletions(-)

diff --git a/flake.lock b/flake.lock
index f40dde9..9f54bbe 100644
--- a/flake.lock
+++ b/flake.lock
@@ -42,15 +42,16 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1731711316,
-        "narHash": "sha256-s5u+A2/Ea9gPveB5wwVM5dWW0NST6kamDsTeovGuLEs=",
+        "lastModified": 1733351931,
+        "narHash": "sha256-ngMjY/ci6490G2gofaS9CODtpnmFoYzfaI13U14TkFM=",
         "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "136fc6057c48de970579e960b62421e9c295b67d",
+        "rev": "157c85903f668fadeb79f330961b7bbe5ee596de",
         "type": "github"
       },
       "original": {
         "owner": "lenianiva",
+        "ref": "157c85903f668fadeb79f330961b7bbe5ee596de",
         "repo": "lean4-nix",
         "type": "github"
       }
diff --git a/flake.nix b/flake.nix
index 91901d8..d8ce698 100644
--- a/flake.nix
+++ b/flake.nix
@@ -4,7 +4,7 @@
   inputs = {
     nixpkgs.url = "github:nixos/nixpkgs/nixos-24.05";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean4-nix.url = "github:lenianiva/lean4-nix";
+    lean4-nix.url = "github:lenianiva/lean4-nix?ref=157c85903f668fadeb79f330961b7bbe5ee596de";
     lspec = {
       url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab";
       flake = false;
@@ -18,80 +18,89 @@
     lean4-nix,
     lspec,
     ...
-  } : flake-parts.lib.mkFlake { inherit inputs; } {
-    flake = {
-    };
-    systems = [
-      "x86_64-linux"
-      "x86_64-darwin"
-    ];
-    perSystem = { system, pkgs, ... }: let
-      pkgs = import nixpkgs {
-        inherit system;
-        overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ];
+  }:
+    flake-parts.lib.mkFlake {inherit inputs;} {
+      flake = {
       };
-      lspecLib = pkgs.lean.buildLeanPackage {
-        name = "LSpec";
-        roots = [ "Main" "LSpec" ];
-        src = "${lspec}";
-      };
-      project = pkgs.lean.buildLeanPackage {
-        name = "Pantograph";
-        roots = [ "Pantograph" ];
-        src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
-          src = ./.;
-          filter = path: type:
-            !(pkgs.lib.hasInfix "/Test/" path) &&
-            !(pkgs.lib.hasSuffix ".md" path) &&
-            !(pkgs.lib.hasSuffix "Repl.lean" path);
-        });
-      };
-      repl = pkgs.lean.buildLeanPackage {
-        name = "Repl";
-        roots = [ "Main" "Repl" ];
-        deps = [ project ];
-        src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
-          src = ./.;
-          filter = path: type:
-            !(pkgs.lib.hasInfix "/Test/" path) &&
-            !(pkgs.lib.hasSuffix ".md" path);
-        });
-      };
-      test = pkgs.lean.buildLeanPackage {
-        name = "Test";
-        # NOTE: The src directory must be ./. since that is where the import
-        # root begins (e.g. `import Test.Environment` and not `import
-        # Environment`) and thats where `lakefile.lean` resides.
-        roots = [ "Test.Main" ];
-        deps = [ lspecLib repl ];
-        src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
-          src = ./.;
-          filter = path: type:
-            !(pkgs.lib.hasInfix "Pantograph" path);
-        });
-      };
-    in rec {
-      packages = {
-        inherit (pkgs.lean) lean lean-all;
-        inherit (project) sharedLib iTree;
-        inherit (repl) executable;
-        default = repl.executable;
-      };
-      legacyPackages = {
-        inherit project;
-        leanPkgs = pkgs.lean;
-      };
-      checks = {
-        test = pkgs.runCommand "test" {
-          buildInputs = [ test.executable pkgs.lean.lean-all ];
-        } ''
-          #export LEAN_SRC_PATH="${./.}"
-          ${test.executable}/bin/test > $out
-        '';
-      };
-      devShells.default = pkgs.mkShell {
-        buildInputs = [ pkgs.lean.lean-all pkgs.lean.lean ];
+      systems = [
+        "aarch64-linux"
+        "aarch64-darwin"
+        "x86_64-linux"
+        "x86_64-darwin"
+      ];
+      perSystem = {
+        system,
+        pkgs,
+        ...
+      }: let
+        pkgs = import nixpkgs {
+          inherit system;
+          overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
+        };
+        lspecLib = pkgs.lean.buildLeanPackage {
+          name = "LSpec";
+          roots = ["Main" "LSpec"];
+          src = "${lspec}";
+        };
+        project = pkgs.lean.buildLeanPackage {
+          name = "Pantograph";
+          roots = ["Pantograph"];
+          src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
+            src = ./.;
+            filter = path: type:
+              !(pkgs.lib.hasInfix "/Test/" path)
+              && !(pkgs.lib.hasSuffix ".md" path)
+              && !(pkgs.lib.hasSuffix "Repl.lean" path);
+          });
+        };
+        repl = pkgs.lean.buildLeanPackage {
+          name = "Repl";
+          roots = ["Main" "Repl"];
+          deps = [project];
+          src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
+            src = ./.;
+            filter = path: type:
+              !(pkgs.lib.hasInfix "/Test/" path)
+              && !(pkgs.lib.hasSuffix ".md" path);
+          });
+        };
+        test = pkgs.lean.buildLeanPackage {
+          name = "Test";
+          # NOTE: The src directory must be ./. since that is where the import
+          # root begins (e.g. `import Test.Environment` and not `import
+          # Environment`) and thats where `lakefile.lean` resides.
+          roots = ["Test.Main"];
+          deps = [lspecLib repl];
+          src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
+            src = ./.;
+            filter = path: type:
+              !(pkgs.lib.hasInfix "Pantograph" path);
+          });
+        };
+      in rec {
+        packages = {
+          inherit (pkgs.lean) lean lean-all;
+          inherit (project) sharedLib iTree;
+          inherit (repl) executable;
+          default = repl.executable;
+        };
+        formatter = pkgs.alejandra;
+        legacyPackages = {
+          inherit project;
+          leanPkgs = pkgs.lean;
+        };
+        checks = {
+          test =
+            pkgs.runCommand "test" {
+              buildInputs = [test.executable pkgs.lean.lean-all];
+            } ''
+              #export LEAN_SRC_PATH="${./.}"
+              ${test.executable}/bin/test > $out
+            '';
+        };
+        devShells.default = pkgs.mkShell {
+          buildInputs = [pkgs.lean.lean-all pkgs.lean.lean];
+        };
       };
     };
-  };
 }

From 6302b747b86fbfa9e9802c50535b102178cb49ec Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 7 Jan 2025 17:51:32 -0800
Subject: [PATCH 3/7] feat: Improve error message clarity

---
 Pantograph/Goal.lean | 31 ++++++++++++++++++++-----------
 Test/Proofs.lean     | 27 +++++++++++++++------------
 2 files changed, 35 insertions(+), 23 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 6ff14d2..3dff60a 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -237,25 +237,34 @@ inductive TacticResult where
   -- The given action cannot be executed in the state
   | invalidAction (message: String)
 
+private def dumpMessageLog (prevMessageLength : Nat) : CoreM (Array String) := do
+  let newMessages ← (← Core.getMessageLog).toList.drop prevMessageLength
+    |>.filterMapM λ m => do
+      if m.severity == .error then
+        return .some $ ← m.toString
+      else
+        return .none
+  Core.resetMessageLog
+  return newMessages.toArray
+
 /-- 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) (guardMVarErrors : Bool := false):
-      Elab.TermElabM TacticResult := do
+protected def GoalState.tryTacticM
+    (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
+    (guardMVarErrors : Bool := false)
+    : Elab.TermElabM TacticResult := do
+  let prevMessageLength := state.coreState.messages.toList.length
   try
     let nextState ← state.step goal tacticM guardMVarErrors
 
     -- 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
-    Core.resetMessageLog
+    let newMessages ← dumpMessageLog prevMessageLength
     if ¬ newMessages.isEmpty then
-      return .failure newMessages.toArray
+      return .failure newMessages
     return .success nextState
   catch exception =>
-    return .failure #[← exception.toMessageData.toString]
+    match exception with
+    | .internal _ => return .failure $ ← dumpMessageLog prevMessageLength
+    | _ => return .failure #[← exception.toMessageData.toString]
 
 /-- Execute a string tactic on given state. Restores TermElabM -/
 @[export pantograph_goal_state_try_tactic_m]
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index a4a916b..a179b74 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -720,7 +720,6 @@ def test_tactic_failure_unresolved_goals : TestM Unit := do
   let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail"
   checkEq s!"{tactic} fails" messages #[s!"{← getFileName}:0:12: error: unsolved goals\np : Nat → Prop\n⊢ p 0\n"]
 
-
 def test_tactic_failure_synthesize_placeholder : TestM Unit := do
   let state? ← startProof (.expr "∀ (p q r : Prop) (h : p → q), q ∧ r")
   let state0 ← match state? with
@@ -736,20 +735,24 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
 
+  let iex : InternalExceptionId := { idx := 4 }
+  IO.println s!"{← iex.getName}"
   let tactic := "simpa [h] using And.imp_left h _"
-  let state2 ← match ← state1.tacticOn 0 tactic with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
+  --let state2 ← match ← state1.tacticOn 0 tactic with
+  --  | .success state => pure state
+  --  | other => do
+  --    addTest $ assertUnreachable $ other.toString
+  --    return ()
 
-  checkEq tactic ((← state2.serializeGoals).map (·.devolatilize))  #[
-    buildGoal [("p", "Prop"), ("q", "Prop"), ("r", "Prop"), ("h", "p → q")] "p ∧ r"
-  ]
+  -- Volatile behaviour. This easily changes across Lean versions
 
-  --let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail"
-  --let message := s!"<Pantograph>:0:31: error: don't know how to synthesize placeholder\ncontext:\np q r : Prop\nh : p → q\n⊢ p ∧ r\n"
-  --checkEq s!"{tactic} fails" messages #[message]
+  --checkEq tactic ((← state2.serializeGoals).map (·.devolatilize))  #[
+  --  buildGoal [("p", "Prop"), ("q", "Prop"), ("r", "Prop"), ("h", "p → q")] "p ∧ r"
+  --]
+
+  let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail"
+  let message := s!"<Pantograph>:0:31: error: don't know how to synthesize placeholder\ncontext:\np q r : Prop\nh : p → q\n⊢ p ∧ r\n"
+  checkEq s!"{tactic} fails" messages #[message]
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [

From f89196036246590131ce66019a9aad664db9b508 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 7 Jan 2025 17:52:28 -0800
Subject: [PATCH 4/7] fix: Volatile test

---
 Test/Integration.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Test/Integration.lean b/Test/Integration.lean
index 77968f0..098b7fc 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -73,7 +73,7 @@ def test_tactic : Test :=
     step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
      ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
     step "goal.print" [("stateId", .num 1), ("parentExpr", .bool true), ("rootExpr", .bool true)]
-     ({ parent? := .some { pp? := .some "fun x => ?m.12 x" }, }: Protocol.GoalPrintResult),
+     ({ parent? := .some { pp? := .some "fun x => ?m.11" }, }: Protocol.GoalPrintResult),
     step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
      ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
   ]

From 5e61282660c72397d478b66eddee60add989679f Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 13 Jan 2025 10:30:26 -0800
Subject: [PATCH 5/7] test: Source location extraction

---
 Test/Environment.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Test/Environment.lean b/Test/Environment.lean
index af98c10..b646279 100644
--- a/Test/Environment.lean
+++ b/Test/Environment.lean
@@ -106,8 +106,8 @@ def test_symbol_location : TestT IO Unit := do
     let .ok result ← Environment.inspect { name := "Nat.le_of_succ_le", source? := .some true } (options := {}) | fail "Inspect failed"
     checkEq "module" result.module? <| .some "Init.Data.Nat.Basic"
 
-    -- Doesn't work for symbols in `Init` for some reason
-    --checkEq "file" result.sourceUri? <| .some "??"
+    -- Extraction of source doesn't work for symbols in `Init` for some reason
+    checkTrue "file" result.sourceUri?.isNone
     checkEq "pos" (result.sourceStart?.map (·.column)) <| .some 0
     checkEq "pos" (result.sourceEnd?.map (·.column)) <| .some 88
 

From 06fdf7e678c1ce2e7a2bb5fe26962c6d89715e22 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 13 Jan 2025 11:09:55 -0800
Subject: [PATCH 6/7] chore: Update Lean to v4.15.0

---
 Pantograph/Frontend/InfoTree.lean |  4 ++++
 Pantograph/Tactic/Prograde.lean   |  2 +-
 flake.lock                        |  7 +++----
 flake.nix                         | 20 +++++---------------
 lean-toolchain                    |  2 +-
 5 files changed, 14 insertions(+), 21 deletions(-)

diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean
index b170ee6..a38775c 100644
--- a/Pantograph/Frontend/InfoTree.lean
+++ b/Pantograph/Frontend/InfoTree.lean
@@ -26,6 +26,8 @@ protected def Info.stx? : Info → Option Syntax
   | .ofFVarAliasInfo      _    => none
   | .ofFieldRedeclInfo    info => info.stx
   | .ofOmissionInfo       info => info.stx
+  | .ofChoiceInfo         info => info.stx
+  | .ofPartialTermInfo    info => info.stx
 /-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
 protected def Info.isOriginal (i : Info) : Bool :=
   match i.stx? with
@@ -141,6 +143,8 @@ partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .
       | .ofFVarAliasInfo _ => pure "[fvar]"
       | .ofFieldRedeclInfo _ => pure "[field_redecl]"
       | .ofOmissionInfo _ => pure "[omission]"
+      | .ofChoiceInfo _ => pure "[choice]"
+      | .ofPartialTermInfo  _ => pure "[partial_term]"
       let children := "\n".intercalate (← children.toList.mapM λ t' => do pure $ indent $ ← t'.toString ctx)
       return s!"{node}\n{children}"
     else throw <| IO.userError "No `ContextInfo` available."
diff --git a/Pantograph/Tactic/Prograde.lean b/Pantograph/Tactic/Prograde.lean
index 0b4719f..c0cdcc1 100644
--- a/Pantograph/Tactic/Prograde.lean
+++ b/Pantograph/Tactic/Prograde.lean
@@ -40,7 +40,7 @@ def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResul
   let fvarId ← mkFreshFVarId
   let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
   let mvarUpstream ←
-    withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
+    Meta.withLCtx lctxUpstream #[] do
       Meta.withNewLocalInstances #[.fvar fvarId] 0 do
         let mvarUpstream ← mkUpstreamMVar mvarId
         --let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
diff --git a/flake.lock b/flake.lock
index 9f54bbe..4a17f3d 100644
--- a/flake.lock
+++ b/flake.lock
@@ -42,16 +42,15 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1733351931,
-        "narHash": "sha256-ngMjY/ci6490G2gofaS9CODtpnmFoYzfaI13U14TkFM=",
+        "lastModified": 1736388194,
+        "narHash": "sha256-ymSrd/A8Pw+9FzbxUbR7CkFHLJK1b4SnFFWg/1e0JeE=",
         "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "157c85903f668fadeb79f330961b7bbe5ee596de",
+        "rev": "90f496bc0694fb97bdfa6adedfc2dc2c841a4cf2",
         "type": "github"
       },
       "original": {
         "owner": "lenianiva",
-        "ref": "157c85903f668fadeb79f330961b7bbe5ee596de",
         "repo": "lean4-nix",
         "type": "github"
       }
diff --git a/flake.nix b/flake.nix
index 1dfc515..af6e4fb 100644
--- a/flake.nix
+++ b/flake.nix
@@ -4,7 +4,7 @@
   inputs = {
     nixpkgs.url = "github:nixos/nixpkgs/nixos-24.05";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean4-nix.url = "github:lenianiva/lean4-nix?ref=157c85903f668fadeb79f330961b7bbe5ee596de";
+    lean4-nix.url = "github:lenianiva/lean4-nix";
     lspec = {
       url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab";
       flake = false;
@@ -18,19 +18,9 @@
     lean4-nix,
     lspec,
     ...
-  } : flake-parts.lib.mkFlake { inherit inputs; } {
-    flake = {
-    };
-    systems = [
-      "aarch64-linux"
-      "aarch64-darwin"
-      "x86_64-linux"
-      "x86_64-darwin"
-    ];
-    perSystem = { system, pkgs, ... }: let
-      pkgs = import nixpkgs {
-        inherit system;
-        overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ];
+  }:
+    flake-parts.lib.mkFlake {inherit inputs;} {
+      flake = {
       };
       systems = [
         "aarch64-linux"
@@ -94,7 +84,6 @@
           inherit (repl) executable;
           default = repl.executable;
         };
-        formatter = pkgs.alejandra;
         legacyPackages = {
           inherit project;
           leanPkgs = pkgs.lean;
@@ -108,6 +97,7 @@
               ${test.executable}/bin/test > $out
             '';
         };
+        formatter = pkgs.alejandra;
         devShells.default = pkgs.mkShell {
           buildInputs = [pkgs.lean.lean-all pkgs.lean.lean];
         };
diff --git a/lean-toolchain b/lean-toolchain
index 1e70935..d0eb99f 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.14.0
+leanprover/lean4:v4.15.0

From 60e78b322eacb6a3bfefff1a527ede2e9cc1ed1c Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 13 Jan 2025 12:28:16 -0800
Subject: [PATCH 7/7] fix: Test failures

---
 Test/Common.lean                |  6 ++++
 Test/Integration.lean           | 12 +++----
 Test/Metavar.lean               |  4 +--
 Test/Proofs.lean                | 61 ++++++++++++++++++++-------------
 Test/Tactic/Congruence.lean     |  6 ++--
 Test/Tactic/MotivatedApply.lean |  6 ++--
 6 files changed, 58 insertions(+), 37 deletions(-)

diff --git a/Test/Common.lean b/Test/Common.lean
index 3cad256..5274bad 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -48,6 +48,12 @@ namespace Condensed
 deriving instance BEq, Repr for LocalDecl
 deriving instance BEq, Repr for Goal
 
+-- Enable string interpolation
+instance : ToString FVarId where
+  toString id := id.name.toString
+instance : ToString MVarId where
+  toString id := id.name.toString
+
 protected def LocalDecl.devolatilize (decl: LocalDecl): LocalDecl :=
   {
     decl with fvarId := { name := .anonymous }
diff --git a/Test/Integration.lean b/Test/Integration.lean
index dce7e65..7864515 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -90,27 +90,27 @@ def test_automatic_mode (automatic: Bool): Test :=
     ],
   }
   let goal2l: Protocol.Goal := {
-    name := "_uniq.59",
+    name := "_uniq.61",
     userName? := .some "inl",
     target := { pp? := .some "q ∨ p" },
     vars := varsPQ ++ #[
-      { name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
+      { name := "_uniq.49", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
     ],
   }
   let goal2r: Protocol.Goal := {
-    name := "_uniq.72",
+    name := "_uniq.74",
     userName? := .some "inr",
     target := { pp? := .some "q ∨ p" },
     vars := varsPQ ++ #[
-      { name := "_uniq.60", userName := "h✝", type? := .some { pp? := .some "q" }, isInaccessible := true}
+      { name := "_uniq.62", userName := "h✝", type? := .some { pp? := .some "q" }, isInaccessible := true}
     ],
   }
   let goal3l: Protocol.Goal := {
-    name := "_uniq.78",
+    name := "_uniq.80",
     userName? := .some "inl.h",
     target := { pp? := .some "p" },
     vars := varsPQ ++ #[
-      { name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
+      { name := "_uniq.49", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
     ],
   }
   [
diff --git a/Test/Metavar.lean b/Test/Metavar.lean
index c6fc4f0..276004b 100644
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@@ -239,7 +239,7 @@ def test_partial_continuation: TestM Unit := do
       return ()
     | .ok state => pure state
   addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
+    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
   addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
 
   -- Roundtrip
@@ -253,7 +253,7 @@ def test_partial_continuation: TestM Unit := do
       return ()
     | .ok state => pure state
   addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
+    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
   addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
 
   -- Continuation should fail if the state does not exist:
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index d7722e2..e13e528 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -241,13 +241,15 @@ def test_or_comm: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let fvP := "_uniq.10"
-  let fvQ := "_uniq.13"
-  let fvH := "_uniq.16"
-  let state1g0 := "_uniq.17"
+  let [state1g0] := state1.goals | fail "Should have 1 goal"
+  let (fvP, fvQ, fvH) ← state1.withContext state1g0 do
+    let lctx ← getLCtx
+    let #[fvP, fvQ, fvH] := lctx.getFVarIds.map (toString ·.name) |
+      panic! "Incorrect number of decls"
+    pure (fvP, fvQ, fvH)
   addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)) =
     #[{
-      name := state1g0,
+      name := state1g0.name.toString,
       target := { pp? := .some "q ∨ p" },
       vars := #[
         { name := fvP, userName := "p", type? := .some { pp? := .some "Prop" } },
@@ -269,7 +271,9 @@ def test_or_comm: TestM Unit := do
       return ()
   addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
     #[branchGoal "inl" "p", branchGoal "inr" "q"])
-  let (caseL, caseR) := ("_uniq.64", "_uniq.77")
+  let [state2g0, state2g1] := state2.goals |
+    fail s!"Should have 2 goals, but it has {state2.goals.length}"
+  let (caseL, caseR) := (state2g0.name.toString, state2g1.name.toString)
   addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) =
     #[caseL, caseR])
   addTest $ LSpec.check "(2 parent exists)" state2.parentExpr?.isSome
@@ -293,7 +297,8 @@ def test_or_comm: TestM Unit := do
       return ()
   let state3_1parent ← state3_1.withParentContext do
     serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!)
-  addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv _uniq.91))")
+  let [state3_1goal0] := state3_1.goals | fail "Should have 1 goal"
+  addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv {state3_1goal0}))")
   addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
   let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
     | .success state => pure state
@@ -559,12 +564,15 @@ def test_nat_zero_add: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
+  let [mvarMotive, mvarMajor, mvarInduct, mvarConduit] := state2.goals |
+      fail "Incorrect number of goals"
+  let .num _ major := mvarMajor.name | fail "Incorrect form of mvar id"
   addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
     #[
-      buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat → Prop" (.some "motive"),
-      buildNamedGoal "_uniq.72" [("n", "Nat")] "Nat",
-      buildNamedGoal "_uniq.73" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
-      buildNamedGoal "_uniq.74" [("n", "Nat")] "?motive ?m.72 = (n + 0 = n)" (.some "conduit")
+      buildNamedGoal mvarMotive.name.toString  [("n", "Nat")] "Nat → Prop" (.some "motive"),
+      buildNamedGoal mvarMajor.name.toString   [("n", "Nat")] "Nat",
+      buildNamedGoal mvarInduct.name.toString  [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
+      buildNamedGoal mvarConduit.name.toString [("n", "Nat")] s!"?motive ?m.{major} = (n + 0 = n)" (.some "conduit")
     ])
 
   let tactic := "exact n"
@@ -647,13 +655,15 @@ def test_nat_zero_add_alt: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let major := "_uniq.72"
+  let [mvarMotive, mvarMajor, mvarInduct, mvarConduit] := state2.goals |
+      fail "Incorrect number of goals"
+  let .num _ major := mvarMajor.name | fail "Incorrect form of mvar id"
   addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
     #[
-      buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat → Prop" (.some "motive"),
-      buildNamedGoal major [("n", "Nat")] "Nat",
-      buildNamedGoal "_uniq.73" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
-      buildNamedGoal "_uniq.74" [("n", "Nat")] "?motive ?m.72 = (n + 0 = n)" (.some "conduit")
+      buildNamedGoal mvarMotive.name.toString [("n", "Nat")] "Nat → Prop" (.some "motive"),
+      buildNamedGoal mvarMajor.name.toString [("n", "Nat")] "Nat",
+      buildNamedGoal mvarInduct.name.toString [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
+      buildNamedGoal mvarConduit.name.toString [("n", "Nat")] s!"?motive ?m.{major} = (n + 0 = n)" (.some "conduit")
     ])
 
   let tactic := "intro x"
@@ -670,8 +680,7 @@ def test_nat_zero_add_alt: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let (eqL, eqR, eqT) := ("_uniq.92", "_uniq.93", "_uniq.91")
-  addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = [eqL, eqR, eqT]
+  let [eqL, eqR, eqT] := state3m2.goals | fail "Incorrect number of goals"
   let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict"
   let state2b ← match state3m2.resume [conduit] with
     | .ok state => pure state
@@ -681,20 +690,26 @@ def test_nat_zero_add_alt: TestM Unit := do
 
   let cNatAdd := "(:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat))"
   let cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))"
-  let fvN := "_uniq.67"
+  let fvN ← state2b.withContext conduit do
+    let lctx ← getLCtx
+    pure $ lctx.getFVarIds.get! 0 |>.name
   let conduitRight := s!"((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN}))"
-  let substOf (mv: String) := s!"(:subst (:mv {mv}) (:fv {fvN}) (:mv {major}))"
+  let substOf (mvarId: MVarId) := s!"(:subst (:mv {mvarId.name}) (:fv {fvN}) (:mv {mvarMajor}))"
+  let .num _ nL := eqL.name | fail "Incorrect form of mvar id"
+  let .num _ nR := eqR.name | fail "Incorrect form of mvar id"
+  let nL' := nL + 4
+  let nR' := nR + 5
   addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) =
     #[
       {
-        name := "_uniq.74",
+        name := mvarConduit.name.toString,
         userName? := .some "conduit",
         target := {
-          pp? := .some "(?m.96 ?m.72 = ?m.98 ?m.72) = (n + 0 = n)",
+          pp? := .some s!"(?m.{nL'} ?m.{major} = ?m.{nR'} ?m.{major}) = (n + 0 = n)",
           sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) {substOf eqT} {substOf eqL} {substOf eqR}) {conduitRight})",
         },
         vars := #[{
-          name := fvN,
+          name := fvN.toString,
           userName := "n",
           type? := .some { pp? := .some "Nat", sexp? := .some "(:c Nat)" },
         }],
diff --git a/Test/Tactic/Congruence.lean b/Test/Tactic/Congruence.lean
index 180c2f4..e861b2f 100644
--- a/Test/Tactic/Congruence.lean
+++ b/Test/Tactic/Congruence.lean
@@ -28,7 +28,7 @@ def test_congr_arg_list : TestT Elab.TermElabM Unit := do
     let results ← Meta.withAssignableSyntheticOpaque do f.apply (← parseSentence "List.reverse")
     addTest $ LSpec.check "apply" (results.length = 0)
     addTest $ LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂")
-    addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)")
+    addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(List.reverse ?a₁ = List.reverse ?a₂) = (l1.reverse = l2.reverse)")
 def test_congr_arg : TestT Elab.TermElabM Unit := do
   let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m"
   let expr ← parseSentence expr
@@ -37,7 +37,7 @@ def test_congr_arg : TestT Elab.TermElabM Unit := do
     let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
     addTest $  LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
       [
-        (`α, "Sort ?u.70"),
+        (`α, "Sort ?u.73"),
         (`a₁, "?α"),
         (`a₂, "?α"),
         (`f, "?α → Nat"),
@@ -52,7 +52,7 @@ def test_congr_fun : TestT Elab.TermElabM Unit := do
     let newGoals ← runTacticOnMVar Tactic.evalCongruenceFun target.mvarId!
     addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
       [
-        (`α, "Sort ?u.159"),
+        (`α, "Sort ?u.165"),
         (`f₁, "?α → Nat"),
         (`f₂, "?α → Nat"),
         (`h, "?f₁ = ?f₂"),
diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean
index 66bb336..2da643e 100644
--- a/Test/Tactic/MotivatedApply.lean
+++ b/Test/Tactic/MotivatedApply.lean
@@ -40,7 +40,7 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do
         "Nat → Prop",
         "Nat",
         "∀ (t : Nat), Nat.below t → ?motive t",
-        "?motive ?m.71 = (n + 0 = n)",
+        "?motive ?m.74 = (n + 0 = n)",
       ])
     addTest test
 
@@ -83,7 +83,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
     let tactic := Tactic.evalMotivatedApply recursor
     let newGoals ← runTacticOnMVar tactic target.mvarId!
-    let majorId := 71
+    let majorId := 74
     addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
       [
         "Nat → Prop",
@@ -100,7 +100,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
 
     addTest $ ← conduit.withContext do
       let t := toString (← Meta.ppExpr $ ← conduit.getType)
-      return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.146 ?m.{majorId}) = (n + 0 = n)")
+      return LSpec.check "conduit" (t = s!"(Nat.add ?m.{majorId} + 0 = ?m.149 ?m.{majorId}) = (n + 0 = n)")
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [