ci-cn-spec-testing.yml

name: CN Spec Testing

on:
  pull_request:
  push:
    branches:
      - master

env:
  CERBERUS_IMAGE_ID: ghcr.io/rems-project/cerberus/cn:release

# cancel in-progress job when a new push is performed
concurrency:
  group: ci-${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true

jobs:
  build:
    strategy:
      matrix:
        # version: [4.12.0, 4.14.1]
        version: [4.14.1]


    runs-on: ubuntu-22.04

    steps:

    - name: Checkout Cerberus 
      uses: actions/checkout@v4

    - name: System dependencies (ubuntu)
      run: |
        sudo apt-get install build-essential libgmp-dev z3 opam cmake lcov
        wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key|sudo apt-key add -
        sudo add-apt-repository "deb http://apt.llvm.org/jammy/ llvm-toolchain-jammy-19 main"
        sudo add-apt-repository "deb-src http://apt.llvm.org/jammy/ llvm-toolchain-jammy-19 main"
        sudo apt-get update
        sudo apt-get install clang-format-19

    - name: Check LibCN code formatting
      run: |
        find runtime/libcn/ -iname '*.h' -o -iname '*.c' | xargs clang-format-19 --dry-run -Werror

    - name: Restore OPAM cache
      id: cache-opam-restore
      uses: actions/cache/restore@v4
      with:
        path: ~/.opam
        key: ${{ matrix.version }}
  
    - name: Setup OPAM
      if: steps.cache-opam-restore.outputs.cache-hit != 'true'
      run: |
        opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
        eval $(opam env --switch=${{ matrix.version }})
        opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released
        opam install --deps-only --yes ./cerberus-lib.opam
  
    - name: Save OPAM cache
      uses: actions/cache/save@v4
      if: steps.cache-opam-restore.outputs.cache-hit != 'true'
      with:
        path: ~/.opam
        key: ${{ matrix.version }}

    - name: Install Cerberus
      run: |
        opam switch ${{ matrix.version }}
        eval $(opam env --switch=${{ matrix.version }})
        opam pin --yes --no-action add cerberus-lib .
        opam pin --yes --no-action add cerberus .
        opam install --yes cerberus

    - name: Install CN
      run: |
        opam switch ${{ matrix.version }}
        eval $(opam env --switch=${{ matrix.version }})
        opam pin --yes --no-action add cn .
        opam install --yes cn

    - name: Run CN-runtime CI tests (Cerberus)
      run: |
        opam switch ${{ matrix.version }}
        eval $(opam env --switch=${{ matrix.version }})
        cd tests; ./run-cn-exec.sh

    - name: Checkout cn-tutorial
      uses: actions/checkout@v4
      with:
        repository: rems-project/cn-tutorial
        path: cn-tutorial
        ref: cn-runtime-testing # FIXME: remove once the branch is merged 

    - name: Run CN-runtime CI tests (CN tutorial)
      run: |
        opam switch ${{ matrix.version }}
        eval $(opam env --switch=${{ matrix.version }})
        cd cn-tutorial; ./runtime-test.sh 
        cd ..

    - name: Run CN-Test-Gen CI tests
      run: |
        opam switch ${{ matrix.version }}
        eval $(opam env --switch=${{ matrix.version }})
        cd tests; ./run-cn-test-gen.sh
    
    - name: Run CN-Seq-Test-Gen CI tests
      run: |
        opam switch ${{ matrix.version }}
        eval $(opam env --switch=${{ matrix.version }})
        cd tests; ./run-cn-seq-test-gen.sh