Repository navigation
Track Lean core changes for measurable monads and rdo #99
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: Build project | |
| on: | |
| push: | |
| branches: | |
| - main # Trigger on pushes to the default branch | |
| pull_request: | |
| branches: | |
| - main | |
| workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface | |
| # Cancel previous runs if a new commit is pushed to the same PR or branch | |
| concurrency: | |
| group: ${{ github.ref }} # Group runs by the ref (branch or PR) | |
| cancel-in-progress: true # Cancel any ongoing runs in the same group | |
| # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages | |
| permissions: | |
| contents: write # Push the provenance ledger back to the branch (see the step that does) | |
| pages: write # Write access to GitHub Pages | |
| id-token: write # Write access to ID tokens | |
| issues: write # Write access to issues | |
| pull-requests: write # Write access to pull requests | |
| actions: read # Read the previous run's artifact, for the referee revision diff | |
| jobs: | |
| build_project: | |
| runs-on: ubuntu-latest | |
| name: Build project | |
| steps: | |
| - name: Cleanup to free disk space | |
| uses: jlumbroso/free-disk-space@54081f138730dfa15788a46383842cd2f914a1be # v1.3.0 | |
| with: | |
| tool-cache: false | |
| android: true # saves approximately 12 GB | |
| dotnet: false | |
| haskell: false | |
| large-packages: false | |
| docker-images: false | |
| swap-storage: false | |
| - name: Checkout project | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| # Load-bearing for provenance, not just a convenience: the ledger's edit half is | |
| # `git blame`, and at the default `fetch-depth: 1` blame attributes the entire library to | |
| # the single fetched commit. | |
| fetch-depth: 0 # Fetch all history for all branches and tags | |
| - name: Build, lint and test project | |
| uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0 | |
| with: | |
| build: true | |
| build-args: "--wfail" | |
| lint: true | |
| mk_all-check: true | |
| - name: Test upstream tracking | |
| run: | | |
| python3 -m unittest discover -s .github/upstream/tests -p 'test_check.py' | |
| node --test .github/upstream/tests/test_notify.cjs | |
| lake env lean .github/upstream/tests/Analogue.lean | |
| - name: Check adapted definitions against the pinned Lean toolchain | |
| run: | | |
| lake env lean .github/upstream/Export.lean > .lake/upstream-current.json | |
| python3 .github/upstream/check.py check --metadata .lake/upstream-current.json \ | |
| --report .lake/upstream-report.md | |
| - name: Show upstream changes | |
| if: always() | |
| run: | | |
| if [ -f .lake/upstream-report.md ]; then | |
| cat .lake/upstream-report.md >> "$GITHUB_STEP_SUMMARY" | |
| fi |