-
Notifications
You must be signed in to change notification settings - Fork 234
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore: adaptations for nightly-2024-02-29 #11070
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A few non-expert comments - it seems this could use a merge of mathlib's master branch.
I was wondering: are the remaining Adaptation note
s 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
Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean
Outdated
Show resolved
Hide resolved
Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean
Outdated
Show resolved
Hide resolved
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean
Outdated
Show resolved
Hide resolved
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.
Thanks 🎉 If CI passes, please remove the label bors d+ |
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
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.
bors p=10 |
I just cherry-picked 51da0513b468f47b974b0aa874ca730371f70416, since it seems to fix |
As this PR is labelled bors merge |
`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>
Pull request successfully merged into bump/v4.7.0. Build succeeded: |
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.
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.
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.
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.
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 bymaxDischargeDepth
(so it could "keep trying"), but everyone else was limited (sosimp
didn't waste time exploring large trees of discharges). Now themaxDischargeDepth
is enforced for everyone, so to keepfield_simp
working we have to increase itsmaxDischargeDepth
. That makes it extremely slow. I've kept themaxDischargeDepth
to 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_simp
to make it performant.#11079 is backporting a few changes to master