From 3e248628e45c8f4bc6d1a99d641f294759d43df4 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 12 Dec 2023 11:06:07 +0100 Subject: [PATCH 1/2] chore: allow updating stage0 via workflow_dispatch follow-up to #3042 --- .github/workflows/update-stage0.yml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/.github/workflows/update-stage0.yml b/.github/workflows/update-stage0.yml index 6995d9424500..c69faa3db0ef 100644 --- a/.github/workflows/update-stage0.yml +++ b/.github/workflows/update-stage0.yml @@ -8,6 +8,7 @@ on: push: branches: - 'master' + workflow_dispatch: concurrency: group: stage0 @@ -23,16 +24,17 @@ jobs: - uses: actions/checkout@v3 with: ssh-key: ${{secrets.STAGE0_SSH_KEY}} - - name: Check if update is needed + - run: echo "DOIT=yes" >> "$GITHUB_ENV" + - name: Check if automatic update is needed + if: github.event_name == 'push' run: | if diff -u src/stdlib_flags.h stage0/src/stdlib_flags.h then echo "src/stdlib_flags.h and stage0/src/stdlib_flags.h agree, nothing to do" echo "DOIT=no" >> "$GITHUB_ENV" - else - echo "DOIT=yes" >> "$GITHUB_ENV" fi - name: Setup git user + if: env.DOIT == 'yes' run: | git config --global user.name "Lean stage0 autoupdater" git config --global user.email "<>" @@ -52,9 +54,9 @@ jobs: run: nix run .#update-stage0-commit - if: env.DOIT == 'yes' run: git show --stat - - if: env.DOIT == 'yes' + - if: env.DOIT == 'yes' && github.event_name == 'push' name: Sanity check # to avoid loops run: | diff -u src/stdlib_flags.h stage0/src/stdlib_flags.h || exit 1 - if: env.DOIT == 'yes' - run: git push origin HEAD:master + run: git push origin From 61bc5cd720af43d19ecc870236e835db21145fb6 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 13 Dec 2023 10:20:31 +0100 Subject: [PATCH 2/2] Different flag name, documentation --- .github/workflows/update-stage0.yml | 24 +++++++++++---------- doc/dev/bootstrap.md | 33 ++++++++++++++++++++++------- 2 files changed, 38 insertions(+), 19 deletions(-) diff --git a/.github/workflows/update-stage0.yml b/.github/workflows/update-stage0.yml index c69faa3db0ef..a2f051acd8d0 100644 --- a/.github/workflows/update-stage0.yml +++ b/.github/workflows/update-stage0.yml @@ -2,7 +2,9 @@ name: Update stage0 # This action will update stage0 on master as soon as # src/stdlib_flags.h and stage0/src/stdlib_flags.h -# are out of sync there. The update bypasses the merge queue to be quick. +# are out of sync there, or when manually triggered. +# The update bypasses the merge queue to be quick. +# Also see . on: push: @@ -24,39 +26,39 @@ jobs: - uses: actions/checkout@v3 with: ssh-key: ${{secrets.STAGE0_SSH_KEY}} - - run: echo "DOIT=yes" >> "$GITHUB_ENV" + - run: echo "should_update_stage0=yes" >> "$GITHUB_ENV" - name: Check if automatic update is needed if: github.event_name == 'push' run: | if diff -u src/stdlib_flags.h stage0/src/stdlib_flags.h then echo "src/stdlib_flags.h and stage0/src/stdlib_flags.h agree, nothing to do" - echo "DOIT=no" >> "$GITHUB_ENV" + echo "should_update_stage0=no" >> "$GITHUB_ENV" fi - name: Setup git user - if: env.DOIT == 'yes' + if: env.should_update_stage0 == 'yes' run: | git config --global user.name "Lean stage0 autoupdater" git config --global user.email "<>" - - if: env.DOIT == 'yes' + - if: env.should_update_stage0 == 'yes' uses: DeterminateSystems/nix-installer-action@main # Would be nice, but does not work yet: # https://github.com/DeterminateSystems/magic-nix-cache/issues/39 # This action does not run that often and building runs in a few minutes, so ok for now - #- if: env.DOIT == 'yes' + #- if: env.should_update_stage0 == 'yes' # uses: DeterminateSystems/magic-nix-cache-action@v2 - - if: env.DOIT == 'yes' + - if: env.should_update_stage0 == 'yes' name: Install Cachix uses: cachix/cachix-action@v12 with: name: lean4 - - if: env.DOIT == 'yes' + - if: env.should_update_stage0 == 'yes' run: nix run .#update-stage0-commit - - if: env.DOIT == 'yes' + - if: env.should_update_stage0 == 'yes' run: git show --stat - - if: env.DOIT == 'yes' && github.event_name == 'push' + - if: env.should_update_stage0 == 'yes' && github.event_name == 'push' name: Sanity check # to avoid loops run: | diff -u src/stdlib_flags.h stage0/src/stdlib_flags.h || exit 1 - - if: env.DOIT == 'yes' + - if: env.should_update_stage0 == 'yes' run: git push origin diff --git a/doc/dev/bootstrap.md b/doc/dev/bootstrap.md index 28963d40ea31..daed7f30056f 100644 --- a/doc/dev/bootstrap.md +++ b/doc/dev/bootstrap.md @@ -65,19 +65,36 @@ You now have a Lean binary and library that include your changes, though their own compilation was not influenced by them, that you can use to test your changes on test programs whose compilation *will* be influenced by the changes. +## Updating stage0 + Finally, when we want to use new language features in the library, we need to -update the stage 0 compiler, which can be done via `make -C stageN update-stage0`. -`make update-stage0` without `-C` defaults to stage1. +update the archived C source code of the stage 0 compiler in `stage0/src`. + +The github repository will automatically update stage0 on `master` once +`src/stdlib_flags.h` and `stage0/src/stdlib_flags.h` are out of sync. -Updates to `stage0` should be their own commits in the Git history. In -other words, before running `make update-stage0`, please commit your -work. Then, commit the updated `stage0` compiler code with the commit message: +If you have write access to the lean4 repository, you can also also manually +trigger that process, for example to be able to use new features in the compiler itself. +You can do that on +or using Github CLI with ``` -chore: update stage0 +gh workflow run update-stage0.yml ``` -The lean4 github repository has automation to update stage0 on `master` once -`src/stdlib_flags.h` and `stage0/src/stdlib_flags.h` are out of sync. +Leaving stage0 updates to the CI automation is preferrable, but should you need +to do it locally, you can use `make update-stage0` in `build/release`, to +update `stage0` from `stage1`, `make -C stageN update-stage0` to update from +another stage, or `nix run .#update-stage0-commit` to update using nix. + +Updates to `stage0` should be their own commits in the Git history. So should +you have to include the stage0 update in your PR (rather than using above +automation after merging changes), commit your work before running `make +update-stage0`, commit the updated `stage0` compiler code with the commit +message: +``` +chore: update stage0 +``` +and coordinate with the admins to not squash your PR. ## Further Bootstrapping Complications