diff options
| -rw-r--r-- | .github/workflows/ci.yml | 1 | ||||
| -rw-r--r-- | Makefile | 3 | ||||
| -rw-r--r-- | flake.nix | 21 |
3 files changed, 23 insertions, 2 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 86b5b300..eeb92c51 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -30,6 +30,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,11 +30,29 @@ }; 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 formatted. Run `make format` to format the project files'. + exit 1 + fi + ''; + installPhase = "touch $out"; + }; aeneas = ocamlPackages.buildDunePackage { pname = "aeneas"; version = "0.1.0"; duneVersion = "3"; src = ./compiler; + OCAMLPARAM="_,warn-error=+A"; # Turn all warnings into errors. propagatedBuildInputs = [ easy_logging charon.packages.${system}.charon-ml ] ++ (with ocamlPackages; [ @@ -167,6 +185,7 @@ inherit aeneas aeneas-tests aeneas-verify-fstar aeneas-verify-coq - aeneas-verify-hol4; }; + aeneas-verify-hol4 + aeneas-check-tidiness; }; }); } |