Skip to content

[Merged by Bors] - feat(push): error message tweaks #38008

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
grunweg wants to merge 3 commits into from
+10 −6
Closed

[Merged by Bors] - feat(push): error message tweaks #38008

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
231714f
chore(AtLocation): make declarations in errors hoverable
grunweg Apr 13, 2026
a57352e
feat(Push): include constant being pushed in the error message
grunweg Apr 13, 2026
e311139
Review feedback
grunweg Apr 14, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Mathlib/Tactic/Push.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Util/AtLocation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,15 +80,15 @@ 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 `{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)
let r ← withReader eraseFVarId <| m tgt
-- 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 `{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).
Expand Down
10 changes: 7 additions & 3 deletions MathlibTest/push_neg.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -145,25 +145,29 @@ 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

/-- error: `push Not` 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
Expand Down
Loading