wip

cryspen · Nov 28, 2024 · 0150344 · 0150344
1 parent ac28c48
commit 0150344
Show file tree

Hide file tree

Showing 3 changed files with 91 additions and 33 deletions.
diff --git 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/coverage/default.nix b/examples/coverage/default.nix
@@ -0,0 +1,52 @@
+{
+  stdenv,
+  lib,
+  hax,
+  coqPackages,
+  gnused,
+  craneLib,
+}:
+let
+  commonArgs = {
+    version = "0.1.0";
+    src = craneLib.cleanCargoSource ../..;
+    doCheck = false;
+    cargoLockListrgoVendorDir = craneLib.vendorMultipleCargoDeps {
+      cargoLockList = [
+        ../Cargo.lock
+        ../../Cargo.lock
+      ];
+    };
+  };
+  cargoArtifacts = craneLib.buildDepsOnly commonArgs;
+in
+  craneLib.mkCargoDerivation (commonArgs
+    // {
+      inherit cargoArtifacts;
+      pname = "coverage";
+      doCheck = false;
+      buildPhaseCargoCommand = ''
+        cp -r --no-preserve=mode ${../../proof-libs/coq/coq/generated-core} generated-core
+
+        cd generated-core
+        
+        coq_makefile -f _CoqProject -o Makefile
+        make
+        sudo make install
+
+        cd ../examples/coverage
+
+        cargo hax into coq
+        cd proofs/coq/extraction
+        
+        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.
+        coq_makefile -f _CoqProject -o Makefile
+        make
+      '';
+      buildInputs = [
+            hax
+            coqPackages.coq-record-update
+            coqPackages.coq
+            gnused
+      ];
+    })
diff --git 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"];