Merge pull request #394 from AeneasVerif/son/fix #1646
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
| on: | |
| # Run the checks on any push to any branch of the repo that doesn't start with `_`. | |
| push: | |
| branches: | |
| - main | |
| # Run the check for any pull request. The check is run on a merge between the | |
| # PR commit and the `main` branch at the time of running the check. | |
| pull_request: | |
| # Runs the check when a PR is added to the merge queue. | |
| merge_group: | |
| # Makes it possible to run the forkflow by hand from GItHub's interface. | |
| workflow_dispatch: | |
| # Cancel previous versions of this job that are still running. | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| nix: | |
| #runs-on: ubuntu-latest | |
| runs-on: [self-hosted, linux, nix] | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - run: nix build -L .#checks.x86_64-linux.aeneas-check-tidiness | |
| - run: nix build -L .#checks.x86_64-linux.check-charon-pin | |
| - run: nix build -L .#aeneas | |
| - run: nix build -L .#checks.x86_64-linux.default | |
| diff_lean_files: | |
| runs-on: [self-hosted, linux, nix] | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 # deep clone in order to get access to other commits | |
| - id: skip_check | |
| run: | | |
| # Compares this version with `main`, and checks whether the lean files changed. | |
| if git diff origin/main --quiet -- tests/lean && git diff origin/main --quiet -- backends/lean; then | |
| echo 'lean files were not changed in this PR.' | |
| echo "CHECK_LEAN=false" >> "$GITHUB_ENV" | |
| else | |
| echo 'lean files were changed in this PR.' | |
| echo "CHECK_LEAN=true" >> "$GITHUB_ENV" | |
| fi | |
| outputs: | |
| check_lean: ${{ env.CHECK_LEAN }} | |
| lean: | |
| needs: [diff_lean_files] | |
| runs-on: [self-hosted, linux, nix] | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - if: needs.diff_lean_files.outputs.check_lean == 'true' | |
| # Lean cannot run its tests in the nix sandbox because `elan` will download things | |
| run: nix develop --command bash -c "cd tests/lean && make" | |
| charon-pin-is-forward: | |
| runs-on: [self-hosted, linux, nix] | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 # deep clone in order to get access to other commits | |
| - run: nix develop --command ./scripts/ci-check-charon-pin-is-forward.sh | |
| charon-pin-is-merged: | |
| runs-on: [self-hosted, linux, nix] | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 # deep clone in order to get access to other commits | |
| - run: nix develop --command ./scripts/ci-check-charon-pin-is-merged.sh | |
| userdocs: | |
| runs-on: [self-hosted, linux, nix] | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - run: nix build '.?dir=docs/user'#book | |
| # TODO: test the Lean examples code via nix build '.?dir=docs/user'#test or something similar. |