[Merged by Bors] - chore(field_theory/intermediate_field): fix timeout #14725
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
alreadydone
added
easy
github-actions
bot
removed
the
awaiting-CI
eric-wieser
reviewed
Jun 14, 2022
eric-wieser
added
awaiting-author
alreadydone
added
awaiting-review
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Thanks bors d+ |
|
✌️ alreadydone can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
bors r+ |
|
Strangely bors reports merge conflict but github doesn't. Let me try again. bors r+ |
|
Already running a review |
|
This means that this PR conflicts with another PR in the bors batch. The only option is to wait for one of the two PRs to get merged. |
bors bot
pushed a commit
that referenced
this pull request
Jun 15, 2022
+ Remove `@[simps]` from `intermediate_field_map` to reduce `decl post-processing of intermediate_field_map` from 18.3s to 46.4ms (on my machine). + Manually provide the two `simp` lemmas previously auto-generated by `@[simps]`. Mathlib compiles even without the two simp lemmas (see commit 1f5a7f1), but I am inclined to keep them in case some other branches/projects are using them. [Zulip reports](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/deterministic.20timeout/near/285792556) about `intermediate_field_map` causing timeout in two separate branches
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Remove
@[simps]fromintermediate_field_mapto reducedecl post-processing of intermediate_field_mapfrom 18.3s to 46.4ms (on my machine).Manually provide the two
simplemmas previously auto-generated by@[simps]. Mathlib compiles even without the two simp lemmas (see commit 1f5a7f1), but I am inclined to keep them in case some other branches/projects are using them.Zulip reports about
intermediate_field_mapcausing timeout in two separate branches