From 1cebf9877b2a546611d5e93d5787618b3fb578c0 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Wed, 10 Dec 2025 19:51:56 -0800 Subject: [PATCH 1/2] chore: backtick identifiers in elaborator tactic messages --- src/Init/Data/Random.lean | 2 +- src/Lean/Elab/Deriving/Repr.lean | 2 +- src/Lean/Elab/Tactic/Change.lean | 2 +- src/Lean/Elab/Tactic/Conv/Congr.lean | 14 +++++++------- src/Lean/Elab/Tactic/Conv/Pattern.lean | 4 ++-- src/Lean/Elab/Tactic/Doc.lean | 2 +- src/Lean/Elab/Tactic/ElabTerm.lean | 2 +- src/Lean/Elab/Tactic/Induction.lean | 12 ++++++------ src/Lean/Elab/Tactic/Lets.lean | 6 +++--- src/Lean/Elab/Tactic/Omega/Frontend.lean | 2 +- src/Lean/Elab/Tactic/Show.lean | 4 ++-- src/Lean/Elab/Tactic/Try.lean | 2 +- 12 files changed, 27 insertions(+), 27 deletions(-) diff --git a/src/Init/Data/Random.lean b/src/Init/Data/Random.lean index f134aa64f918..c5162475faec 100644 --- a/src/Init/Data/Random.lean +++ b/src/Init/Data/Random.lean @@ -27,7 +27,7 @@ class RandomGen (g : Type u) where and a new generator. -/ next : g → Nat × g /-- - The 'split' operation allows one to obtain two distinct random number + The `split` operation allows one to obtain two distinct random number generators. This is very useful in functional programs (for example, when passing a random number generator down to recursive calls). -/ split : g → g × g diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean index dabb23f02e5d..529080653214 100644 --- a/src/Lean/Elab/Deriving/Repr.lean +++ b/src/Lean/Elab/Deriving/Repr.lean @@ -31,7 +31,7 @@ def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM Term : forallTelescopeReducing ctorVal.type fun xs _ => do let mut fields ← `(Format.nil) if xs.size != numParams + fieldNames.size then - throwError "'deriving Repr' failed, unexpected number of fields in structure" + throwError "`deriving Repr` failed, unexpected number of fields in structure" for h : i in *...fieldNames.size do let fieldName := fieldNames[i] let fieldNameLit := Syntax.mkStrLit (toString fieldName) diff --git a/src/Lean/Elab/Tactic/Change.lean b/src/Lean/Elab/Tactic/Change.lean index 07722437f8c3..b4d20a19fb52 100644 --- a/src/Lean/Elab/Tactic/Change.lean +++ b/src/Lean/Elab/Tactic/Change.lean @@ -79,7 +79,7 @@ the main goal. -/ let (tgt', mvars) ← withCollectingNewGoalsFrom (elabChange (← getMainTarget) newType) (← getMainTag) `change liftMetaTactic fun mvarId => do return (← mvarId.replaceTargetDefEq tgt') :: mvars) - (failed := fun _ => throwError "'change' tactic failed") + (failed := fun _ => throwError "`change` tactic failed") | _ => throwUnsupportedSyntax end Lean.Elab.Tactic diff --git a/src/Lean/Elab/Tactic/Conv/Congr.lean b/src/Lean/Elab/Tactic/Conv/Congr.lean index a5fa1888f30f..7099af3a6895 100644 --- a/src/Lean/Elab/Tactic/Conv/Congr.lean +++ b/src/Lean/Elab/Tactic/Conv/Congr.lean @@ -33,7 +33,7 @@ private partial def mkCongrThm (origTag : Name) (f : Expr) (args : Array Expr) ( MetaM (Expr × Array (Option MVarId) × Array (Option MVarId)) := do let funInfo ← getFunInfoNArgs f args.size let some congrThm ← mkCongrSimpCore? f funInfo (← getCongrSimpKinds f funInfo) (subsingletonInstImplicitRhs := false) - | throwError "'congr' conv tactic failed to create congruence theorem" + | throwError "`congr` conv tactic failed to create congruence theorem" let mut eNew := f let mut proof := congrThm.proof let mut mvarIdsNew := #[] @@ -68,7 +68,7 @@ private partial def mkCongrThm (origTag : Name) (f : Expr) (args : Array Expr) ( | .heq | .fixedNoParam => unreachable! if congrThm.argKinds.size < args.size then if congrThm.argKinds.size == 0 then - throwError "'congr' conv tactic failed to create congruence theorem" + throwError "`congr` conv tactic failed to create congruence theorem" let (proof', mvarIdsNew', mvarIdsNewInsts') ← mkCongrThm origTag eNew args[funInfo.getArity...*] addImplicitArgs nameSubgoals for arg in args[funInfo.getArity...*] do @@ -100,7 +100,7 @@ def congr (mvarId : MVarId) (addImplicitArgs := false) (nameSubgoals := true) : mvarId.assign proof return mvarIdsNew.toList ++ mvarIdsNewInsts.toList else - throwError "invalid 'congr' conv tactic, application or implication expected{indentExpr lhs}" + throwError "invalid `congr` conv tactic, application or implication expected{indentExpr lhs}" @[builtin_tactic Lean.Parser.Tactic.Conv.congr] def evalCongr : Tactic := fun _ => do replaceMainGoal <| List.filterMap id (← congr (← getMainGoal)) @@ -110,7 +110,7 @@ def congrFunN (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do let (lhs, rhs) ← getLhsRhsCore mvarId let lhs := (← instantiateMVars lhs).cleanupAnnotations unless lhs.isApp do - throwError "invalid 'arg 0' conv tactic, application expected{indentExpr lhs}" + throwError "invalid `arg 0` conv tactic, application expected{indentExpr lhs}" lhs.withApp fun f xs => do let (g, mvarNew) ← mkConvGoalFor f mvarId.assign (← xs.foldlM (init := mvarNew) Meta.mkCongrFun) @@ -250,7 +250,7 @@ def evalArg (tacticName : String) (i : Int) (explicit : Bool) : TacticM Unit := let (lhs, rhs) ← getLhsRhsCore mvarId let lhs := (← instantiateMVars lhs).cleanupAnnotations let .app f a := lhs - | throwError "invalid 'fun' conv tactic, application expected{indentExpr lhs}" + | throwError "invalid `fun` conv tactic, application expected{indentExpr lhs}" let (g, mvarNew) ← mkConvGoalFor f mvarId.assign (← Meta.mkCongrFun mvarNew a) resolveRhs "fun" rhs (.app g a) @@ -307,8 +307,8 @@ private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId : else let lhsType ← whnfD (← inferType lhs) unless lhsType.isForall do - throwError "invalid 'ext' conv tactic, function or arrow expected{indentD m!"{lhs} : {lhsType}"}" - let [mvarId] ← mvarId.apply (← mkConstWithFreshMVarLevels ``funext) | throwError "'apply funext' unexpected result" + throwError "invalid `ext` conv tactic, function or arrow expected{indentD m!"{lhs} : {lhsType}"}" + let [mvarId] ← mvarId.apply (← mkConstWithFreshMVarLevels ``funext) | throwError "`apply funext` unexpected result" let userNames := if let some userName := userName? then [userName] else [] let (_, mvarId) ← mvarId.introN 1 userNames markAsConvGoal mvarId diff --git a/src/Lean/Elab/Tactic/Conv/Pattern.lean b/src/Lean/Elab/Tactic/Conv/Pattern.lean index 9483e23ed39e..2758e2764339 100644 --- a/src/Lean/Elab/Tactic/Conv/Pattern.lean +++ b/src/Lean/Elab/Tactic/Conv/Pattern.lean @@ -132,11 +132,11 @@ private def pre (pattern : AbstractMVarsResult) (state : IO.Ref PatternMatchStat let (result, _) ← Simp.main lhs ctx (methods := { pre := pre patternA state }) let subgoals ← match ← state.get with | .all #[] | .occs _ 0 _ => - throwError "'pattern' conv tactic failed, pattern was not found{indentExpr patternA.expr}" + throwError "`pattern` conv tactic failed, pattern was not found{indentExpr patternA.expr}" | .all subgoals => pure subgoals | .occs subgoals idx remaining => if let some (i, _) := remaining.getLast? then - throwError "'pattern' conv tactic failed, pattern was found only {idx} times but {i+1} expected" + throwError "`pattern` conv tactic failed, pattern was found only {idx} times but {i+1} expected" pure <| (subgoals.qsort (·.1 < ·.1)).map (·.2) (← getRhs).mvarId!.assign result.expr (← getMainGoal).assign (← result.getProof) diff --git a/src/Lean/Elab/Tactic/Doc.lean b/src/Lean/Elab/Tactic/Doc.lean index 426b8574370f..3a3e51176fb1 100644 --- a/src/Lean/Elab/Tactic/Doc.lean +++ b/src/Lean/Elab/Tactic/Doc.lean @@ -35,7 +35,7 @@ open Lean.Parser.Command | `(«register_tactic_tag»|$[$doc:docComment]? register_tactic_tag $tag:ident $user:str) => do let docstring ← doc.mapM getDocStringText modifyEnv (knownTacticTagExt.addEntry · (tag.getId, user.getString, docstring)) - | _ => throwError "Malformed 'register_tactic_tag' command" + | _ => throwError "Malformed `register_tactic_tag` command" /-- Gets the first string token in a parser description. For example, for a declaration like diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index e652f3318443..8aab8a34c934 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/src/Lean/Elab/Tactic/ElabTerm.lean @@ -242,7 +242,7 @@ def refineCore (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool) : Ta let mvarId ← mvarId.tryClear h.fvarId! replaceMainGoal (mvarIds' ++ [mvarId]) else - throwError "'specialize' requires a term of the form `h x_1 .. x_n` where `h` appears in the local context" + throwError "`specialize` requires a term of the form `h x_1 .. x_n` where `h` appears in the local context" | _ => throwUnsupportedSyntax /-- diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index a82191b06213..e66fc7f9604a 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -18,8 +18,8 @@ public section register_builtin_option tactic.customEliminators : Bool := { defValue := true - descr := "enable using custom eliminators in the 'induction' and 'cases' tactics \ - defined using the '@[induction_eliminator]' and '@[cases_eliminator]' attributes" + descr := "enable using custom eliminators in the `induction` and `cases` tactics \ + defined using the `@[induction_eliminator]` and `@[cases_eliminator]` attributes" } end @@ -1005,11 +1005,11 @@ def evalInduction : Tactic := fun stx => register_builtin_option tactic.fun_induction.unfolding : Bool := { defValue := true - descr := "if set to 'true', then 'fun_induction' and 'fun_cases' will use the “unfolding \ - functional induction (resp. cases) principle” ('….induct_unfolding'/'….fun_cases_unfolding'), \ + descr := "if set to `true`, then `fun_induction` and `fun_cases` will use the \"unfolding \ + functional induction (resp. cases) principle\" (`….induct_unfolding`/`….fun_cases_unfolding`), \ which will attempt to replace the function goal of interest in the goal with the appropriate \ - right-hand-side in each case. If 'false', the regular “functional induction principle” \ - ('….induct'/'….fun_cases') is used." + right-hand-side in each case. If `false`, the regular \"functional induction principle\" \ + (`….induct`/`….fun_cases`) is used." } /-- diff --git a/src/Lean/Elab/Tactic/Lets.lean b/src/Lean/Elab/Tactic/Lets.lean index 23d1744d45eb..b4fe009bc0db 100644 --- a/src/Lean/Elab/Tactic/Lets.lean +++ b/src/Lean/Elab/Tactic/Lets.lean @@ -55,7 +55,7 @@ declare_config_elab elabExtractLetsConfig ExtractLetsConfig let ((fvars, _), mvarId) ← mvarId.extractLets givenNames config return (fvars, [mvarId]) extractLetsAddVarInfo ids fvars) - (failed := fun _ => throwError "'extract_lets' tactic failed") + (failed := fun _ => throwError "`extract_lets` tactic failed") | _ => throwUnsupportedSyntax /-! @@ -70,7 +70,7 @@ declare_config_elab elabLiftLetsConfig LiftLetsConfig withLocation (expandOptLocation (Lean.mkOptionalNode loc?)) (atLocal := fun h => liftMetaTactic1 fun mvarId => mvarId.liftLetsLocalDecl h config) (atTarget := liftMetaTactic1 fun mvarId => mvarId.liftLets config) - (failed := fun _ => throwError "'lift_lets' tactic failed") + (failed := fun _ => throwError "`lift_lets` tactic failed") | _ => throwUnsupportedSyntax /-! @@ -82,7 +82,7 @@ declare_config_elab elabLiftLetsConfig LiftLetsConfig withLocation (expandOptLocation (Lean.mkOptionalNode loc?)) (atLocal := fun h => liftMetaTactic1 fun mvarId => mvarId.letToHaveLocalDecl h) (atTarget := liftMetaTactic1 fun mvarId => mvarId.letToHave) - (failed := fun _ => throwError "'let_to_have' tactic failed") + (failed := fun _ => throwError "`let_to_have` tactic failed") | _ => throwUnsupportedSyntax end Lean.Elab.Tactic diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean index 77641e15e326..91b95e828463 100644 --- a/src/Lean/Elab/Tactic/Omega/Frontend.lean +++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean @@ -248,7 +248,7 @@ where let (lc, prf, facts) ← asLinearCombo rhs let prf' : OmegaM Expr := do mkEqTrans rw (← prf) pure (lc, prf', facts) - | none => panic! "Invalid rewrite rule in 'asLinearCombo'" + | none => panic! "Invalid rewrite rule in `asLinearCombo`" handleNatCast (e i n : Expr) : OmegaM (LinearCombo × OmegaM Expr × List Expr) := do match n with | .fvar h => diff --git a/src/Lean/Elab/Tactic/Show.lean b/src/Lean/Elab/Tactic/Show.lean index 14ee4b24b81c..47dd3f012152 100644 --- a/src/Lean/Elab/Tactic/Show.lean +++ b/src/Lean/Elab/Tactic/Show.lean @@ -55,11 +55,11 @@ where setGoals newGoals simpleError (p tgt : Expr) : MetaM MessageData := do return m!"\ - 'show' tactic failed, pattern{indentExpr p}\n\ + `show` tactic failed, pattern{indentExpr p}\n\ is not definitionally equal to target{indentExpr tgt}" manyError (p tgt : Expr) : MetaM MessageData := do return m!"\ - 'show' tactic failed, no goals unify with the given pattern.\n\ + `show` tactic failed, no goals unify with the given pattern.\n\ \n\ In the first goal, the pattern{indentExpr p}\n\ is not definitionally equal to the target{indentExpr tgt}\n\ diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean index 950b81577aa5..055125f12152 100644 --- a/src/Lean/Elab/Tactic/Try.lean +++ b/src/Lean/Elab/Tactic/Try.lean @@ -273,7 +273,7 @@ builtin_initialize registerBuiltinAttribute { let prio ← match stx with | `(attr| try_suggestion $n:num) => pure n.getNat | `(attr| try_suggestion) => pure 1000 -- Default priority - | _ => throwError "invalid 'try_suggestion' attribute syntax" + | _ => throwError "invalid `try_suggestion` attribute syntax" let attrKind := if kind == AttributeKind.local then AttributeKind.local else AttributeKind.global trySuggestionExtension.add { name := declName, From e26082092ea8691e783e355636fe30084a8a1e4a Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Thu, 1 Jan 2026 14:12:46 -0800 Subject: [PATCH 2/2] chore: update expected output for backtick changes MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 --- tests/lean/conv1.lean.expected.out | 12 ++++++------ tests/lean/run/showTactic.lean | 4 ++-- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/tests/lean/conv1.lean.expected.out b/tests/lean/conv1.lean.expected.out index d35b5c483e36..44ecd3e14f60 100644 --- a/tests/lean/conv1.lean.expected.out +++ b/tests/lean/conv1.lean.expected.out @@ -160,10 +160,10 @@ x y z : Nat x y z : Nat | y + z -conv1.lean:248:58-248:83: error: 'pattern' conv tactic failed, pattern was found only 4 times but 5 expected -conv1.lean:249:58-249:85: error: 'pattern' conv tactic failed, pattern was found only 4 times but 5 expected -conv1.lean:250:58-250:85: error: 'pattern' conv tactic failed, pattern was found only 3 times but 5 expected -conv1.lean:251:58-251:87: error: 'pattern' conv tactic failed, pattern was found only 2 times but 5 expected +conv1.lean:248:58-248:83: error: `pattern` conv tactic failed, pattern was found only 4 times but 5 expected +conv1.lean:249:58-249:85: error: `pattern` conv tactic failed, pattern was found only 4 times but 5 expected +conv1.lean:250:58-250:85: error: `pattern` conv tactic failed, pattern was found only 3 times but 5 expected +conv1.lean:251:58-251:87: error: `pattern` conv tactic failed, pattern was found only 2 times but 5 expected P Q : Nat → Nat → Nat → Prop h : P = Q h2 : Q 1 2 3 @@ -180,7 +180,7 @@ P Q : Nat → Nat → Nat → Prop h : P = Q h2 : Q 1 2 3 | P -conv1.lean:275:10-275:13: error: invalid 'fun' conv tactic, application expected +conv1.lean:275:10-275:13: error: invalid `fun` conv tactic, application expected p P Q : Nat → Nat → Nat → Prop h : P = Q @@ -190,5 +190,5 @@ P Q : Nat → Nat → Nat → Prop h : P = Q h2 : Q 1 2 3 | P -conv1.lean:287:10-287:15: error: invalid 'arg 0' conv tactic, application expected +conv1.lean:287:10-287:15: error: invalid `arg 0` conv tactic, application expected p diff --git a/tests/lean/run/showTactic.lean b/tests/lean/run/showTactic.lean index cb0f88a5698f..498a7c2fb1d2 100644 --- a/tests/lean/run/showTactic.lean +++ b/tests/lean/run/showTactic.lean @@ -22,7 +22,7 @@ example : x = 0 := by -/ /-- -error: 'show' tactic failed, pattern +error: `show` tactic failed, pattern x = 1 is not definitionally equal to target x = 0 @@ -123,7 +123,7 @@ also weren't defeq. -/ /-- -error: 'show' tactic failed, no goals unify with the given pattern. +error: `show` tactic failed, no goals unify with the given pattern. In the first goal, the pattern x = 4