feat: add is_value and is_strict_value grind_pattern constraint…
#6479
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 | |
| env: | |
| CCACHE_DIR: ${{ github.workspace }}/.ccache | |
| CCACHE_COMPRESS: true | |
| CCACHE_MAXSIZE: 400M | |
| 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@v5 | |
| 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` | |
| path: | | |
| .ccache | |
| build/stage1/**/*.trace | |
| build/stage1/**/*.olean* | |
| build/stage1/**/*.ilean | |
| build/stage1/**/*.ir | |
| build/stage1/**/*.c | |
| build/stage1/**/*.c.o* | |
| key: Linux Lake-build-v4-${{ github.sha }} | |
| # fall back to (latest) previous cache | |
| restore-keys: | | |
| Linux Lake-build-v4 | |
| - if: env.should_update_stage0 == 'yes' | |
| # sync options with `Linux Lake` to ensure cache reuse | |
| run: | | |
| mkdir -p build | |
| cmake --preset release -B build -DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true | |
| shell: 'nix develop -c bash -euxo pipefail {0}' | |
| - if: env.should_update_stage0 == 'yes' | |
| run: | | |
| make -j$NPROC -C build 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 |