diff options
| -rw-r--r-- | .github/workflows/ci.yml | 1 | ||||
| -rw-r--r-- | Makefile | 11 | ||||
| -rw-r--r-- | charon-pin | 2 | ||||
| -rw-r--r-- | flake.nix | 24 | ||||
| -rwxr-xr-x | scripts/update-charon-pin.sh | 7 |
5 files changed, 41 insertions, 4 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4826114e..eeb423b6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -36,6 +36,7 @@ jobs: steps: - uses: actions/checkout@v4 - run: nix build -L .#checks.x86_64-linux.aeneas-check-tidiness + - run: nix build -L .#checks.x86_64-linux.check-charon-pin - run: nix build -L .#aeneas - run: nix build -L .#checks.x86_64-linux.aeneas-tests - run: nix build -L .#checks.x86_64-linux.aeneas-verify-fstar @@ -77,6 +77,17 @@ build-bin-dir: build-bin build-lib doc: cd compiler && dune build @doc +# Fetches the latest commit from charon and updates `flake.lock` accordingly. +.PHONY: update-charon-pin +update-charon-pin: + nix flake lock --update-input charon + $(MAKE) charon-pin + +# Keep the commit revision in `./charon-pin` as well so that non-nix users can +# know which commit to use. +./charon-pin: flake.lock + nix-shell -p jq --run './scripts/update-charon-pin.sh' >> ./charon-pin + .PHONY: clean clean: clean-generated cd compiler && dune clean diff --git a/charon-pin b/charon-pin new file mode 100644 index 00000000..d2e70db4 --- /dev/null +++ b/charon-pin @@ -0,0 +1,2 @@ +# This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas. +1a205c55b02f3dff1ae238dfdac5a58d58de6006 @@ -2,8 +2,8 @@ description = "Aeneas"; inputs = { - # Remark: when adding inputs here, don't forget to also add them in the list - # of outputs below! + # Remark: when adding inputs here, don't forget to also add them in the + # arguments to `outputs` below! charon.url = "github:aeneasverif/charon"; flake-utils.follows = "charon/flake-utils"; nixpkgs.follows = "charon/nixpkgs"; @@ -41,7 +41,7 @@ ]; buildPhase = '' if ! dune build @fmt; then - echo 'ERROR: Code is not formatted. Run `make format` to format the project files'. + echo 'ERROR: Code is not formatted. Run `make format` to format the project files.' exit 1 fi ''; @@ -163,6 +163,21 @@ # The build doesn't generate anything installPhase = "touch $out"; }; + + check-charon-pin = pkgs.runCommand "aeneas-check-charon-pin" { + buildInputs = [ pkgs.jq ]; + } '' + CHARON_REV_FROM_FLAKE="$(jq -r .nodes.charon.locked.rev ${./flake.lock})" + CHARON_REV_FROM_PIN="$(tail -1 ${./charon-pin})" + if [[ "$CHARON_REV_FROM_FLAKE" != "$CHARON_REV_FROM_PIN" ]]; then + echo 'ERROR: The charon version in `flacke.lock` differs from the one in `charon-pin`.' + echo ' In `flake.lock`: '"$CHARON_REV_FROM_FLAKE" + echo ' In `charon-pin`: '"$CHARON_REV_FROM_PIN" + echo 'Use `make charon-pin` to update the `./charon-pin` file.' + exit 1 + fi + touch $out + ''; in { packages = { inherit aeneas; @@ -186,6 +201,7 @@ aeneas-verify-fstar aeneas-verify-coq aeneas-verify-hol4 - aeneas-check-tidiness; }; + aeneas-check-tidiness + check-charon-pin; }; }); } diff --git a/scripts/update-charon-pin.sh b/scripts/update-charon-pin.sh new file mode 100755 index 00000000..418602b8 --- /dev/null +++ b/scripts/update-charon-pin.sh @@ -0,0 +1,7 @@ +#!/usr/bin/env bash +if ! which jq 2> /dev/null 1>&2; then + echo 'Error: command `jq` not found.' + exit 1 +fi +echo '# This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.' > ./charon-pin +jq -r .nodes.charon.locked.rev flake.lock >> ./charon-pin |