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.

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

chore: remove workaround in widgets #3105

Merged
merged 1 commit into from
Dec 22, 2023
Merged

Conversation

Vtec234
Copy link
Member

@Vtec234 Vtec234 commented Dec 21, 2023

This is a follow-up on #2964 that updates stage0, removes a workaround , and updates release notes.

@nomeata
Copy link
Collaborator

nomeata commented Dec 21, 2023

These days we can let GitHub update stage0, which I find a bit cleaner. Should we trigger a stage0 update on master and only the workaround needs to be PRed then, or is that for some reason not desirable here?

@Vtec234
Copy link
Member Author

Vtec234 commented Dec 21, 2023

@nomeata it would be desirable, I just couldn't figure out how to do it! It looked like #3042 only runs if stdlib_flags.h has changed which is not the case here.

@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 Dec 21, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Dec 21, 2023

  • ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-21 11:27:43)
  • ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-12-22' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-12-22 14:55:39)

@Vtec234 Vtec234 requested a review from kim-em as a code owner December 21, 2023 11:34
@Vtec234 Vtec234 changed the title chore: update-stage0 chore: update-stage0, rm workaround, update release notes Dec 21, 2023
@nomeata
Copy link
Collaborator

nomeata commented Dec 21, 2023

It can only be done by people with write permissions. Started at https://github.com/leanprover/lean4/actions/runs/7287788936, let’s see if this works (this is rather new)

@kim-em
Copy link
Collaborator

kim-em commented Dec 21, 2023

We will merge this, but I'll also cherry-pick the release notes onto the release/v4.5.0 branch when I start that tomorrow.

@nomeata
Copy link
Collaborator

nomeata commented Dec 21, 2023

@Vtec234, done, you can merge latest master into this.

@Vtec234 Vtec234 changed the title chore: update-stage0, rm workaround, update release notes chore: remove workaround in widgets Dec 22, 2023
@Vtec234 Vtec234 enabled auto-merge December 22, 2023 14:46
@Vtec234 Vtec234 added this pull request to the merge queue Dec 22, 2023
Merged via the queue into leanprover:master with commit 7c38649 Dec 22, 2023
9 checks passed
@Vtec234 Vtec234 deleted the upd-stg0 branch December 22, 2023 15:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants