ci.yml

name: CI
on:
  push:
    branches-ignore:
    - _**
  pull_request:
  workflow_dispatch:
    inputs:
      nocache:
        description: Do not use stored OPAM cache
        type: boolean
        default: false
  schedule:
    - cron: '0 0 * * *'

defaults:
  run:
    shell: bash

jobs:
  build-deps:
    runs-on: ubuntu-latest
    steps:

      - name: Setup ocaml
        uses: ocaml/setup-ocaml@v3
        with:
           ocaml-compiler: 5.3.0

      - uses: actions/checkout@master
        with:
          path: karamel

      # We keep the OPAM state fully cached between runs, and rely on OPAM to
      # update itself. This means we don't build F* again if it doesn't change.
      # The nightly build will start from scratch.
      - name: Try restore OPAM state
        if: ${{ inputs.nocache != 'true' && github.event_name != 'schedule' }}
        uses: actions/cache/restore@v4
        with:
          path: _opam
          key: opam-${{ runner.os }}-${{ runner.arch }}-fstar1-${{ github.run_id }}
          restore-keys: |
            opam-${{ runner.os }}-${{ runner.arch }}-fstar1-
            opam-${{ runner.os }}-${{ runner.arch }}-

      # Build F*, from the fstar1 branch.
      - run: opam update
      - run: opam pin -n fstar git+https://github.com/FStarLang/FStar#fstar1
      - run: opam install fstar

      # Install karamel deps
      - run: opam install --deps-only karamel/karamel.opam
      - run: opam install ctypes ctypes-foreign # not in deps?

      - name: Build EverParse opam dependencies
        run: |
          opam install re
          # FIXME: we should rather do the following:
          # opam install --deps-only ./everparse/opt/everparse-deps.opam
          # But the maximum available version of sexplib with ocaml 4.x
          # is 0.16, which requires sexplib0 0.16,
          # whereas F* installs sexplib0 0.17
          # Fortunately, sexplib is required only by 3d,
          # and so far no Karamel regression test suite for EverParse
          # requires 3d

      # Paranoid delete before saving. Note: run_id is constant across reruns.
      - name: Delete OPAM state if it already existed
        run: |
          gh cache delete opam-${{ runner.os }}-${{ runner.arch }}-fstar1-${{ github.run_id }} || true
        env:
          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
          GH_REPO: ${{ github.repository }}
          BRANCH: ${{ github.ref }}

      - name: Save OPAM state
        uses: actions/cache/save@v4
        with:
          path: _opam
          key: opam-${{ runner.os }}-${{ runner.arch }}-fstar1-${{ github.run_id }}

  build-and-test:
    needs: build-deps
    runs-on: ubuntu-latest
    steps:
      - name: Install Z3 with script
        run: |
          wget https://raw.githubusercontent.com/FStarLang/FStar/refs/heads/master/.scripts/get_fstar_z3.sh -O get_fstar_z3.sh
          chmod +x get_fstar_z3.sh
          ./get_fstar_z3.sh /usr/local/bin
       # If these fail, stop right now.
      - run: which z3-4.8.5
      - run: which z3-4.13.3

      - name: Setup ocaml
        uses: ocaml/setup-ocaml@v3
        with:
           ocaml-compiler: 5.3.0

      - uses: actions/checkout@master
        with:
          path: karamel

      - name: Restore OPAM state
        uses: actions/cache/restore@v4
        with:
          fail-on-cache-miss: true # should never happen, cache was filled by build-deps
          path: _opam
          key: opam-${{ runner.os }}-${{ runner.arch }}-fstar1-${{ github.run_id }}

      - uses: actions/setup-node@v4
        with:
          node-version: 16

      - name: Karamel CI
        working-directory: karamel
        run: |
          eval $(opam env)
          . $HOME/.cargo/env
          export OCAMLRUNPARAM=b
          make -kj$(nproc)
          make -kj$(nproc) -C test everything

      - name: Build book
        working-directory: karamel
        run: |
          eval $(opam env)
          sudo apt-get install -y python3-sphinx python3-sphinx-rtd-theme
          make -C book html

      - name: Upload book artifact
        uses: actions/upload-artifact@v4
        with:
          path: karamel/book/_build
          name: book

  # EverParse (CBOR, COSE) regressions
  test-everparse:
    needs: build-deps
    runs-on: ubuntu-latest
    steps:

      - name: Setup ocaml
        uses: ocaml/setup-ocaml@v3
        with:
           ocaml-compiler: 5.3.0

      - uses: actions/checkout@master
        with:
          path: karamel

      - name: Restore OPAM state
        uses: actions/cache/restore@v4
        with:
          fail-on-cache-miss: true # should never happen, cache was filled by build-deps
          path: _opam
          key: opam-${{ runner.os }}-${{ runner.arch }}-fstar1-${{ github.run_id }}

      - name: Setup environment
        run: |
          echo "KRML_HOME=$(pwd)/karamel" >> $GITHUB_ENV
          echo "EVERPARSE_USE_KRML_HOME=1" >> $GITHUB_ENV
          echo "ADMIT=1" >> $GITHUB_ENV

      - name: Restore EverParse cache if it exists
        uses: actions/cache/restore@v4
        with:
          path: everparse
          key: everparse-${{ runner.os }}-${{ runner.arch }}-${{ github.run_id }}
          restore-keys: |
            everparse-${{ runner.os }}-${{ runner.arch }}-

      # NOTE: we use `git checkout` instead of actions/checkout,
      # because of `git pull` below
      - name: Clone EverParse if it does not exist
        run: |
          if ! [[ -d everparse ]] ; then git clone \
            https://github.com/project-everest/everparse ; fi

      # Need to build Karamel only at the last minute, since `opam
      # install` might recompile F*
      - name: Build Karamel
        working-directory: karamel
        run: |
          eval $(opam env)
          . $HOME/.cargo/env
          export OCAMLRUNPARAM=b
          OTHERFLAGS='--admit_smt_queries true' make -kj$(nproc)

      - name: Generate CBOR and COSE .krml files
        working-directory: everparse
        run: |
          git pull && make cbor-extract-krml cose-extract-krml -kj$(nproc)

      # Paranoid delete before saving. Note: run_id is constant across reruns.
      - name: Delete EverParse cache if it already existed
        run: |
          gh cache delete everparse-${{ runner.os }}-${{ runner.arch }}-${{ github.run_id }} || true
        env:
          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
          GH_REPO: ${{ github.repository }}
          BRANCH: ${{ github.ref }}

      - name: Save EverParse cache
        uses: actions/cache/save@v4
        with:
          path: everparse
          key: everparse-${{ runner.os }}-${{ runner.arch }}-${{ github.run_id }}

      - name: Generate CBOR snapshot with Karamel
        run: |
          make -C everparse cbor-snapshot -Otarget -kj$(nproc)
      - name: Test CBOR snapshot
        run: |
          make -C everparse cbor-test-unverified -Otarget -kj$(nproc)
      - name: Generate COSE snapshot with Karamel
        run: |
          make -C everparse cose-snapshot -Otarget -kj$(nproc)
      - name: Test COSE snapshot
        run: |
          make -C everparse cose-extracted-test -Otarget -kj$(nproc)

  # This is checked in parallel with no F* around. It checks that the
  # krllib snapshot builds, on several systems.
  build-krmllib:
    strategy:
      matrix:
        os:
          - ubuntu-22.04
          - ubuntu-24.04
          - macos-14
          - macos-15
        cc:
          - gcc
          - clang

    runs-on: ${{ matrix.os }}
    steps:
      - uses: actions/checkout@master
      - name: Build the checked-in krmllib
        run: |
          export CC=${{matrix.cc}}
          export KRML_INCLUDEDIR=$(pwd)/include
          export KRML_LIBDIR=$(pwd)/krmllib
          make -kj$(nproc) -C krmllib/dist/generic -f Makefile.basic

  build-and-test-pulse:
    runs-on: ubuntu-latest
    needs: build-deps
    steps:
      - name: Setup ocaml
        uses: ocaml/setup-ocaml@v3
        with:
           ocaml-compiler: 5.3.0

      # Note, we prefer to restore the -master cache, but if it doesn't exist,
      # we restore the latest normal one.
      - name: Restore OPAM state
        uses: actions/cache/restore@v4
        with:
          fail-on-cache-miss: true
          path: _opam
          key: opam-${{ runner.os }}-${{ runner.arch }}-master-${{ github.run_id }}
          restore-keys: |
            opam-${{ runner.os }}-${{ runner.arch }}-master-
            opam-${{ runner.os }}-${{ runner.arch }}-

      # Build F*, master branch
      - run: opam update
      - run: opam pin -n fstar git+https://github.com/FStarLang/FStar#master
      - run: opam install fstar

      # Save OPAM state, note master- in key.
      - name: Save OPAM state
        uses: actions/cache/save@v4
        with:
          path: _opam
          key: opam-${{ runner.os }}-${{ runner.arch }}-master-${{ github.run_id }}

      - name: Install Z3 with script
        run: |
          wget https://raw.githubusercontent.com/FStarLang/FStar/refs/heads/master/.scripts/get_fstar_z3.sh -O get_fstar_z3.sh
          chmod +x get_fstar_z3.sh
          ./get_fstar_z3.sh /usr/local/bin
       # If these fail, stop right now.
      - run: which z3-4.8.5
      - run: which z3-4.13.3

      - uses: actions/checkout@master
        with:
          path: karamel

      - uses: actions/setup-node@v4
        with:
          node-version: 16

      - run: echo "KRML_HOME=$(pwd)/karamel" >> $GITHUB_ENV

      - name: Karamel CI (test-pulse)
        working-directory: karamel
        run: |
          eval $(opam env)
          export OCAMLRUNPARAM=b
          make -kj$(nproc) test-pulse

  test-eurydice:
    runs-on: ubuntu-latest
    steps:
      - name: Install Nix
        uses: DeterminateSystems/nix-installer-action@main

      - name: Setup Cachix
        uses: cachix/cachix-action@v15
        with:
          name: hacl

      - name: Build and test Eurydice against this Karamel
        run: |
          nix build -L --no-link \
            "github:AeneasVerif/eurydice#checks.x86_64-linux.default" \
            --override-input karamel "github:FStarLang/karamel/$GITHUB_SHA"

  # A single no-op job to use for branch protection
  ciok:
    runs-on: ubuntu-latest
    if: ${{ cancelled() || contains(needs.*.result, 'cancelled') || contains(needs.*.result, 'failure') }}
    needs:
      - build-and-test
      - build-and-test-pulse
      - build-krmllib
      - test-eurydice
    steps:
      # Note: this only runs when a dependency fails. If they all succeed,
      # this jobs is skipped, which counts as a success.
      # https://github.com/actions/runner/issues/2566
      - run: exit 1

  publish_book:
    runs-on: ubuntu-latest
    if: ${{ github.ref == 'refs/heads/master' }}
    needs: build-and-test
    steps:
      - uses: actions/checkout@master
      - uses: actions/download-artifact@v4
        with:
          name: book
          path: book/_build

      - name: Configure git
        run: |
          git config --global user.name "Dzomo, the Everest Yak"
          git config --global user.email "24394600+dzomo@users.noreply.github.com"

      - run: .scripts/publish_tutorial.sh
        env:
          DZOMO_GITHUB_TOKEN: ${{secrets.DZOMO_GITHUB_TOKEN}}