diff options
Diffstat (limited to '')
| -rw-r--r-- | .github/workflows/ci.yml | 1 | ||||
| -rw-r--r-- | Makefile | 3 | ||||
| -rw-r--r-- | flake.nix | 20 |
3 files changed, 22 insertions, 2 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6b5aacf0..66fda7af 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -11,6 +11,7 @@ jobs: steps: #- uses: cachix/install-nix-action@v22 - uses: actions/checkout@v4 + - run: nix build -L .#checks.x86_64-linux.aeneas-check-tidiness - 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 @@ -113,7 +113,8 @@ verify: # Reformat the project .PHONY: format format: - cd compiler && dune build @fmt --auto-promote + @# `|| `true` because the command returns an error if it changed anything, which we don't care about. + cd compiler && dune fmt || true # The commands to run Charon to generate the .llbc files ifeq (, $(REGEN_LLBC)) @@ -30,6 +30,23 @@ }; buildInputs = [ ocamlPackages.calendar ]; }; + + aeneas-check-tidiness = pkgs.stdenv.mkDerivation { + name = "aeneas-check-tidiness"; + src = ./compiler; + buildInputs = [ + ocamlPackages.dune_3 + ocamlPackages.ocaml + ocamlPackages.ocamlformat + ]; + buildPhase = '' + if ! dune build @fmt; then + echo 'ERROR: Code is not fmrmatted. Run `make format` to format the project files'. + exit 1 + fi + ''; + installPhase = "touch $out"; + }; aeneas = ocamlPackages.buildDunePackage { pname = "aeneas"; version = "0.1.0"; @@ -167,6 +184,7 @@ inherit aeneas aeneas-tests aeneas-verify-fstar aeneas-verify-coq - aeneas-verify-hol4; }; + aeneas-verify-hol4 + aeneas-check-tidiness; }; }); } |