15 changed files with 198 additions and 154 deletions
--- a/Pantograph/Frontend/Basic.lean
+++ b/Pantograph/Frontend/Basic.lean
@ -67,7 +67,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
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@ -80,10 +80,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
@ -138,7 +138,7 @@ private def collectSorrysInTree (t : Elab.InfoTree) (options : GoalCollectionOpt
@[export pantograph_frontend_collect_sorrys_m]
 def collectSorrys (step: CompilationStep) (options : GoalCollectionOptions := {})
    : IO (List InfoWithContext) := do
-  return (← step.trees.mapM $ λ tree => collectSorrysInTree tree options).join
+  return (← step.trees.mapM $ λ tree => collectSorrysInTree tree options).flatten

 structure AnnotatedGoalState where
  state : GoalState
@ -167,7 +167,7 @@ def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState
      let range := stxByteRange tacticInfo.stx
      return mvarIds.map (·, range)
    | _ => panic! "Invalid info"
-  let annotatedGoals := List.join (← goalsM.run {} |>.run' {})
+  let annotatedGoals := List.flatten (← goalsM.run {} |>.run' {})
  let goals := annotatedGoals.map Prod.fst
  let srcBoundaries := annotatedGoals.map Prod.snd
  let root := match goals with
--- 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
@ -87,9 +89,9 @@ partial def InfoTree.filter (p : Info → Bool) (m : MVarId → Bool := fun _ =>
  | .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 []

 /-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
@ -103,7 +105,7 @@ partial def InfoTree.findAllInfo
  | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) haltOnMatch pred
  | .node i children  =>
    let head := if pred i then [(i, context?, children)] else []
-    let tail := if haltOnMatch ∧ !head.isEmpty then [] else children.toList.bind (fun t => findAllInfo t context? haltOnMatch pred)
+    let tail := if haltOnMatch ∧ !head.isEmpty then [] else children.toList.flatMap (fun t => findAllInfo t context? haltOnMatch pred)
    head ++ tail
  | _ => []

@ -119,7 +121,7 @@ partial def InfoTree.findAllInfoM [Monad m]
    let (flagCollect, flagRecurse) ← pred i context?
    let head := if flagCollect then [(i, context?, children)] else []
    let tail := if ¬ flagRecurse then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? pred)
-    return head ++ (← tail).join
+    return head ++ (← tail).flatten
  | _ => return []

@[export pantograph_infotree_to_string_m]
@ -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."
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@ -238,25 +238,34 @@ inductive TacticResult where
  -- The given action cannot be executed in the state
  | invalidAction (message: String)

-/-- 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
-  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
+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
+  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 ← 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]
--- 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
--- 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 }
--- a/Test/Environment.lean
+++ b/Test/Environment.lean
@ -106,10 +106,10 @@ 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 "??"
-    checkEq "pos" result.sourceStart? <| .some { line := 344, column := 0 }
-    checkEq "pos" result.sourceEnd? <| .some { line := 344, column := 88 }
+    -- 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

 def suite: List (String × IO LSpec.TestSeq) :=
  [
--- 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),
  ]
@ -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}
    ],
  }
  [
--- 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:
--- 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.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 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.68"
+  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.67" [("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 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.88", "_uniq.89", "_uniq.87")
-  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.63"
+  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.70",
+        name := mvarConduit.name.toString,
        userName? := .some "conduit",
        target := {
-          pp? := .some "(?m.92 ?m.68 = ?m.94 ?m.68) = (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)" },
        }],
@ -720,7 +735,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 +750,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) :=
--- 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₂"),
--- 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.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 := 67
+    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.138 ?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) :=
  [
--- a/flake.lock
+++ b/flake.lock
@ -42,11 +42,11 @@
        "nixpkgs": "nixpkgs"
      },
      "locked": {
-        "lastModified": 1731711316,
-        "narHash": "sha256-s5u+A2/Ea9gPveB5wwVM5dWW0NST6kamDsTeovGuLEs=",
+        "lastModified": 1736388194,
+        "narHash": "sha256-ymSrd/A8Pw+9FzbxUbR7CkFHLJK1b4SnFFWg/1e0JeE=",
        "owner": "lenianiva",
        "repo": "lean4-nix",
-        "rev": "136fc6057c48de970579e960b62421e9c295b67d",
+        "rev": "90f496bc0694fb97bdfa6adedfc2dc2c841a4cf2",
        "type": "github"
      },
      "original": {
--- a/flake.nix
+++ b/flake.nix
@ -18,7 +18,8 @@
    lean4-nix,
    lspec,
    ...
-  } : flake-parts.lib.mkFlake { inherit inputs; } {
+  }:
+    flake-parts.lib.mkFlake {inherit inputs;} {
      flake = {
      };
      systems = [
@ -27,36 +28,40 @@
        "x86_64-linux"
        "x86_64-darwin"
      ];
-    perSystem = { system, pkgs, ... }: let
+      perSystem = {
+        system,
+        pkgs,
+        ...
+      }: let
        pkgs = import nixpkgs {
          inherit system;
-        overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ];
+          overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
        };
        lspecLib = pkgs.lean.buildLeanPackage {
          name = "LSpec";
-        roots = [ "Main" "LSpec" ];
+          roots = ["Main" "LSpec"];
          src = "${lspec}";
        };
        project = pkgs.lean.buildLeanPackage {
          name = "Pantograph";
-        roots = [ "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);
+              !(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 ];
+          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);
+              !(pkgs.lib.hasInfix "/Test/" path)
+              && !(pkgs.lib.hasSuffix ".md" path);
          });
        };
        test = pkgs.lean.buildLeanPackage {
@ -64,8 +69,8 @@
          # 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 ];
+          roots = ["Test.Main"];
+          deps = [lspecLib repl];
          src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
            src = ./.;
            filter = path: type:
@ -84,15 +89,17 @@
          leanPkgs = pkgs.lean;
        };
        checks = {
-        test = pkgs.runCommand "test" {
-          buildInputs = [ test.executable pkgs.lean.lean-all ];
+          test =
+            pkgs.runCommand "test" {
+              buildInputs = [test.executable pkgs.lean.lean-all];
            } ''
              #export LEAN_SRC_PATH="${./.}"
              ${test.executable}/bin/test > $out
            '';
        };
+        formatter = pkgs.alejandra;
        devShells.default = pkgs.mkShell {
-        buildInputs = [ pkgs.lean.lean-all pkgs.lean.lean ];
+          buildInputs = [pkgs.lean.lean-all pkgs.lean.lean];
        };
      };
    };
--- a/2
+++ b/2
@ -1 +1 @@
-leanprover/lean4:v4.12.0
+leanprover/lean4:v4.15.0