chore: move Nat theorems into namespace in ForLean #3092
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 | |
| - name: Compile Library 🧐 | |
| run: | | |
| lake -R exe cache get # download cache of mathlib docs. | |
| lake -R build SSA | |
| - name: Compile Decide Experiment 🧐 | |
| run: | | |
| lake -R exe cache get # download cache of mathlib docs. | |
| lake -R build SSA.Experimental.Bits.Decide SSA.Experimental.Bits.Fast.Decide | |
| - name: Compile Hacker's Delight Theorems 🧮 | |
| run: | | |
| lake -R exe cache get # download cache of mathlib docs. | |
| lake -R build SSA.Projects.InstCombine.HackersDelight # compile and check the Hacker's Delight theorems | |
| - name: Compile Alive Examples | |
| run: | | |
| lake -R exe cache get # download cache of mathlib docs. | |
| lake -R build AliveExamples 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 exe cache get # download cache of mathlib docs. | |
| lake -R build SSA.Projects.CIRCT.DC # 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)` | |
| }) |