Merge pull request #144 from AeneasVerif/ci-checks

ci: check formatting and forbid compilation warnings
AeneasVerif · Apr 23, 2024 · b9e70f5 · b9e70f5
2 parents 0425143 + 7a50094
commit b9e70f5
Show file tree

Hide file tree

Showing 4 changed files with 46 additions and 20 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -31,7 +31,5 @@ jobs:
       #- uses: cachix/install-nix-action@v22
       - uses: actions/checkout@v4
       - run: nix build -L .#charon
-      - run: nix build -L .#checks.x86_64-linux.tests
-      - run: nix build -L .#checks.x86_64-linux.tests-polonius
       - run: nix build -L .#charon-ml
-      - run: nix build -L .#checks.x86_64-linux.charon-ml-tests
+      - run: nix flake check -L
diff --git a/Makefile b/Makefile
@@ -9,6 +9,11 @@ default: build-charon-rust
 .PHONY: all
 all: build test nix
 
+.PHONY: format
+format:
+	cd charon && $(MAKE) format
+	cd charon-ml && $(MAKE) format
+
 # We use Rust nightly in order to:
 # - be able to write a Rustc plugin
 # - use Polonius in some tests

diff --git a/charon-ml/Makefile b/charon-ml/Makefile
@@ -17,7 +17,7 @@ tests: build copy-tests
 # Reformat the code
 .PHONY: format
 format:
-	dune build @fmt --auto-promote
+	dune fmt
 
 .PHONY: copy-tests
 copy-tests:

diff --git a/flake.nix b/flake.nix
@@ -26,24 +26,29 @@
 
         rustToolchain = pkgs.rust-bin.fromRustupToolchainFile ./rust-toolchain.template;
         craneLib = (crane.mkLib pkgs).overrideToolchain rustToolchain;
-        charon =
-          let
-            # Clean up the source directory.
-            sourceFilter = path: type:
+
+        cleanedUpSrc = pkgs.lib.cleanSourceWith {
+          src = ./charon;
+          filter = path: type:
             (craneLib.filterCargoSources path type)
               || (pkgs.lib.hasPrefix (toString ./charon/tests) path)
               || (path == toString ./charon/rust-toolchain);
-            cleanedUpSrc = pkgs.lib.cleanSourceWith {
-              src = ./charon;
-              filter = sourceFilter;
-            };
-            cargoArtifacts = craneLib.buildDepsOnly { src = cleanedUpSrc; };
-          in craneLib.buildPackage {
-            src = cleanedUpSrc;
-            inherit cargoArtifacts;
-            # Check the `ui_llbc` files are correct instead of overwriting them.
-            cargoTestCommand = "IN_CI=1 cargo test --profile release";
-          };
+        };
+        craneArgs = {
+          src = cleanedUpSrc;
+          RUSTFLAGS="-D warnings"; # Turn all warnings into errors.
+        };
+
+        charon = craneLib.buildPackage (craneArgs // {
+          # It's important to pass the same `RUSTFLAGS` to dependencies otherwise we'll have to rebuild them.
+          cargoArtifacts = craneLib.buildDepsOnly craneArgs;
+          # Check the `ui_llbc` files are correct instead of overwriting them.
+          cargoTestCommand = "IN_CI=1 cargo test --profile release";
+        });
+
+        # Check rust files are correctly formatted.
+        charon-check-fmt = craneLib.cargoFmt craneArgs;
+
         tests =
           let cargoArtifacts = craneLib.buildDepsOnly { src = ./tests; };
           in craneLib.buildPackage {
@@ -187,6 +192,7 @@
             pname = "charon";
             version = "0.1.0";
             duneVersion = "3";
+            OCAMLPARAM="_,warn-error=+A"; # Turn all warnings into errors.
             preCheck = if doCheck then ''
               mkdir -p tests/serialized
               cp ${tests}/llbc/* tests/serialized
@@ -207,6 +213,23 @@
           };
         charon-ml = mk-charon-ml false;
         charon-ml-tests = mk-charon-ml true;
+
+        charon-ml-check-fmt = pkgs.stdenv.mkDerivation {
+          name = "charon-ml-check-fmt";
+          src = ./charon-ml;
+          buildInputs = [
+            ocamlPackages.dune_3
+            ocamlPackages.ocaml
+            ocamlPackages.ocamlformat
+          ];
+          buildPhase = ''
+            if ! dune build @fmt; then
+              echo 'ERROR: Ocaml code is not formatted. Run `make format` to format the project files'.
+              exit 1
+            fi
+          '';
+          installPhase = "touch $out";
+        };
       in {
         packages = {
           inherit charon charon-ml rustc-tests;
@@ -229,6 +252,6 @@
             self.packages.${system}.charon-ml
           ];
         };
-        checks = { inherit tests tests-polonius charon-ml-tests; };
+        checks = { inherit tests tests-polonius charon-ml-tests charon-check-fmt charon-ml-check-fmt; };
       });
 }