Zulip Chat Archive

Stream: new members

Topic: Wall of warnings of `unreachableTactic`/`unusedTactic`

Snir Broshi (Feb 01 2026 at 05:31):

Umm what just happened?

import Mathlib
theorem foo : StrictMonoOn (α := Nat) (id ∘ id) .univ := by
  apply StrictMonoOn.comp (α := Nat) (s := setOf True)
  · sorry
  · sorry
  · sorry
  · sorry

image.png

Is this a known/unknown bug? I know that declaration uses sorry is because errors (delab errors?) return sorry when they break.
This code is error-free, it only has warnings :eyes:

version with #guard_msgs

Eric Wieser (Feb 01 2026 at 05:35):

I think there is a non-linter bug here:

import Mathlib

theorem foo : StrictMonoOn (α := Nat) (id ∘ id) .univ := by
  apply StrictMonoOn.comp (α := Nat) (s := setOf True)

this should raise a type error, but does not

Eric Wieser (Feb 01 2026 at 05:36):

It was fine in Lean 4.27.0

Eric Wieser (Feb 01 2026 at 05:36):

Can you try to minize and post in #lean4?

Snir Broshi (Feb 01 2026 at 05:36):

What type error should this throw?

Eric Wieser (Feb 01 2026 at 05:38):

setOf True is illegal

Eric Wieser (Feb 01 2026 at 05:38):

Try changing the web editor to "mathlib stable" to see the correct behavior

Eric Wieser (Feb 01 2026 at 05:40):

Hey, you can write whatever you like too!

theorem foo : StrictMonoOn (α := Nat) (id ∘ id) .univ := by
  apply StrictMonoOn.comp (α := Nat) (s := setOf True)
  exact "qed"

Snir Broshi (Feb 01 2026 at 05:53):

This is somehow Mathlib's fault:

import Mathlib

def MyProp {α : Type} (f : α → α) (s : Bool) : Prop :=
  s = s

theorem MyProp.mk {α : Type} {f : α → α} {s : Bool} : MyProp f s := by
  sorry

theorem foo : MyProp (α := Nat) id true := by
  apply MyProp.mk (α := Nat) (s := "foo")
  exact "qed"

No Mathlib stuff used, but removing the import surfaces the errors

Snir Broshi (Feb 01 2026 at 05:59):

This is getting too minimized, I'm now confused how anything even works correctly in this mathlib version

import Mathlib.Tactic

def MyProp (n : Nat) : Prop :=
  n = n

theorem MyProp.mk (n : Nat) : MyProp n :=
  rfl

theorem foo : MyProp 1337 := by
  apply MyProp.mk "foo"
  exact "qed"

Snir Broshi (Feb 01 2026 at 06:11):

I think I've narrowed it down to the "apply with" tactic, and #34524 changed it 3 days ago, so cc @Anne Baanen 

import Mathlib.Tactic.ApplyWith

def MyProp (n : Nat) : Prop :=
  n = n

theorem MyProp.mk (n : Nat) : MyProp n :=
  rfl

theorem foo : MyProp 1337 := by
  apply MyProp.mk "foo"
  exact "qed"

Snir Broshi (Feb 01 2026 at 06:16):

Ooh this also means a workaround is to not use apply for now, I'll just refine for now

Snir Broshi (Feb 01 2026 at 06:21):

I assume this thread will conclude with a fix + tests, but is there some way to prevent this "auto sorry and ignore everything that follows" in the future? Perhaps change the thing that auto-inserts sorry to instead log "you've triggered an internal error, please report this on Zulip"?

Eric Wieser (Feb 02 2026 at 06:51):

https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/optConfig.20causes.20tactics.20to.20be.20ignored/near/571337570

Last updated: Feb 28 2026 at 14:05 UTC