Zulip Chat Archive
Stream: general
Topic: grind bugs
Wrenna Robson (Oct 13 2025 at 14:11):
Where do I file bug reports about grind?
Kevin Buzzard (Oct 13 2025 at 14:35):
You might want to first run them through #**lean4> to check they're bugs and go on from there.
Wrenna Robson (Oct 13 2025 at 14:36):
The specific issue I'm having is that deprecated lemmas fed to grind don't seem to flag as such.
Wrenna Robson (Oct 13 2025 at 14:36):
But knowing that I should start there is useful.
Kevin Buzzard (Oct 13 2025 at 14:48):
BTW they like things mathlib-free over there (if possible).
Wrenna Robson (Oct 13 2025 at 14:48):
Aye.
Wrenna Robson (Oct 13 2025 at 14:48):
Not an issue I think (I mean I found the issue in mathlib but I assume it is not limited to it)
Last updated: Dec 20 2025 at 21:32 UTC