diff options
author | Son HO | 2024-04-23 16:37:54 +0200 |
---|---|---|
committer | GitHub | 2024-04-23 16:37:54 +0200 |
commit | f3007820a21d11721507f5054b30bf5ae99a7b95 (patch) | |
tree | 8c84f338a6b86dd146500e18708594a0e449c880 /flake.nix | |
parent | 008596885544999b159244528c5a3b2a17151721 (diff) | |
parent | 10e5ca4c48c1d5729ee877612b7d95dfe2636159 (diff) |
Merge pull request #154 from AeneasVerif/ci-fmt
ci: check code formatting and forbid warnings
Diffstat (limited to 'flake.nix')
-rw-r--r-- | flake.nix | 21 |
1 files changed, 20 insertions, 1 deletions
@@ -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; }; }); } |