[Merged by Bors] - chore: bump to nightly-2023-08-17#6019
[Merged by Bors] - chore: bump to nightly-2023-08-17#6019
Conversation
There was a problem hiding this comment.
Looked through all the files, basically everything is just removing superfluous simp-calls, except one deletion marked below.
In my optinion any_goals simp would be better than _ <;> (try simp) or all_goals (try simp) and it's a bit a shame that <;> simp does not work like any_goals simp.
One thing I did not check is if this PR really modifies all tactics that rely on simp making no progress.
9a539d8 to
6b5c3f9
Compare
| | `(tactic| whisker_simps) => do | ||
| evalTactic (← `(tactic| | ||
| simp only [Category.assoc, Bicategory.comp_whiskerLeft, Bicategory.id_whiskerLeft, | ||
| simp (config := {failIfUnchanged := false}) only [Category.assoc, |
There was a problem hiding this comment.
Can you add an explanation of why failIfUnchanged is helpful here? Should whisker_simps take it's own config argument to allow the caller to customize this?
There was a problem hiding this comment.
It hadn't even occurred to me this counted as a user facing tactic. Mostly it is just used as a component in coherence. But sure, I'll give it a simp configuration.
|
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
The major change here is adapting to `simp` failing if it makes no progress. The vast majority of the redundant `simp`s found due to this change were extracted to #6632. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
The major change here is adapting to
simpfailing if it makes no progress.The vast majority of the redundant
simps found due to this change were extracted to #6632.