Skip to content
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.

Sign up for GitHub

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

Jump to bottom

feat: bundle of widget improvements #2964

Merged
merged 18 commits into from
Dec 21, 2023
Merged

feat: bundle of widget improvements #2964

merged 18 commits into from
Dec 21, 2023

Conversation

Vtec234
Copy link
Member

@Vtec234 Vtec234 commented Nov 26, 2023 •
edited
Loading

Implements RFC #2963.

Leftover tasks:

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 26, 2023
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 26, 2023
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#2964
82fd5d2
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Nov 26, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Nov 26, 2023 •
edited
Loading

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 27, 2023
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#2964
91fc481
Kha
Kha approved these changes Dec 10, 2023
View reviewed changes
Copy link
Member

@Kha Kha left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There isn't really any non-widget code to review, so just a comment from me

src/Lean/Server/InfoUtils.lean Outdated Show resolved Hide resolved
@Vtec234 Vtec234 changed the title Bundle of widget improvements feat: bundle of widget improvements Dec 13, 2023
@Vtec234 Vtec234 mentioned this pull request Dec 13, 2023
Merged
@Vtec234 Vtec234 force-pushed the widget-modules branch 2 times, most recently from 96db5c4 to 684b8e2 Compare December 15, 2023 20:45
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 15, 2023
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#2964
df351c9
@kim-em kim-em added the full-ci label Dec 20, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Dec 20, 2023
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 20, 2023
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#2964
e51b53f
kim-em
kim-em approved these changes Dec 21, 2023
View reviewed changes
Copy link
Collaborator

@kim-em kim-em left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The necessary changes in Mathlib look fine with me, so I would be okay with merging this. We are now extremely close to the cut-off for v4.5.0-rc1, however.

@kim-em kim-em added this pull request to the merge queue Dec 21, 2023
Merged via the queue into leanprover:master with commit 8d04ac1 Dec 21, 2023
36 checks passed
kim-em added a commit to leanprover-community/batteries that referenced this pull request Dec 21, 2023
@kim-em
feat: adaptations for leanprover/lean4#2964
823a1f4
digama0 pushed a commit to leanprover-community/batteries that referenced this pull request Dec 21, 2023
@kim-em
feat: adaptations for leanprover/lean4#2964 (#475)
4165f2c
@Vtec234 Vtec234 deleted the widget-modules branch December 21, 2023 10:51
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 21, 2023
@kim-em
feat: adaptations for leanprover/lean4#2964
0f91279
@kim-em kim-em mentioned this pull request Dec 21, 2023
Closed
@Vtec234 Vtec234 mentioned this pull request Dec 21, 2023
Merged
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 21, 2023
@kim-em
feat: adaptations for leanprover/lean4#2964 (#9176)
43459fe 
This is a PR to `bump/v4.5.0`, containing the adaptations required for @Vtec234's leanprover/lean4#2964.

This will bring `bump/v4.5.0` up to `nightly-2023-12-21`, which will tomorrow become `v4.5.0-rc1`. Thus once this PR is delegated and merged, Mathlib should be ready to move to the next release.



Co-authored-by: Scott Morrison <[email protected]>
kim-em added a commit to leanprover-community/batteries that referenced this pull request Dec 21, 2023
@kim-em @kmill
chore: move toolchain to v4.5.0-rc1, and merge changes from bump/v4.5…
ee49cf8 
….0 (#479)

* fixes for lean4#2973 (#470)

Co-authored-by: Kyle Miller <[email protected]>

* feat: adaptations for leanprover/lean4#2964 (#475)

* chore: move toolchain to v4.5.0-rc1

---------

Co-authored-by: Kyle Miller <[email protected]>
@kim-em kim-em mentioned this pull request Dec 21, 2023
Closed
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 22, 2023
@kim-em @eric-wieser
chore: move to v4.5.0-rc1, and merge changes from bump/v4.5.0 branc…
58eef79 
…h. (#9188)

This PR:
* bumps to lean-toolchain to `v4.5.0-rc1`
* bumps the Std and Aesop dependencies to their versions using `v4.5.0-rc1`
* merge the already reviewed changes from the `bump/v4.5.0` branch
  * adaptations for leanprover/lean4#2923 in #9011
  * adaptations for leanprover/lean4#2973 in #9161
  * adaptations for leanprover/lean4#2964 in #9176

Co-authored-by: Scott Morrison <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
@nomeata nomeata mentioned this pull request Dec 22, 2023
Closed
github-merge-queue bot pushed a commit that referenced this pull request Dec 22, 2023
@Vtec234
chore: remove workaround in widgets (#3105)
7c38649 
This is a follow-up on #2964 that ~~updates stage0,~~ removes a
workaround ~~, and updates release notes.~~
@Vtec234 Vtec234 mentioned this pull request Jul 20, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em kim-em approved these changes

@Kha Kha Kha approved these changes

@mhuisi mhuisi Awaiting requested review from mhuisi mhuisi is a code owner

@leodemoura leodemoura Awaiting requested review from leodemoura

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@Vtec234 @leanprover-community-mathlib4-bot @Kha @kim-em