[Merged by Bors] - fix: make the allowed unused tactics extensible#14557
[Merged by Bors] - fix: make the allowed unused tactics extensible#14557
Conversation
PR summary 4d954560deImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>
## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit> |
grunweg
left a comment
There was a problem hiding this comment.
This change seems well-motivated; thank you for doing this!
I have two wording suggestions on the docs. I'm seeing IO.Ref for the first time (and it's undocumented...), so somebody else should review this part carefully. The remainder looks good to me.
|
PS. I would call this a "feature" PR; this might be a matter of taste :-) |
|
@eric-wieser, I know that you have some reservations on |
|
Thanks, looks good to me. Let's have a more qualified pair of eyes, perhaps Eric? |
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
|
Thanks 🎉 If CI passes, please remove the label bors d+ |
|
✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
|
bors r+ |
This PR allows to change the tactics that the unused tactic linter ignores. The main use-case is allowing `done` at the end of proofs, which is very useful for teaching purposes. See for instance [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Disable.20.60linter.2EunusedTactic.60.20warning.20for.20.60done.60).
|
Pull request successfully merged into master. Build succeeded: |
This PR allows to change the tactics that the unused tactic linter ignores.
The main use-case is allowing
doneat the end of proofs, which is very useful for teaching purposes. See for instance this Zulip thread.