name: CI

permissions: read-all
on:
  push:
    branches: ["main"]
  pull_request:
    branches: ["main"]
  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

env:
  CHARON_REPO: AeneasVerif/charon

jobs:
  build:
    strategy:
      matrix:
        operating-system: [macos-latest, macos-13]
    runs-on: ${{ matrix.operating-system }}
    steps:
      # Setup steps: checkout, z3, node, ocaml and opam
      - uses: actions/checkout@v4
      - name: Setup Z3
        uses: cda-tum/setup-z3@v1
        id: z3
      - name: Setup node
        uses: actions/setup-node@v4
        with:
          cache: "yarn"
      - name: Setup OCaml
        uses: ocaml/setup-ocaml@v3
        with:
          ocaml-compiler: 5.3.0
          dune-cache: true
          opam-pin: false
      - name: Restore opam cache
        uses: actions/cache@v4
        with:
          path: _opam
          key: ${{ runner.os }}-${{ runner.arch }}-opam-${{ hashFiles('*.opam') }}
          restore-keys: |
            ${{ runner.os }}-${{ runner.arch }}-opam-
      - run: opam update
      # OCaml build
      - name: setup dependencies
        run: make ocaml-deps
      - name: Build OCaml stuff
        run: make ocaml
      - name: Check formatting
        run: make ocaml-format-check

      # Install Rust and Charon
      - name: Get Charon's commit hash
        run: |
          HASH=$(opam pin | grep "charon\." | sed -E 's/.*#([a-f0-9]{40}).*/\1/' | head -n 1)
          echo "CHARON_COMMIT_HASH=$HASH" >> $GITHUB_ENV
      - name: Get Rust toolchain
        run: curl https://raw.githubusercontent.com/$CHARON_REPO/$CHARON_COMMIT_HASH/charon/rust-toolchain > rust-toolchain
      - name: Setup Rust
        uses: actions-rust-lang/setup-rust-toolchain@v1
      - name: Restore Charon cache
        uses: actions/cache@v4
        id: restore-charon-cache
        with:
          path: charon-bin
          key: ${{ runner.os }}-${{ runner.arch }}-charon-${{ env.CHARON_COMMIT_HASH }}
      - name: Install charon if not cached
        run: |
          brew install make
          cd ..
          mkdir charon
          cd charon
          git init
          git remote add origin https://github.com/$CHARON_REPO.git
          git fetch --depth=1 origin $CHARON_COMMIT_HASH
          git checkout $CHARON_COMMIT_HASH
          gmake build-dev-charon-rust
          cp -r bin ../soteria/charon-bin
        if: ${{ !steps.restore-charon-cache.outputs.cache-hit }}
      - name: Add Charon to path
        run: echo "$PWD/charon-bin/" >> $GITHUB_PATH

      # Run tests
      - name: Test
        run: Make ocaml-test

      # Building js stuff
      - name: Install JS dependencies
        run: yarn install
      - name: Build JS stuff
        run: yarn compile

      # Packaging OCaml distribution and sending it as artifact
      - name: OCaml zip file creation
        run: make package
      - name: Upload zip file
        uses: actions/upload-artifact@v4
        with:
          name: ${{ matrix.operating-system }}-package
          path: package
          if-no-files-found: error
      - name: Opam Cleanup
        run: opam clean -a -r

  test-package:
    strategy:
      matrix:
        operating-system: [macos-latest, macos-13]
    runs-on: ${{ matrix.operating-system }}
    needs: build
    steps:
      - name: checkout Collections-C, version where we find a bug
        uses: actions/checkout@v4
        with:
          repository: srdja/Collections-C
          ref: 67a094035b3f7159cf3f9af82c55ae63fcb86a34
      - name: Create compilation database
        run: |
          mkdir -p build
          cd build
          cmake -DCMAKE_EXPORT_COMPILE_COMMANDS=1 ..
      - name: Download package
        uses: actions/download-artifact@v4
        with:
          name: ${{ matrix.operating-system }}-package
      - name: Add executable permissions
        run: |
          chmod +x ./bin/soteria-c
          chmod +x ./bin/z3
      - run: CERB_INSTALL_PREFIX=$(pwd) DYLD_LIBRARY_PATH=./lib:$DYLD_LIBRARY_PATH ./bin/soteria-c capture-db build/compile_commands.json
        env:
          SOTERIA_Z3_PATH: ./bin/z3
          SOTERIA_AUTO_INCLUDE_PATH: ./lib/soteria-c
          SOTERIA_SOLVER_TIMEOUT: 100