chore: add simple simp benchmark (#9380) #87
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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, 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 | |
| cancel-in-progress: true | |
| jobs: | |
| update-stage0: | |
| runs-on: nscloud-ubuntu-22.04-amd64-8x16 | |
| steps: | |
| # This action should push to an otherwise protected branch, so it | |
| # uses a deploy key with write permissions, as suggested at | |
| # https://stackoverflow.com/a/76135647/946226 | |
| - uses: actions/checkout@v4 | |
| with: | |
| ssh-key: ${{secrets.STAGE0_SSH_KEY}} | |
| - 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 "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.should_update_stage0 == 'yes' | |
| name: Install Nix | |
| uses: DeterminateSystems/nix-installer-action@main | |
| - name: Open Nix shell once | |
| if: env.should_update_stage0 == 'yes' | |
| run: true | |
| shell: 'nix develop -c bash -euxo pipefail {0}' | |
| - name: Set up NPROC | |
| if: env.should_update_stage0 == 'yes' | |
| run: | | |
| echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV | |
| shell: 'nix develop -c bash -euxo pipefail {0}' | |
| - name: Restore Cache | |
| if: env.should_update_stage0 == 'yes' | |
| uses: actions/cache/restore@v4 | |
| with: | |
| # NOTE: must be in sync with `restore-cache` in `build-template.yml` | |
| # TODO: actually switch to USE_LAKE once it caches more; for now it just caches more often than any other build type so let's use its cache | |
| path: | | |
| .ccache | |
| key: Linux Lake-build-v3-${{ github.sha }} | |
| # fall back to (latest) previous cache | |
| restore-keys: | | |
| Linux Lake-build-v3 | |
| - if: env.should_update_stage0 == 'yes' | |
| run: cmake --preset release | |
| shell: 'nix develop -c bash -euxo pipefail {0}' | |
| - if: env.should_update_stage0 == 'yes' | |
| run: make -j$NPROC -C build/release update-stage0-commit | |
| shell: 'nix develop -c bash -euxo pipefail {0}' | |
| - if: env.should_update_stage0 == 'yes' | |
| run: git show --stat | |
| - 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.should_update_stage0 == 'yes' | |
| run: git push origin |