[Merged by Bors] - chore: adaptations for nightly-2024-02-29#11070
Closed
kim-em wants to merge 31 commits intobump/v4.7.0from
Closed
[Merged by Bors] - chore: adaptations for nightly-2024-02-29#11070kim-em wants to merge 31 commits intobump/v4.7.0from
kim-em wants to merge 31 commits intobump/v4.7.0from
Conversation
grunweg
reviewed
Feb 29, 2024
Contributor
grunweg
left a comment
There was a problem hiding this comment.
A few non-expert comments - it seems this could use a merge of mathlib's master branch.
I was wondering: are the remaining Adaptation notes supposed to stay? If so, would a tracking issue for them be useful, so they don't get forgotten?
Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean
Outdated
Show resolved
Hide resolved
jcommelin
reviewed
Feb 29, 2024
Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean
Outdated
Show resolved
Hide resolved
grunweg
reviewed
Feb 29, 2024
jcommelin
reviewed
Mar 1, 2024
Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean
Outdated
Show resolved
Hide resolved
grunweg
reviewed
Mar 1, 2024
Contributor
grunweg
left a comment
There was a problem hiding this comment.
I've gone over the entire diff: apart from these few nits and the ones already mentioned, the changes are either mechanical, improvements or reverting temporary sorries.
grunweg
reviewed
Mar 1, 2024
Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean
Outdated
Show resolved
Hide resolved
mathlib-bors bot
pushed a commit
that referenced
this pull request
Mar 1, 2024
A random collection of changes, backporting from the upcoming Lean bump. - squeeze one simp - backport one more simp change (which probably was missed in the previous backports) - rewrite the `field_simp` in SolutionOfCubic: with the upcoming Lean bump, this would become **very** slow Similar to #10996 and #11001.
Member
|
Thanks 🎉 If CI passes, please remove the label bors d+ |
Contributor
|
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
riccardobrasca
pushed a commit
that referenced
this pull request
Mar 1, 2024
A random collection of changes, backporting from the upcoming Lean bump. - squeeze one simp - backport one more simp change (which probably was missed in the previous backports) - rewrite the `field_simp` in SolutionOfCubic: with the upcoming Lean bump, this would become **very** slow Similar to #10996 and #11001.
Contributor
Author
|
bors p=10 |
Contributor
|
I just cherry-picked 51da0513b468f47b974b0aa874ca730371f70416, since it seems to fix |
|
As this PR is labelled bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Mar 2, 2024
`field_simp` is a very ambitious tactic, that tries to prove that it can clear denominators. Previously it was taking advantage of essentially a bug in the simp discharging framework, so that parts of its discharging strategy were not limited by `maxDischargeDepth` (so it could "keep trying"), but everyone else was limited (so `simp` didn't waste time exploring large trees of discharges). Now the `maxDischargeDepth` is enforced for everyone, so to keep `field_simp` working we have to increase its `maxDischargeDepth`. That makes it extremely slow. I've kept the `maxDischargeDepth` to a minimum, but still there are some `set_option maxHeartbeats` (all with notes attached). After we've merged this, someone is going to have to rewrite `field_simp` to make it performant. Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de> Co-authored-by: adomani <adomani@gmail.com>
Contributor
|
Pull request successfully merged into bump/v4.7.0. Build succeeded: |
kbuzzard
pushed a commit
that referenced
this pull request
Mar 12, 2024
A random collection of changes, backporting from the upcoming Lean bump. - squeeze one simp - backport one more simp change (which probably was missed in the previous backports) - rewrite the `field_simp` in SolutionOfCubic: with the upcoming Lean bump, this would become **very** slow Similar to #10996 and #11001.
dagurtomas
pushed a commit
that referenced
this pull request
Mar 22, 2024
A random collection of changes, backporting from the upcoming Lean bump. - squeeze one simp - backport one more simp change (which probably was missed in the previous backports) - rewrite the `field_simp` in SolutionOfCubic: with the upcoming Lean bump, this would become **very** slow Similar to #10996 and #11001.
utensil
pushed a commit
that referenced
this pull request
Mar 26, 2024
A random collection of changes, backporting from the upcoming Lean bump. - squeeze one simp - backport one more simp change (which probably was missed in the previous backports) - rewrite the `field_simp` in SolutionOfCubic: with the upcoming Lean bump, this would become **very** slow Similar to #10996 and #11001.
xgenereux
pushed a commit
that referenced
this pull request
Apr 15, 2024
A random collection of changes, backporting from the upcoming Lean bump. - squeeze one simp - backport one more simp change (which probably was missed in the previous backports) - rewrite the `field_simp` in SolutionOfCubic: with the upcoming Lean bump, this would become **very** slow Similar to #10996 and #11001.
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
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.
field_simpis a very ambitious tactic, that tries to prove that it can clear denominators. Previously it was taking advantage of essentially a bug in the simp discharging framework, so that parts of its discharging strategy were not limited bymaxDischargeDepth(so it could "keep trying"), but everyone else was limited (sosimpdidn't waste time exploring large trees of discharges). Now themaxDischargeDepthis enforced for everyone, so to keepfield_simpworking we have to increase itsmaxDischargeDepth. That makes it extremely slow. I've kept themaxDischargeDepthto a minimum, but still there are someset_option maxHeartbeats(all with notes attached).After we've merged this, someone is going to have to rewrite
field_simpto make it performant.#11079 is backporting a few changes to master