diff --git a/.github/workflows/install_and_test.yml b/.github/workflows/install_and_test.yml index b1bb630d7..54b70bb98 100644 --- a/.github/workflows/install_and_test.yml +++ b/.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 + diff --git a/README.md b/README.md index 106d700c3..1d42e8de0 100644 --- a/README.md +++ b/README.md @@ -60,14 +60,12 @@ manager (with flakes enabled -+ 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` diff --git a/cli/default.nix b/cli/default.nix index 0805ea169..f1499d08e 100644 --- a/cli/default.nix +++ b/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="." diff --git a/engine/default.nix b/engine/default.nix index a8b9c3be8..ef0288b83 100644 --- a/engine/default.nix +++ b/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";