ci.yml

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.