diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ab55f9db4..e6bf55468 100644 --- 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 index a0cff6fb6..2ea81b507 100644 --- 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 index fbc45833d..6c895e839 100644 --- 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 index 71f63cd35..d39667ba0 100644 --- a/flake.nix +++ b/flake.nix @@ -26,24 +26,27 @@ 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; + cargoArtifacts = craneLib.buildDepsOnly { src = cleanedUpSrc; }; + }; + + charon = craneLib.buildPackage (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 { @@ -207,6 +210,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 +249,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; }; }); }