Merge pull request #385 from Nadrieril/ci

flake.nix

@@ -8,7 +8,6 @@
     flake-utils.follows = "charon/flake-utils";
     nixpkgs.follows = "charon/nixpkgs";
     fstar.url = "github:FStarLang/fstar";
-    flake-compat.url = "github:nix-community/flake-compat";
   };
 
   # Remark: keep the list of outputs in sync with the list of inputs above
@@ -179,15 +178,15 @@
         # reuse the build of ./backends/hol4.
         aeneas-verify-hol4 = pkgs.stdenv.mkDerivation {
           name = "aeneas_verify_hol4";
-          # Remark: we tried to filter the sources to only include ./backends/hol4
-          # and ./tests/hol4 (see comment below), but it didn't work
-          src = ./.;
-          # src = pkgs.lib.cleanSourceWith {
-          #   src = ./.;
-          #   filter = path: type:
-          #     pkgs.lib.hasPrefix (toString ./backends/hol4) path
-          #     || pkgs.lib.hasPrefix (toString ./tests/hol4) path;
-          # };
+          src = pkgs.lib.cleanSourceWith {
+            src = ./.;
+            filter = path: type:
+              # If we exclude these, the filter won't recurse into them.
+              path == toString ./backends || path == toString ./tests
+              || pkgs.lib.hasPrefix (toString ./backends/hol4) path
+              || pkgs.lib.hasPrefix (toString ./tests/hol4) path
+            ;
+          };
           buildInputs = [ pkgs.hol ];
           buildPhase = ''
             cd ./tests/hol4
@@ -198,14 +197,6 @@
           installPhase = "touch $out";
         };
 
-        aeneas-checks = pkgs.runCommand "aeneas-checks" { } ''
-          echo ${aeneas-tests}
-          echo ${aeneas-verify-coq}
-          echo ${aeneas-verify-fstar}
-          echo ${aeneas-verify-hol4}
-          touch $out
-        '';
-
         check-charon-pin = pkgs.runCommand "aeneas-check-charon-pin"
           {
             buildInputs = [ pkgs.jq ];
@@ -248,8 +239,20 @@
           ];
         };
         checks = {
-          default = aeneas-checks;
-          inherit aeneas-check-tidiness check-charon-pin;
+          default = pkgs.runCommand "aeneas-checks" { } ''
+            echo ${aeneas-tests}
+            echo ${aeneas-verify-coq}
+            echo ${aeneas-verify-fstar}
+            echo ${aeneas-verify-hol4}
+            touch $out
+          '';
+          inherit
+            aeneas-tests
+            aeneas-verify-coq
+            aeneas-verify-fstar
+            aeneas-verify-hol4
+            aeneas-check-tidiness
+            check-charon-pin;
         };
       });
 }