Merge pull request #489 from hacspec/optimize-nix-plus-cachix

feat(nix): make derivations lighter, use `cachix`

.github/workflows/install_and_test.yml

@@ -40,8 +40,10 @@ jobs:
       uses: actions/checkout@v3
       with:
         repository: 'hacspec/specs'
+        path: specs
 
     - name: Extract specifications
+      working-directory: specs
       run: |
         paths=$(tomlq -r '.workspace.members | .[]' Cargo.toml)
         for cratePath in $paths; do
@@ -66,3 +68,14 @@ jobs:
           hacspec-halo2-fstar
           hacspec-weierstrass-coq
           hacspec-weierstrass-fstar
+
+    - name: Push to Cachix
+      if: ${{ github.event_name == 'workflow_dispatch'  || github.event_name == 'merge_group'  }}
+      env:
+        CACHIX_AUTH_TOKEN: ${{ secrets.CACHIX_AUTH_TOKEN }}
+      run: |
+        nix profile install nixpkgs#cachix nixpkgs#jq
+        nix build --json \
+          | jq -r '.[].outputs | to_entries[].value' \
+          | cachix push hax
+

README.md

@@ -60,14 +60,12 @@ manager</a> <i>(with <a href="https://nixos.wiki/wiki/Flakes">flakes</a> enabled
 
 </details>
 
-+ Run hax on a crate to get F\*/Coq/...:
-   - `cd path/to/your/crate`
-   - `nix run github:hacspec/hax -- into fstar`
-      will create `fst` modules in the directory `hax/extraction/fstar`.
-      *Note: replace `fstar` by your backend of choice*
-
-+ Install the tool:  `nix profile install github:hacspec/hax`
-   - then run `cargo hax --help` anywhere
++ **Run hax on a crate directly** to get F\*/Coq/... (assuming you are in the crate's folder):
+   - `nix run github:hacspec/hax -- into fstar` extracts F*.
+
++ **Install hax**:  `nix profile install github:hacspec/hax`, then run `cargo hax --help` anywhere
++ **Note**: in any of the Nix commands above, replace `github:hacspec/hax` by `./dir` to compile a local checkout of hax that lives in `./some-dir`
++ **Setup binary cache**: [using Cachix](https://app.cachix.org/cache/hax), just `cachix use hax`
 
 </details>
 

cli/default.nix

@@ -40,7 +40,16 @@
     // {
       pname = pname;
     });
-  hax = craneLib.buildPackage (
+  hax = stdenv.mkDerivation {
+    name = hax_with_artifacts.name;
+    unpackPhase = "true";
+    buildPhase = "true";
+    installPhase = ''
+      mkdir -p $out
+      cp -r ${hax_with_artifacts}/bin $out/bin
+    '';
+  };
+  hax_with_artifacts = craneLib.buildPackage (
     commonArgs
     // {
       inherit cargoArtifacts pname;
@@ -73,7 +82,7 @@
       mv $INDEX index.html
     '';
   };
-  binaries = [hax hax-engine rustc gcc];
+  binaries = [hax hax-engine.bin rustc gcc];
   tests = craneLib.buildPackage (commonArgs
     // {
       inherit cargoArtifacts;
@@ -112,8 +121,8 @@ in
           pname = "hax_engine_names_extract";
           cargoLock = ../Cargo.lock;
           cargoToml = ../engine/names/extract/Cargo.toml;
-          cargoArtifacts = hax;
-          nativeBuildInputs = [hax];
+          cargoArtifacts = hax_with_artifacts;
+          nativeBuildInputs = [hax_with_artifacts];
           postUnpack = ''
             cd $sourceRoot/engine/names/extract
             sourceRoot="."

engine/default.nix

@@ -9,6 +9,7 @@
   closurecompiler,
   gnused,
   lib,
+  removeReferencesTo,
 }: let
   non_empty_list = ocamlPackages.buildDunePackage rec {
     pname = "non_empty_list";
@@ -86,8 +87,15 @@
       nodejs
       ocamlPackages.js_of_ocaml-compiler
       jq
+      removeReferencesTo
     ];
     strictDeps = true;
+    installPhase = ''
+      dune install --prefix=$bin --libdir=$lib/lib/ocaml/${ocamlPackages.ocaml.version}/site-lib/
+      find "$bin" -type f -exec remove-references-to -t ${ocamlPackages.ocaml} '{}' +
+    '';
+
+    outputs = ["out" "bin" "lib"];
     passthru = {
       docs = hax-engine.overrideAttrs (old: {
         name = "hax-engine-docs";