Check world (build F* and all projects) #45
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 |