check-world.yml

name: Check world (build F* and all projects)

# This workflow builds/checks F* and a selection of subprojects
# depending on it.
#
# It is meant to test if an F* patch impacts other projects heavily or
# not. Jobs can (and will) run in parallel if the dependencies allow,
# using (mostly) Github hosted runners which are small-ish 4 core VMs.
#
# The steps are containerized and running on a docker container
# 'mtzguido/fstar-base-testing` built from .docker/nu_base.Dockerfile
# (FIXME: it needs a big cleanup and should go into an FStarLang
# namespace)
#
# Self-hosted runners *can* be used, and it's desirable to do it for
# things like HACL* or everparse that take really long on Github VMs
# (build-hacl takes ~1h50m on github runners, ~20m on a new-ish 16-core
# 32-thread desktop). HOWEVER, Github actions seems to be incredibly
# stupid in bind mounting the workspace for the job from the current
# directory of the runner, which means the workspace has the UID of the
# user that started the runner, but the steps of the job run inside the
# runner with the UID of the docker user. If these UIDs differ, the job
# will quickly fail to do anything and break. I'm not sure what the
# canonical fix is here, I think this is insane. FIXME
#
# We also use some custom actions. They are all not very well documented
# and not robust, so think twice (or ask) before using elsewhere!
# - mtzguido/set-opam-env:
#   this sets up the opam environment for the following steps
#   (`eval $(opam env)` will not cut it, nor will `opam env >> $GITHUB_ENV`)
#
# - mtzguido/gci-upload:
#   this uploads an artifact, much like github/upload-artifact, but first
#   packages it up into a tarball to preserve permissions (like exec bits).
#   Again it's insane that github does not do this by default. The tarball
#   will anyways be zipped afterwards since all github artifacts are zipped,
#   and will show up in the workflow run page.
#   It takes an optional 'extra' for argments to tar, that we use to ignore
#   some directories. It also ignores .git by default.
#   The 'hometag' is a way to set home variables when downloading the artifacts.
#
# - mtzguido/gci-download:
#   The companion to gci-upload. It will download the zipped tarball, unzip,
#   and extract into a directory named like the artifact. If the gci-upload had
#   a 'hometag: FOO', then the client downloading the artifact will get FOO_HOME
#   set in the environment, equal to the directory where the artifact was extracted.
#   This means most jobs do
#
#     - uses: mtzguido/gci-download@master
#       with:
#         name: FStar
#
#   And get a working F* with FSTAR_HOME set in the FStar directory.
#
#
# Adding new jobs should be relatively easy. Just state dependencies in
# the 'needs', and start the job by fetching the required dependencies
# with gci-download, and then build. The examples below should serve
# as a guide. If possible, separate the building from the testing,
# since future jobs may need the built resource, but all tests are
# independent. (However note that there is an overhead to start a job,
# it's ~40s alone to start a container, so don't overdo it by splitting
# up too much).

on:
  # push:
  workflow_dispatch:
  workflow_call:

# TODO:
# Is there a way to set the default container?
# Move to the regular fstar-ci-base too

defaults:
  run:
    shell: bash

jobs:
  build-fstar:
    runs-on: ubuntu-latest
    container: mtzguido/fstar-base-testing
    steps:
      - name: Cleanup
        run: find . -delete
      - run: echo "HOME=/home/opam" >> $GITHUB_ENV
      - uses: mtzguido/set-opam-env@master

      - name: Checkout
        uses: actions/checkout@master
        with:
          path: FStar/

      - name: Prep
        run: |
          # In case we edited fstar.opam, install new deps here
          # This will most likely fail to like krml below, what's going on?
          # opam install --confirm-level=unsafe-yes --deps-only ./FStar/fstar.opam
      - name: Build
        run: make -C FStar -skj$(nproc)

      - uses: mtzguido/gci-upload@master
        with:
          name: FStar
          extra: --exclude=FStar/ocaml/_build
          hometag: FSTAR

  test-fstar:
    runs-on: ubuntu-latest
    container: mtzguido/fstar-base-testing
    needs: build-fstar
    steps:
      - name: Cleanup
        run: find . -delete
      - run: echo "HOME=/home/opam" >> $GITHUB_ENV
      - uses: mtzguido/set-opam-env@master

      - uses: mtzguido/gci-download@master
        with:
          name: FStar

      - name: Test
        run: make -C FStar -skj$(nproc) ci-uregressions

  test-fstar-boot:
    runs-on: ubuntu-latest
    container: mtzguido/fstar-base-testing
    # needs: build-fstar
    # ^ This does not really depend on the previous job, but this can be
    # enabled if we wanted to sequentialize them for whatever reason.
    #   We start from scratch since we need a git repo to check the
    # diff, and that is not contained in the artifact. We could just
    # take the ulib checked files from the artifact, if we really wanted
    # to, but checking ulib with ADMIT is quite fast anyway.
    steps:
      - name: Cleanup
        run: find . -delete
      - run: echo "HOME=/home/opam" >> $GITHUB_ENV
      - uses: mtzguido/set-opam-env@master

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

      - name: Bootstrap
        run: |
          make -C FStar -skj$(nproc) 1
          make -C FStar -skj$(nproc) full-bootstrap ADMIT=1

      - name: Check diff
        run: |
          cd FStar/
          ./.scripts/check-snapshot-diff.sh

      - uses: mtzguido/gci-upload@master
        with:
          name: FStar-boot
          path: FStar
          extra: --exclude=FStar/ocaml/_build
          hometag: FSTAR

  build-krml:
    runs-on: ubuntu-latest
    container: mtzguido/fstar-base-testing
    needs: build-fstar
    steps:
      - name: Cleanup
        run: find . -delete
      - run: echo "HOME=/home/opam" >> $GITHUB_ENV
      - uses: mtzguido/set-opam-env@master

      - uses: mtzguido/gci-download@master
        with:
          name: FStar

      - name: Checkout karamel
        uses: actions/checkout@master
        with:
          path: karamel/
          repository: FStarLang/karamel

      - name: Prep
        run: |
          # Fails mysteriously:
          #
          # Error:  Package conflict!
          #   * No agreement on the version of ocaml:
          #     - (invariant) -> ocaml-base-compiler = 4.14.2 -> ocaml = 4.14.2
          # No solution found, exiting
          #     - karamel -> fstar -> ocaml < 4.06.0
          #     You can temporarily relax the switch invariant with `--update-invariant'
          #   * No agreement on the version of ocaml-base-compiler:
          #     - (invariant) -> ocaml-base-compiler = 4.14.2
          #     - karamel -> fstar -> ocaml < 4.06.0 -> ocaml-base-compiler = 3.07+1
          #   * Missing dependency:
          #     - karamel -> fstar -> z3 = 4.8.5 -> conf-python-2-7
          #     depends on the unavailable system package 'python2.7'. Use `--no-depexts' to attempt installation anyway, or it is possible that a depext package name in the opam file is incorrect.
          #   * Missing dependency:
          #     - karamel -> fstar -> ocaml < 4.06.0 -> ocaml-variants >= 3.11.1 -> ocaml-beta
          #     unmet availability conditions: 'enable-ocaml-beta-repository'
          #   * Missing dependency:
          #     - karamel -> fstar -> ocaml < 4.06.0 -> ocaml-variants >= 3.11.1 -> system-msvc
          #     unmet availability conditions: 'os = "win32"'
          #
          # opam install --confirm-level=unsafe-yes --deps-only ./karamel/karamel.opam

      - name: Build krml
        run: make -C karamel -skj$(nproc)

      # krml is a symlink to _build/default/src/Karamel.exe, but we want to exclude _build.
      # So, overwrite the link with the actual file.
      - name: Fix for symlink
        run: |
          cp --remove-destination $(realpath karamel/krml) karamel/krml

      - uses: mtzguido/gci-upload@master
        with:
          name: karamel
          extra: --exclude=karamel/_build
          hometag: KRML

  test-krml:
    runs-on: ubuntu-latest
    container: mtzguido/fstar-base-testing
    needs:
      - build-fstar
      - build-krml
    steps:
      - name: Cleanup
        run: find . -delete
      - run: echo "HOME=/home/opam" >> $GITHUB_ENV
      - uses: mtzguido/set-opam-env@master

      - uses: mtzguido/gci-download@master
        with:
          name: FStar

      - uses: mtzguido/gci-download@master
        with:
          name: karamel

      - name: Test
        run: make -C karamel -skj$(nproc) test

  build-steel:
    runs-on: ubuntu-latest
    container: mtzguido/fstar-base-testing
    needs:
      - build-fstar
    steps:
      - name: Cleanup
        run: find . -delete
      - run: echo "HOME=/home/opam" >> $GITHUB_ENV
      - uses: mtzguido/set-opam-env@master

      - uses: mtzguido/gci-download@master
        with:
          name: FStar

      - name: Checkout steel
        uses: actions/checkout@master
        with:
          path: steel/
          repository: FStarLang/steel

      - name: Build
        run: make -C steel -skj$(nproc)

      - uses: mtzguido/gci-upload@master
        with:
          name: steel
          hometag: STEEL

  test-steel:
    runs-on: ubuntu-latest
    container: mtzguido/fstar-base-testing
    needs:
      - build-fstar
      - build-krml
      - build-steel
    steps:
      - name: Cleanup
        run: find . -delete
      - run: echo "HOME=/home/opam" >> $GITHUB_ENV
      - uses: mtzguido/set-opam-env@master

      - uses: mtzguido/gci-download@master
        with:
          name: FStar

      - uses: mtzguido/gci-download@master
        with:
          name: karamel

      - uses: mtzguido/gci-download@master
        with:
          name: steel

      - name: Test
        run: make -C steel -skj$(nproc) test

  build-pulse:
    runs-on: ubuntu-latest
    container: mtzguido/fstar-base-testing
    needs:
      - build-fstar
    steps:
      - name: Cleanup
        run: find . -delete
      - run: echo "HOME=/home/opam" >> $GITHUB_ENV
      - uses: mtzguido/set-opam-env@master

      - uses: mtzguido/gci-download@master
        with:
          name: FStar

      - name: Checkout pulse
        uses: actions/checkout@master
        with:
          path: pulse/
          repository: FStarLang/pulse

      - name: Build
        run: make -C pulse -skj$(nproc)

      - uses: mtzguido/gci-upload@master
        with:
          name: pulse
          hometag: PULSE

  test-pulse-boot:
    runs-on: ubuntu-latest
    container: mtzguido/fstar-base-testing
    needs:
      - test-fstar-boot
    steps:
      - name: Cleanup
        run: find . -delete
      - run: echo "HOME=/home/opam" >> $GITHUB_ENV
      - uses: mtzguido/set-opam-env@master

      - uses: mtzguido/gci-download@master
        with:
          name: FStar-boot

      - name: Checkout pulse
        uses: actions/checkout@master
        with:
          path: pulse/
          repository: FStarLang/pulse

      - name: Build
        run: |
          # This is similar for 'make full-boot', but does not
          # check the library.
          make -C pulse/src -skj$(nproc) clean-snapshot
          make -C pulse/src -skj$(nproc) extract
          make -C pulse/src -skj$(nproc) build-ocaml

      - name: Check diff
        run: |
          cd pulse/
          ./.scripts/check-snapshot-diff.sh

  test-pulse:
    runs-on: ubuntu-latest
    container: mtzguido/fstar-base-testing
    needs:
      - build-fstar
      - build-krml
      - build-pulse
    steps:
      - name: Cleanup
        run: find . -delete
      - run: echo "HOME=/home/opam" >> $GITHUB_ENV
      - uses: mtzguido/set-opam-env@master

      - uses: mtzguido/gci-download@master
        with:
          name: FStar

      - uses: mtzguido/gci-download@master
        with:
          name: karamel

      - uses: mtzguido/gci-download@master
        with:
          name: pulse

      - name: Test
        run: make -C pulse -skj$(nproc) test

  build-hacl:
    # runs-on: [self-hosted, linux, big] # using a faster runner
    # NOTE: To use a self-hosted runner, we must make sure that
    # the runner is executing as UID 1001 (which is the one the
    # docker container uses) or it will be unable to write to its
    # workspace. This is simply a terrible design by github actions.
    # Somehow the cloud runners work regardless of the uid in
    # the container.
    runs-on: ubuntu-latest
    container: mtzguido/fstar-base-testing
    needs:
      - build-fstar
      - build-krml
    steps:
      - name: Cleanup
        run: find . -delete
      - run: echo "HOME=/home/opam" >> $GITHUB_ENV
      - uses: mtzguido/set-opam-env@master

      - uses: mtzguido/gci-download@master
        with:
          name: FStar

      - uses: mtzguido/gci-download@master
        with:
          name: karamel

      - name: Checkout hacl-star
        uses: actions/checkout@master
        with:
          path: hacl-star/
          repository: hacl-star/hacl-star

      - run: echo "HACL_HOME=$(pwd)/hacl-star" >> $GITHUB_ENV

      - name: Get Vale
        run: ./hacl-star/tools/get_vale.sh

      - name: Build
        run: |
          NPROC=$(nproc)
          if [ $NPROC -gt 16 ]; then NPROC=16; fi
          make -C hacl-star -skj${NPROC}

      - uses: mtzguido/gci-upload@master
        with:
          name: hacl-star
          hometag: HACL

  test-hacl:
    runs-on: ubuntu-latest
    container: mtzguido/fstar-base-testing
    needs:
      - build-fstar
      - build-krml
      - build-hacl
    steps:
      - name: Cleanup
        run: find . -delete
      - run: echo "HOME=/home/opam" >> $GITHUB_ENV
      - uses: mtzguido/set-opam-env@master

      - uses: mtzguido/gci-download@master
        with:
          name: FStar

      - uses: mtzguido/gci-download@master
        with:
          name: karamel

      - uses: mtzguido/gci-download@master
        with:
          name: hacl-star

      - name: Get Vale (again)
        run: ./hacl-star/tools/get_vale.sh

      - name: Test
        run: make -C hacl-star -skj$(nproc) test

  build-everparse:
    runs-on: ubuntu-latest
    container: mtzguido/fstar-base-testing
    needs:
      - build-fstar
      - build-krml
    steps:
      - name: Cleanup
        run: find . -delete
      - run: echo "HOME=/home/opam" >> $GITHUB_ENV
      - uses: mtzguido/set-opam-env@master

      - uses: mtzguido/gci-download@master
        with:
          name: FStar

      - uses: mtzguido/gci-download@master
        with:
          name: karamel

      - name: Checkout everparse
        uses: actions/checkout@master
        with:
          path: everparse/
          repository: project-everest/everparse

      - name: Build
        run: |
          NPROC=$(nproc)
          if [ $NPROC -gt 16 ]; then NPROC=16; fi
          make -C everparse -skj${NPROC}

      - uses: mtzguido/gci-upload@master
        with:
          name: everparse
          hometag: EVERPARSE

  test-everparse:
    runs-on: ubuntu-latest
    container: mtzguido/fstar-base-testing
    needs:
      - build-fstar
      - build-krml
      - build-everparse
    steps:
      - name: Cleanup
        run: find . -delete
      - run: echo "HOME=/home/opam" >> $GITHUB_ENV
      - uses: mtzguido/set-opam-env@master

      - uses: mtzguido/gci-download@master
        with:
          name: FStar

      - uses: mtzguido/gci-download@master
        with:
          name: karamel

      - uses: mtzguido/gci-download@master
        with:
          name: everparse

      - name: Test
        run: make -C everparse -skj$(nproc) test

  build-merkle-tree:
    runs-on: ubuntu-latest
    container: mtzguido/fstar-base-testing
    needs:
      - build-fstar
      - build-krml
      - build-hacl
    steps:
      - name: Cleanup
        run: find . -delete
      - run: echo "HOME=/home/opam" >> $GITHUB_ENV
      - uses: mtzguido/set-opam-env@master

      - uses: mtzguido/gci-download@master
        with:
          name: FStar

      - uses: mtzguido/gci-download@master
        with:
          name: karamel

      - uses: mtzguido/gci-download@master
        with:
          name: hacl-star

      - name: Checkout merkle-tree
        uses: actions/checkout@master
        with:
          path: merkle-tree/
          repository: hacl-star/merkle-tree

      - name: Build
        run: |
          NPROC=$(nproc)
          if [ $NPROC -gt 16 ]; then NPROC=16; fi
          make -C merkle-tree -skj${NPROC} dist/libmerkletree.a

      - uses: mtzguido/gci-upload@master
        with:
          name: merkle-tree

  test-merkle-tree:
    runs-on: ubuntu-latest
    container: mtzguido/fstar-base-testing
    needs:
      - build-fstar
      - build-krml
      - build-hacl
      - build-merkle-tree
    steps:
      - name: Cleanup
        run: find . -delete
      - run: echo "HOME=/home/opam" >> $GITHUB_ENV
      - uses: mtzguido/set-opam-env@master

      - uses: mtzguido/gci-download@master
        with:
          name: FStar

      - uses: mtzguido/gci-download@master
        with:
          name: karamel

      - uses: mtzguido/gci-download@master
        with:
          name: hacl-star

      - uses: mtzguido/gci-download@master
        with:
          name: merkle-tree

      - name: Test
        run: make -C merkle-tree -skj$(nproc) test

  build-mitls-fstar:
    runs-on: ubuntu-latest
    container: mtzguido/fstar-base-testing
    needs:
      - build-fstar
      - build-krml
      - build-hacl
      - build-everparse
    steps:
      - name: Cleanup
        run: find . -delete
      - run: echo "HOME=/home/opam" >> $GITHUB_ENV
      - uses: mtzguido/set-opam-env@master

      - uses: mtzguido/gci-download@master
        with:
          name: FStar

      - uses: mtzguido/gci-download@master
        with:
          name: karamel

      - uses: mtzguido/gci-download@master
        with:
          name: everparse

      - uses: mtzguido/gci-download@master
        with:
          name: hacl-star

      - name: Checkout mitls-fstar
        uses: actions/checkout@master
        with:
          path: mitls-fstar/
          repository: project-everest/mitls-fstar

      - name: Build
        run: make -C mitls-fstar/src/tls -skj$(nproc)

      - uses: mtzguido/gci-upload@master
        with:
          name: mitls-fstar
          hometag: MITLS

  test-mitls-fstar:
    runs-on: ubuntu-latest
    container: mtzguido/fstar-base-testing
    needs:
      - build-fstar
      - build-krml
      - build-hacl
      - build-everparse
      - build-mitls-fstar
    steps:
      - name: Cleanup
        run: find . -delete
      - run: echo "HOME=/home/opam" >> $GITHUB_ENV
      - uses: mtzguido/set-opam-env@master

      - uses: mtzguido/gci-download@master
        with:
          name: FStar

      - uses: mtzguido/gci-download@master
        with:
          name: karamel

      - uses: mtzguido/gci-download@master
        with:
          name: everparse

      - uses: mtzguido/gci-download@master
        with:
          name: hacl-star

      - uses: mtzguido/gci-download@master
        with:
          name: mitls-fstar

      - name: Build
        run: make -C mitls-fstar/src/tls -skj$(nproc) test


  ### Nix jobs, for some Inria projects
  #
  # NOTE: these jobs are not containerized
  # 1- it should not be needed since Nix takes care of isolating the environment
  # 2- it would actually fail to setup Nix due to permissions in the container, and I haven't
  #    found a clear reference on what the permissions/uids should be.
  #
  # The fstar-nix job is here to
  # 1- Test the nix build in this workflow too
  # 2- Reuse the built F* in the following projects, via the magic-nix-cache (note the 'needs')

  fstar-nix:
    runs-on: ubuntu-latest
    steps:
    - uses: actions/checkout@v4
    - uses: DeterminateSystems/nix-installer-action@main
    - uses: DeterminateSystems/magic-nix-cache-action@main
    - name: Build
      run: nix build -L

  comparse:
    needs: fstar-nix
    runs-on: ubuntu-latest
    steps:
      - uses: DeterminateSystems/nix-installer-action@main
      - uses: DeterminateSystems/magic-nix-cache-action@main

      - uses: actions/checkout@master
        with:
          repository: TWal/comparse

      - name: Update fstar flake and check
        run: |
          nix flake update --update-input fstar-flake --override-input fstar-flake "github:${{github.repository}}?rev=${{github.sha}}"
          nix flake check

  dy-star:
    needs: fstar-nix
    runs-on: ubuntu-latest
    steps:
      - uses: DeterminateSystems/nix-installer-action@main
      - uses: DeterminateSystems/magic-nix-cache-action@main

      - uses: actions/checkout@master
        with:
          repository: REPROSEC/dolev-yao-star-extrinsic

      - name: Update fstar flake and check
        run: |
          nix flake update --update-input fstar-flake --override-input fstar-flake "github:${{github.repository}}?rev=${{github.sha}}"
          nix flake check

  mls-star:
    needs: fstar-nix
    runs-on: ubuntu-latest
    steps:
      - uses: DeterminateSystems/nix-installer-action@main
      - uses: DeterminateSystems/magic-nix-cache-action@main

      - uses: actions/checkout@master
        with:
          repository: Inria-Prosecco/mls-star

      - name: Update fstar flake and check
        run: |
          nix flake update --update-input fstar-flake --override-input fstar-flake "github:${{github.repository}}?rev=${{github.sha}}"
          nix flake check