on:
  push:
    branches-ignore: [ '_**' ]
  pull_request:
  workflow_dispatch:

jobs:
  nix:
    #runs-on: ubuntu-latest
    runs-on: [self-hosted, linux, nix]
    steps:
      #- uses: cachix/install-nix-action@v22
      - uses: actions/checkout@v4
      - run: nix build -L .#checks.x86_64-linux.aeneas-check-tidiness
      - run: nix build -L .#aeneas
      - run: nix build -L .#checks.x86_64-linux.aeneas-tests
      - run: nix build -L .#checks.x86_64-linux.aeneas-verify-fstar
      - run: nix build -L .#checks.x86_64-linux.aeneas-verify-coq
      - run: nix build -L .#checks.x86_64-linux.aeneas-verify-hol4
      # Lean doesn't work with Nix
      #- run: nix build -L .#checks.x86_64-linux.aeneas-verify-lean
  lean: # Lean isn't supported by Nix, so we put it in a different job
    runs-on: [ubuntu-latest]
    steps:
      # Install curl
      - run: sudo apt update && sudo apt install curl
      # Install Elan (https://leanprover-community.github.io/install/linux.html) and Lean in
      # non-interactive mode:
      - run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | bash -s -- -y
      # Checkout the repo and download it to the runner
      - name: Checkout
        uses: actions/checkout@v4
      # Verify - note that we need to update the environment with `source` so
      # that the lake binary is in the path.
      - run: source ~/.profile && cd tests/lean && make