diff --git a/.github/workflows/extract_and_run_coq.yml b/.github/workflows/extract_and_run_coq.yml index 46a8f4976..0cd929bef 100644 --- a/.github/workflows/extract_and_run_coq.yml +++ b/.github/workflows/extract_and_run_coq.yml @@ -14,40 +14,40 @@ jobs: - name: ⤵ Install hax run: | - nix profile install --verbose ./hax + nix build .\#coq-coverage-example - - name: build coverage example - working-directory: hax/examples/coverage - run: | - nix run . into coq + # - name: build coverage example + # working-directory: hax/examples/coverage + # run: | + # nix run . into coq - - name: install annotated core for coq - working-directory: hax/proof-libs/coq/coq/generated-core - run: | - nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile" && \ - nix-shell --packages coq coqPackages.coq-record-update --run "make" && \ - nix-shell --packages coq coqPackages.coq-record-update --run "sudo make install" + # - name: install annotated core for coq + # working-directory: hax/proof-libs/coq/coq/generated-core + # run: | + # nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile" && \ + # nix-shell --packages coq coqPackages.coq-record-update --run "make" && \ + # nix-shell --packages coq coqPackages.coq-record-update --run "sudo make install" - - name: run coq - coverage - working-directory: hax/examples/coverage/proofs/coq/extraction - run: | - sed 's/_impl_f_/_f_/' < Coverage_Test_instance.v > Coverage_Test_instance.v # TODO: this is a hotfix, should be solved in backend and removed from here. - nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile" - nix-shell --packages coq coqPackages.coq-record-update --run "make" + # - name: run coq - coverage + # working-directory: hax/examples/coverage/proofs/coq/extraction + # run: | + # sed 's/_impl_f_/_f_/' < Coverage_Test_instance.v > Coverage_Test_instance.v # TODO: this is a hotfix, should be solved in backend and removed from here. + # nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile" + # nix-shell --packages coq coqPackages.coq-record-update --run "make" - - name: build and run coq on tests - env: - FILES: assert attribute-opaque enum-struct-variant - NOT_SUPPORTED_FILES: attributes cli conditional-match constructor-as-closure cyclic-modules enum-repr even dyn functions - run: | - for f in $FILES; do \ - cd hax/tests/$f && \ - nix run . into coq && \ - cd ../../.. - done - for f in $FILES; do \ - cd hax/tests/$f/proofs/coq/extraction && \ - nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile" && \ - nix-shell --packages coq coqPackages.coq-record-update --run "make" && \ - cd ../../../../../../ - done + # - name: build and run coq on tests + # env: + # FILES: assert attribute-opaque enum-struct-variant + # NOT_SUPPORTED_FILES: attributes cli conditional-match constructor-as-closure cyclic-modules enum-repr even dyn functions + # run: | + # for f in $FILES; do \ + # cd hax/tests/$f && \ + # nix run . into coq && \ + # cd ../../.. + # done + # for f in $FILES; do \ + # cd hax/tests/$f/proofs/coq/extraction && \ + # nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile" && \ + # nix-shell --packages coq coqPackages.coq-record-update --run "make" && \ + # cd ../../../../../../ + # done diff --git a/examples/commonArgs.nix b/examples/commonArgs.nix new file mode 100644 index 000000000..6238f52ea --- /dev/null +++ b/examples/commonArgs.nix @@ -0,0 +1,26 @@ +{ + craneLib, + lib, +}: +let + matches = re: path: !builtins.isNull (builtins.match re path); +in +{ + version = "0.0.1"; + src = lib.cleanSourceWith { + src = craneLib.path ./..; + filter = path: type: + # We include only certain files. FStar files under the example + # directory are listed out. Same for proverif (*.pvl) files. + ( matches ".*(Makefile|.*[.](rs|toml|lock|diff|fsti?|pv))$" path + && !matches ".*examples/.*[.]fsti?$" path + ) || ("directory" == type); + }; + doCheck = false; + cargoVendorDir = craneLib.vendorMultipleCargoDeps { + cargoLockList = [ + ./Cargo.lock + ../Cargo.lock + ]; + }; +} diff --git a/examples/coverage/default.nix b/examples/coverage/default.nix new file mode 100644 index 000000000..abc457c6a --- /dev/null +++ b/examples/coverage/default.nix @@ -0,0 +1,38 @@ +{ + stdenv, + lib, + hax, + coqPackages, + gnused, + craneLib, + bat, + coqGeneratedCore ? import ../../proof-libs/coq/coq {inherit stdenv coqPackages;}, +}: +let + commonArgs = import ../commonArgs.nix {inherit craneLib lib;}; + cargoArtifacts = craneLib.buildDepsOnly commonArgs; +in + craneLib.mkCargoDerivation (commonArgs + // { + inherit cargoArtifacts; + pname = "coverage"; + doCheck = false; + buildPhaseCargoCommand = '' + cd examples/coverage + cargo hax into coq + + cd proofs/coq/extraction + echo -e "-R ${coqGeneratedCore}/lib/coq/user-contrib/Core Core\n$(cat _CoqProject)" > _CoqProject + coq_makefile -f _CoqProject -o Makefile + make + ''; + buildInputs = [ + hax + coqPackages.coq-record-update + coqPackages.coq + gnused + ]; + }) + + + # COQLIB diff --git a/examples/default.nix b/examples/default.nix index bd602e515..29f68c404 100644 --- a/examples/default.nix +++ b/examples/default.nix @@ -9,26 +9,7 @@ jq, proverif, }: let - matches = re: path: !builtins.isNull (builtins.match re path); - commonArgs = { - version = "0.0.1"; - src = lib.cleanSourceWith { - src = craneLib.path ./..; - filter = path: type: - # We include only certain files. FStar files under the example - # directory are listed out. Same for proverif (*.pvl) files. - ( matches ".*(Makefile|.*[.](rs|toml|lock|diff|fsti?|pv))$" path - && !matches ".*examples/.*[.]fsti?$" path - ) || ("directory" == type); - }; - doCheck = false; - cargoVendorDir = craneLib.vendorMultipleCargoDeps { - cargoLockList = [ - ./Cargo.lock - ../Cargo.lock - ]; - }; - }; + commonArgs = import ./commonArgs.nix {inherit craneLib lib;}; cargoArtifacts = craneLib.buildDepsOnly commonArgs; in craneLib.mkCargoDerivation (commonArgs diff --git a/flake.nix b/flake.nix index 168556d28..cf7f1e499 100644 --- a/flake.nix +++ b/flake.nix @@ -91,6 +91,12 @@ check-examples = checks.examples; check-readme-coherency = checks.readme-coherency; + coq-coverage-example = pkgs.callPackage ./examples/coverage { + inherit (packages) hax; + inherit (pkgs) coqPackages; + inherit craneLib; + }; + rust-by-example-hax-extraction = pkgs.stdenv.mkDerivation { name = "rust-by-example-hax-extraction"; phases = ["installPhase"]; diff --git a/proof-libs/coq/coq/default.nix b/proof-libs/coq/coq/default.nix new file mode 100644 index 000000000..d0ccfd8f0 --- /dev/null +++ b/proof-libs/coq/coq/default.nix @@ -0,0 +1,22 @@ +{ + stdenv ? (import {}).stdenv, + coqPackages ? (import {}).coqPackages, +}: +stdenv.mkDerivation { + name = "hax-coq-generated-core"; + src = ./generated-core; + buildPhase = '' + coq_makefile -f _CoqProject -o Makefile + make + ''; + installPhase = '' + export DESTDIR=$out + make install + mv $out/nix/store/*/lib $out + rm -rf $out/nix + ''; + buildInputs = [ + coqPackages.coq-record-update + coqPackages.coq + ]; +}