[Merged by Bors] - chore: move Mathlib to v4.7.0-rc1#11162
Closed
[Merged by Bors] - chore: move Mathlib to v4.7.0-rc1#11162
Conversation
…n split tactic) (#10330) This was previously #10328, but I merged this into `master`, not `bump/v4.7.0`. 🤦♀️ Trying again. --- <!-- The text above the `---` will become the commit message when your PR is merged. Please leave a blank newline before the `---`, otherwise GitHub will format the text above it as a title. To indicate co-authors, include lines at the bottom of the commit message (that is, before the `---`) using the following format: Co-authored-by: Author Name <author@email.com> Any other comments you want to keep out of the PR commit should go below the `---`, and placed outside this HTML comment, or else they will be invisible to reviewers. If this PR depends on other PRs, please list them below this comment, using the following format: - [ ] depends on: #abc [optional extra text] - [ ] depends on: #xyz [optional extra text] --> [](https://gitpod.io/from-referrer/) --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Note this is a PR to `bump/v4.7.0`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
This is a PR to bump/v4.7.0
This is a PR to bump/v4.7.0 Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Vierkantor <vierkantor@vierkantor.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com>
`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>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Contributor
Author
|
bors p=10 |
|
As this PR is labelled bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Mar 5, 2024
This is a very large PR, but it has been reviewed piecemeal already in PRs to the `bump/v4.7.0` branch as we update to intermediate nightlies. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: damiano <adomani@gmail.com>
Contributor
|
Build failed: |
Contributor
Author
|
bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Mar 5, 2024
This is a very large PR, but it has been reviewed piecemeal already in PRs to the `bump/v4.7.0` branch as we update to intermediate nightlies. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: damiano <adomani@gmail.com>
|
As this PR is labelled bors merge |
Contributor
|
Already running a review |
Contributor
|
Pull request successfully merged into master. Build succeeded: |
kbuzzard
pushed a commit
that referenced
this pull request
Mar 12, 2024
This is a very large PR, but it has been reviewed piecemeal already in PRs to the `bump/v4.7.0` branch as we update to intermediate nightlies. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: damiano <adomani@gmail.com>
dagurtomas
pushed a commit
that referenced
this pull request
Mar 22, 2024
This is a very large PR, but it has been reviewed piecemeal already in PRs to the `bump/v4.7.0` branch as we update to intermediate nightlies. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: damiano <adomani@gmail.com>
utensil
pushed a commit
that referenced
this pull request
Mar 26, 2024
This is a very large PR, but it has been reviewed piecemeal already in PRs to the `bump/v4.7.0` branch as we update to intermediate nightlies. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: damiano <adomani@gmail.com>
This was referenced Apr 6, 2024
xgenereux
pushed a commit
that referenced
this pull request
Apr 15, 2024
This is a very large PR, but it has been reviewed piecemeal already in PRs to the `bump/v4.7.0` branch as we update to intermediate nightlies. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: damiano <adomani@gmail.com>
mathlib-bors bot
pushed a commit
that referenced
this pull request
May 15, 2024
In this PR, we implements process when an new equation is added to a congruence closure. Also, `Lean.Expr.relSidesIfSymm?` is removed in #11162, but this def is required for `cc` tactic, so we recover this. Co-authored-by: Pol'tta / Miyahara Kō <52843868+Komyyy@users.noreply.github.com>
callesonne
pushed a commit
that referenced
this pull request
May 16, 2024
In this PR, we implements process when an new equation is added to a congruence closure. Also, `Lean.Expr.relSidesIfSymm?` is removed in #11162, but this def is required for `cc` tactic, so we recover this. Co-authored-by: Pol'tta / Miyahara Kō <52843868+Komyyy@users.noreply.github.com>
grunweg
pushed a commit
that referenced
this pull request
May 17, 2024
In this PR, we implements process when an new equation is added to a congruence closure. Also, `Lean.Expr.relSidesIfSymm?` is removed in #11162, but this def is required for `cc` tactic, so we recover this. Co-authored-by: Pol'tta / Miyahara Kō <52843868+Komyyy@users.noreply.github.com>
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
3 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.
This is a very large PR, but it has been reviewed piecemeal already in PRs to the
bump/v4.7.0branch as we update to intermediate nightlies.