Skip to content

[Merged by Bors] - chore: more backporting of simp changes from #10995#11001

Closed
kim-em wants to merge 5 commits intomasterfrom
pm_simp2
Closed

[Merged by Bors] - chore: more backporting of simp changes from #10995#11001
kim-em wants to merge 5 commits intomasterfrom
pm_simp2

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Feb 27, 2024 •
edited by mathlib-bors bot
Loading

No description provided.

@kim-em kim-em changed the title chore: more back of simp changes from #10995 chore: more backporting of simp changes from #10995 Feb 27, 2024
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Feb 27, 2024

Thanks 🎉

If CI passes, please remove the label awaiting-CI and merge this yourself, by adding a comment bors r+.

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 27, 2024

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@jcommelin jcommelin added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 27, 2024
@github-actions github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 27, 2024
@kim-em kim-em added auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. and removed awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Feb 27, 2024
@ghost
Copy link
Copy Markdown

ghost commented Feb 27, 2024

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Feb 27, 2024
@kim-em @PatrickMassot
chore: more backporting of simp changes from #10995 (#11001)
d9589c1 
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 27, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: more backporting of simp changes from #10995 [Merged by Bors] - chore: more backporting of simp changes from #10995 Feb 27, 2024
@mathlib-bors mathlib-bors bot closed this Feb 27, 2024
@mathlib-bors mathlib-bors bot deleted the pm_simp2 branch February 27, 2024 10:02
@grunweg grunweg mentioned this pull request Mar 1, 2024
Closed
mathlib-bors bot pushed a commit that referenced this pull request Mar 1, 2024
@grunweg
chore: backport a few misc changes from #11070 to master (#11079)
79aeb77 
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.
riccardobrasca pushed a commit that referenced this pull request Mar 1, 2024
@kim-em @PatrickMassot @riccardobrasca
chore: more backporting of simp changes from #10995 (#11001)
052bc52 
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
riccardobrasca pushed a commit that referenced this pull request Mar 1, 2024
@grunweg @riccardobrasca
chore: backport a few misc changes from #11070 to master (#11079)
171dfad 
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.
kbuzzard pushed a commit that referenced this pull request Mar 12, 2024
@kim-em @PatrickMassot @kbuzzard
chore: more backporting of simp changes from #10995 (#11001)
7fd0498 
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
kbuzzard pushed a commit that referenced this pull request Mar 12, 2024
@grunweg @kbuzzard
chore: backport a few misc changes from #11070 to master (#11079)
6ca0ccf 
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
@kim-em @PatrickMassot @dagurtomas
chore: more backporting of simp changes from #10995 (#11001)
66c0098 
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@grunweg @dagurtomas
chore: backport a few misc changes from #11070 to master (#11079)
90147dd 
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
@grunweg @utensil
chore: backport a few misc changes from #11070 to master (#11079)
9d3727b 
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
@kim-em @PatrickMassot @xgenereux
chore: more backporting of simp changes from #10995 (#11001)
fbfd450 
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
xgenereux pushed a commit that referenced this pull request Apr 15, 2024
@grunweg @xgenereux
chore: backport a few misc changes from #11070 to master (#11079)
ac6094f 
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer).

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@kim-em @jcommelin @PatrickMassot