chore: allow updating stage0 via workflow_dispatch (#3052)

follow-up to #3042

.github/workflows/update-stage0.yml

@@ -2,12 +2,15 @@ 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 <doc/dev/bootstrap.md>.
 
 on:
   push:
     branches:
       - 'master'
+  workflow_dispatch:
 
 concurrency:
   group: stage0
@@ -23,38 +26,39 @@ jobs:
     - uses: actions/checkout@v3
       with:
         ssh-key: ${{secrets.STAGE0_SSH_KEY}}
-    - name: Check if update is needed
+    - 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"
-        else
-          echo "DOIT=yes" >> "$GITHUB_ENV"
+          echo "should_update_stage0=no" >> "$GITHUB_ENV"
         fi
     - name: Setup git user
+      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'
+    - 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'
-      run: git push origin HEAD:master
+    - if: env.should_update_stage0 == 'yes'
+      run: git push origin

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 <https://github.com/nomeata/lean4/actions/workflows/update-stage0.yml>
+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