ci.yml

on:
  # Run the checks on the latest commit from `main`
  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: cachix/install-nix-action@v22
      - uses: actions/checkout@v4
      - run: nix build -L .#charon
      - run: nix build -L .#charon-ml
      - run: nix flake check -L

  check-version-number:
    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-version-number.sh

  aeneas:
    needs: [nix]
    runs-on: [self-hosted, linux, nix]
    steps:
      - run: |
          nix build --refresh -L 'github:aeneasverif/aeneas#checks.x86_64-linux.aeneas-tests' \
              --override-input charon github:aeneasverif/charon/${{ github.sha }} \
              --override-input charon/rust-overlay github:oxalica/rust-overlay/master

  eurydice:
    needs: [nix]
    runs-on: [self-hosted, linux, nix]
    steps:
      - uses: actions/checkout@v4
        with:
          repository: Inria-Prosecco/circus-green
      - run: |
          nix flake lock --refresh --update-input eurydice
          nix flake lock --override-input charon github:aeneasverif/charon/${{ github.sha }}
          ./check.sh eurydice

  kyber:
    needs: [eurydice]
    runs-on: [self-hosted, linux, nix]
    steps:
      - uses: actions/checkout@v4
        with:
          repository: Inria-Prosecco/circus-green
      - run: |
          nix flake lock --refresh --update-input eurydice
          nix flake lock --override-input charon github:aeneasverif/charon/${{ github.sha }}
          ./check.sh ml-kem-small