chore: automata: prove worklistRun #4537
This file contains 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: core library | |
| on: | |
| push: | |
| branches: | |
| - "main" | |
| pull_request: | |
| merge_group: | |
| permissions: | |
| contents: write | |
| jobs: | |
| build: | |
| name: core library | |
| permissions: | |
| pull-requests: write | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout 🛎️ | |
| uses: actions/checkout@v3 | |
| - name: Install elan 🕑 | |
| run: | | |
| set -o pipefail | |
| curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y | |
| ~/.elan/bin/lean --version | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Cache `.lake` folder | |
| id: cache-lake | |
| uses: actions/cache@v4 | |
| with: | |
| path: .lake | |
| key: ${{ runner.os }}-lake-${{ hashFiles('lake-manifest.json') }}-4 | |
| - name: Get mathlib cache (only if no cache available) | |
| if: steps.cache-lake.outputs.cache-hit != 'true' | |
| run: | | |
| lake -R exe cache get # download cache of mathlib docs. | |
| - name: Compile Library 🧐 | |
| run: | | |
| lake -R build SSA | |
| - name: Compile Decide Experiment 🧐 | |
| run: | | |
| lake -R build SSA.Experimental.Bits.Decide SSA.Experimental.Bits.Fast.Decide | |
| - name: Compile Hacker's Delight Theorems 🧮 | |
| run: | | |
| lake -R build SSA.Projects.InstCombine.HackersDelight.ch2_1DeMorgan # compile and check the Hacker's Delight theorems chapter 2-1 | |
| lake -R build SSA.Projects.InstCombine.HackersDelight.ch2_2AdditionAndLogicalOps # compile and check the Hacker's Delight theorems chapter 2-2 | |
| - name: Compile Alive Examples | |
| run: | | |
| lake -R build AliveExamples | |
| lake -R build AliveStatements 2>&1 | tee out | |
| echo `grep theorem SSA/Projects/InstCombine/AliveStatements.lean | wc -l` > all | |
| grep 'Alive.*sorry' out | wc -l > failed | |
| x=$((`cat all` - `cat failed`)); echo $x > diff | |
| echo "ALIVE_SUCCESS=$(cat diff)" >> $GITHUB_ENV | |
| echo "ALIVE_ALL=$(cat all)" >> $GITHUB_ENV | |
| echo "ALIVE_FAILED=$(cat failed)" >> $GITHUB_ENV | |
| - name: Compile DC | |
| run: | | |
| lake -R build SSA.Projects.CIRCT.Handshake.Handshake # compile and check CIRCT's Handshake Dialect | |
| lake -R build SSA.Projects.CIRCT.Handshake.HandshakeExample # test CIRCT's Handshake Dialect | |
| lake -R build SSA.Projects.CIRCT.DC.DC # compile and check CIRCT's DC Dialect | |
| lake -R build SSA.Projects.CIRCT.DC.DCExample # compile and check CIRCT's DC Dialect | |
| - uses: actions/github-script@v6 | |
| if: github.event_name == 'pull_request' | |
| with: | |
| script: | | |
| github.rest.issues.createComment({ | |
| issue_number: context.issue.number, | |
| owner: context.repo.owner, | |
| repo: context.repo.repo, | |
| body: `Alive Statistics: ${{env.ALIVE_SUCCESS}} / ${{env.ALIVE_ALL}} (${{env.ALIVE_FAILED}} failed)` | |
| }) |