From 231714f1c49b1549581b3448ecb0fa051daa1642 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 13 Apr 2026 17:17:26 +0200 Subject: [PATCH 1/3] chore(AtLocation): make declarations in errors hoverable logWarning does most of the heavy listing (by adding the necessary message context), so this was very easy. Also add a test for the current push_neg error if no progress was made. Making it print the constant pushed would be more readable (but that is not as obvious). --- Mathlib/Util/AtLocation.lean | 4 ++-- MathlibTest/push_neg.lean | 5 +++++ 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/Mathlib/Util/AtLocation.lean b/Mathlib/Util/AtLocation.lean index 8a5188270832b3..195f7b32870c81 100644 --- a/Mathlib/Util/AtLocation.lean +++ b/Mathlib/Util/AtLocation.lean @@ -80,7 +80,7 @@ def transformAtLocalDecl (m : Expr → ReaderT Simp.Context MetaM Simp.Result) ( ReaderT Simp.Context MetaM (Option MVarId) := do let ldecl ← fvarId.getDecl if ldecl.isImplementationDetail then - throwError "Cannot run `{proc}` at `{ldecl.userName}`, it is an implementation detail" + throwError "Cannot run `{proc}` at `{ldecl.toExpr}`, it is an implementation detail" let tgt ← instantiateMVars (← fvarId.getType) let eraseFVarId (ctx : Simp.Context) := ctx.setSimpTheorems <| ctx.simpTheorems.eraseTheorem (.fvar fvarId) @@ -88,7 +88,7 @@ def transformAtLocalDecl (m : Expr → ReaderT Simp.Context MetaM Simp.Result) ( -- we use expression equality here (rather than defeq) to be consistent with, e.g., -- `applySimpResultToLocalDeclCore` if failIfUnchanged && tgt.cleanupAnnotations == r.expr.cleanupAnnotations then - throwError "`{proc}` made no progress at `{ldecl.userName}`" + throwError "`{proc}` made no progress at `{ldecl.toExpr}`" return (← applySimpResultToLocalDecl goal fvarId r mayCloseGoal).map Prod.snd /-- Use the procedure `m` to transform at specified locations (hypotheses and/or goal). diff --git a/MathlibTest/push_neg.lean b/MathlibTest/push_neg.lean index d4c2c51bc9b3a4..f520ac0d8c3b27 100644 --- a/MathlibTest/push_neg.lean +++ b/MathlibTest/push_neg.lean @@ -164,6 +164,11 @@ def inductive_proof : True := by push Not at inductive_proof trivial +-- XXX: can the error message mention the constant being pushed? +/-- error: `push` made no progress on the goal -/ +#guard_msgs in +example {P : Prop} (h : P) : P := by push Not + section use_distrib example (h : ¬ p ∨ ¬ q) : ¬ (p ∧ q) := by From a57352efe3ad24b3ee703e843ab6c6d86e5f356d Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 13 Apr 2026 17:27:25 +0200 Subject: [PATCH 2/3] feat(Push): include constant being pushed in the error message --- Mathlib/Tactic/Push.lean | 2 +- MathlibTest/push_neg.lean | 9 ++++----- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/Mathlib/Tactic/Push.lean b/Mathlib/Tactic/Push.lean index 6085ff1b37543f..e1f951681515f7 100644 --- a/Mathlib/Tactic/Push.lean +++ b/Mathlib/Tactic/Push.lean @@ -211,7 +211,7 @@ def elabDischarger (stx : TSyntax ``discharger) : TacticM Simp.Discharge := def push (cfg : Config) (disch? : Option Simp.Discharge) (head : Head) (loc : Location) (failIfUnchanged : Bool := true) : TacticM Unit := do let cfg := { distrib := cfg.distrib || (← getBoolOption `push_neg.use_distrib) } - transformAtLocation (pushCore head cfg disch? ·) "push" loc failIfUnchanged + transformAtLocation (pushCore head cfg disch? ·) s!"push {head}" loc failIfUnchanged /-- `push c` rewrites the goal by pushing the constant `c` deeper into an expression. diff --git a/MathlibTest/push_neg.lean b/MathlibTest/push_neg.lean index f520ac0d8c3b27..38685991053c69 100644 --- a/MathlibTest/push_neg.lean +++ b/MathlibTest/push_neg.lean @@ -145,27 +145,26 @@ example (h : p ∧ q) : ¬¬(p ∧ q) := by exact h -- new error message as of https://github.com/leanprover-community/mathlib4/issues/27562 -/-- error: `push` made no progress anywhere -/ +/-- error: `push Not` made no progress anywhere -/ #guard_msgs in example {P : Prop} (h : P) : P := by push Not at * -- new behaviour as of https://github.com/leanprover-community/mathlib4/issues/27562 -- (Previously, because of a metavariable instantiation issue, the tactic succeeded as a no-op.) -/-- error: `push` made no progress at `h` -/ +/-- error: `push Not` made no progress at `h` -/ #guard_msgs in example {x y : ℕ} : True := by have h : x ≤ y := test_sorry push Not at h -- new behaviour as of https://github.com/leanprover-community/mathlib4/issues/27562 (previously the tactic succeeded as a no-op) -/-- error: Cannot run `push` at `inductive_proof`, it is an implementation detail -/ +/-- error: Cannot run `push Not` at `inductive_proof`, it is an implementation detail -/ #guard_msgs in def inductive_proof : True := by push Not at inductive_proof trivial --- XXX: can the error message mention the constant being pushed? -/-- error: `push` made no progress on the goal -/ +/-- error: `push Not` made no progress on the goal -/ #guard_msgs in example {P : Prop} (h : P) : P := by push Not From e311139e3832361c965d973c8ead139e74d8f975 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 14 Apr 2026 13:20:56 +0200 Subject: [PATCH 3/3] Review feedback --- Mathlib/Util/AtLocation.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Util/AtLocation.lean b/Mathlib/Util/AtLocation.lean index 195f7b32870c81..dce5c65dad9610 100644 --- a/Mathlib/Util/AtLocation.lean +++ b/Mathlib/Util/AtLocation.lean @@ -80,7 +80,7 @@ def transformAtLocalDecl (m : Expr → ReaderT Simp.Context MetaM Simp.Result) ( ReaderT Simp.Context MetaM (Option MVarId) := do let ldecl ← fvarId.getDecl if ldecl.isImplementationDetail then - throwError "Cannot run `{proc}` at `{ldecl.toExpr}`, it is an implementation detail" + throwError "Cannot run `{proc}` at `{Expr.fvar fvarId}`, it is an implementation detail" let tgt ← instantiateMVars (← fvarId.getType) let eraseFVarId (ctx : Simp.Context) := ctx.setSimpTheorems <| ctx.simpTheorems.eraseTheorem (.fvar fvarId) @@ -88,7 +88,7 @@ def transformAtLocalDecl (m : Expr → ReaderT Simp.Context MetaM Simp.Result) ( -- we use expression equality here (rather than defeq) to be consistent with, e.g., -- `applySimpResultToLocalDeclCore` if failIfUnchanged && tgt.cleanupAnnotations == r.expr.cleanupAnnotations then - throwError "`{proc}` made no progress at `{ldecl.toExpr}`" + throwError "`{proc}` made no progress at `{Expr.fvar fvarId}`" return (← applySimpResultToLocalDecl goal fvarId r mayCloseGoal).map Prod.snd /-- Use the procedure `m` to transform at specified locations (hypotheses and/or goal).