feat: add impossible tactic combinator (#13771)
#55
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 | |
| defaults: | |
| run: | |
| # like Linux release | |
| shell: nix develop .#oldGlibc -c bash -euxo pipefail {0} | |
| 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@v6 | |
| with: | |
| ssh-key: ${{secrets.STAGE0_SSH_KEY}} | |
| - shell: bash | |
| run: echo "should_update_stage0=yes" >> "$GITHUB_ENV" | |
| - name: Check if automatic update is needed | |
| if: github.event_name == 'push' | |
| shell: bash | |
| 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' | |
| shell: bash | |
| 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 | |
| - 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 | |
| - name: Restore Cache | |
| if: env.should_update_stage0 == 'yes' | |
| uses: actions/cache/restore@v5 | |
| 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 release-build-v4-${{ github.sha }} | |
| # fall back to (latest) previous cache | |
| restore-keys: | | |
| Linux release-build-v4 | |
| - if: env.should_update_stage0 == 'yes' | |
| name: Configure Build | |
| # sync options with `Linux release` to ensure cache reuse | |
| run: | | |
| mkdir -p build | |
| cd build | |
| wget -q https://github.com/leanprover/lean-llvm/releases/download/22.1.4/lean-llvm-x86_64-linux-gnu.tar.zst | |
| PREPARE="$(../script/prepare-llvm-linux.sh lean-llvm*)" | |
| eval "OPTIONS=($PREPARE)" | |
| cmake .. --preset release -B . -DWFAIL=ON -DLEAN_EXTRA_CXX_FLAGS=-Werror "${OPTIONS[@]}" | |
| - if: env.should_update_stage0 == 'yes' | |
| run: | | |
| make -j$NPROC -C build update-stage0-commit | |
| - 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 |