feat(Tactic): erw tries rw first and warns if that succeeds#17638
feat(Tactic): erw tries rw first and warns if that succeeds#17638Vierkantor wants to merge 3 commits intomasterfrom
erw tries rw first and warns if that succeeds#17638Conversation
PR summary de4fb5fbf8
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Tactic.Common | 244 | 246 | +2 (+0.82%) |
| Mathlib.Algebra.Order.CauSeq.Basic | 543 | 545 | +2 (+0.37%) |
| Mathlib.CategoryTheory.Sites.Subcanonical | 680 | 682 | +2 (+0.29%) |
Import changes for all files
| Files | Import difference |
|---|---|
| There are 4496 files with changed transitive imports taking up over 190394 characters: this is too many to display! | |
You can run scripts/import_trans_difference.sh all locally to see the whole output. |
Declarations diff
No declarations were harmed in the making of this PR! 🐙
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
|
Thanks for this PR! I'm (perhaps needlessly so) worries about the performance effects of this change. Can you benchmark this/is the speedcenter up and working already? |
Unfortunately the speedcenter was still down yesterday, and I don't see any movement in the zulip thread. I agree that this will make Mathlib a bit slower, but the extra cost of doing a |
927ac49 to
b297481
Compare
b297481 to
18e2fdb
Compare
grunweg
left a comment
There was a problem hiding this comment.
Two nits about outdated comments - otherwise the erw -> rw replacements look good to me. The macro looks plausible to me, but I'm not an expert on them - that's a low-confidence approval of that part.
Nicely spotted, thanks! |
|
Lets split this into separate PRs for changing proofs and for the macro. |
|
I would prefer a solution where we only run the extra check in CI, like we do for |
1c9b47b to
edc1e5c
Compare
See #17703 for only the changed proofs. |
|
I'm curious about the overall balance of this PR, thus let me bench it. |
|
!bench |
Go through Mathlib and replace `erw` calls where `rw` would also succeed. This PR is split off from #17638, containing all the changes that the linter suggested. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
|
This PR/issue depends on: |
|
Here are the benchmark results for commit edc1e5c. Benchmark Metric Change
================================================================================
- ~Mathlib.Algebra.Module.LocalizedModule instructions 8.2%
- ~Mathlib.CategoryTheory.Adjunction.Lifting.Right instructions 46.6%
- ~Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing instructions 15.4%
- ~Mathlib.RepresentationTheory.GroupCohomology.Resolution instructions 8.1% |
|
The previous PR was performance-neutral - so the benchmark should mostly represent the effect of this PR. Overall, there is a slowdown of 200*10⁹ instruction (about 0.1-0.2% of all of mathlib). |
|
I'll hold off on merging this PR then, running it manually every so often until the number of |
6f76810 to
af3c28c
Compare
Automatically found by the `erw` linter from #17638.
The `erw` linter of #17638 spotted two `erw`s that can be turned into `rw` for free.
This PR adds a macro rule to the `erw` tactic that first tries `rw` at reducible transparency, and displays a "Try this:" if that succeeded. This should help us get rid of uselessly slow `erw`s. This is a relatively simple implementation that does not verify if `erw` and `rw` would have resulted in the same exact rewrite. So it is possible that `erw` and `rw` both succeed but rewrite different occurrences, and there would be a suggestion to replace `erw` with `rw` in that case. I think the complication of running both at the same time and checking the goal state afterwards doesn't weigh up to accepting that this happens and adding an explanation to the warning generated by `erw`. I import the `erw` extension in `Tactic.Common`: it might be nice to migrate this up even earlier in the import hierarchy but `Mathlib.Tactic.TryThis` is a somewhat heavy import to put in `Mathlib.Tactic.Core`.
af3c28c to
de4fb5f
Compare
The linter of #17638 found five more `erw`s that could also be `rw`s. 🐙
The linter of #17638 found five more `erw`s that could also be `rw`s. 🐙
The linter of #17638 found five more `erw`s that could also be `rw`s. 🐙
The linter of #17638 found five more `erw`s that could also be `rw`s. 🐙
The `erw` linter from #17638 caught these `erw`s that can become `rw` without breaking the proofs.
The `erw` linter from #17638 caught these `erw`s that can become `rw` without breaking the proofs.
|
I think this can now be definitively closed in favour of |
This PR adds a macro rule to the
erwtactic that first triesrwat reducible transparency, and displays a "Try this:" if that succeeded. This should help us get rid of uselessly slowerws.This is a relatively simple implementation that does not verify if
erwandrwwould have resulted in the same exact rewrite. So it is possible thaterwandrwboth succeed but rewrite different occurrences, and there would be a suggestion to replaceerwwithrwin that case. I think the complication of running both at the same time and checking the goal state afterwards doesn't weigh up to accepting that this happens and adding an explanation to the warning generated byerw.I import the
erwextension inTactic.Common: it might be nice to migrate this up even earlier in the import hierarchy butMathlib.Tactic.TryThisis a somewhat heavy import to put inMathlib.Tactic.Core.Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Fixing.20the.20.60erw.60.20hell.20around.20concrete.20categories
erwwithrwwhere possible #17703