Check world (build F* and all projects) #47

Workflow file for this run

.github/workflows/check-world.yml at 738fbc0

	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

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Check world (build F* and all projects) #47

Workflow file

Check world (build F* and all projects) #47

Jobs

Run details

Workflow file for this run