CI build fixes

SSProve · Feb 22, 2025 · d2b8787 · d2b8787
1 parent 3f59a42
commit d2b8787
Show file tree

Hide file tree

Showing 9 changed files with 65 additions and 24 deletions.
diff --git a/.github/workflows/nix-action-8.18.yml b/.github/workflows/nix-action-8.18.yml
@@ -36,12 +36,18 @@ jobs:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community, math-comp
         name: ssprove
+    - id: stepGetDerivation
+      name: Getting derivation for current job (coq)
+      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
+        \"8.18\" --argstr job \"coq\" \\\n   --dry-run 2> err > out || (touch fail;
+        true)\n"
+    - name: Error reporting
+      run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
+    - name: Failure check
+      run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
-      name: Checking presence of CI target coq
-      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr
-        bundle \"8.18\" --argstr job \"coq\" \\\n   --dry-run 2>&1 > /dev/null)\n
-        echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
-        s/.*/built/\") >> $GITHUB_OUTPUT\n"
+      name: Checking presence of CI target for current job
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
@@ -84,12 +90,18 @@ jobs:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community, math-comp
         name: ssprove
+    - id: stepGetDerivation
+      name: Getting derivation for current job (mathcomp-analysis)
+      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
+        \"8.18\" --argstr job \"mathcomp-analysis\" \\\n   --dry-run 2> err > out
+        || (touch fail; true)\n"
+    - name: Error reporting
+      run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
+    - name: Failure check
+      run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
-      name: Checking presence of CI target mathcomp-analysis
-      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr
-        bundle \"8.18\" --argstr job \"mathcomp-analysis\" \\\n   --dry-run 2>&1 >
-        /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\
-        \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
+      name: Checking presence of CI target for current job
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
@@ -153,12 +165,18 @@ jobs:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community, math-comp
         name: ssprove
+    - id: stepGetDerivation
+      name: Getting derivation for current job (ssprove)
+      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
+        \"8.18\" --argstr job \"ssprove\" \\\n   --dry-run 2> err > out || (touch
+        fail; true)\n"
+    - name: Error reporting
+      run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
+    - name: Failure check
+      run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
-      name: Checking presence of CI target ssprove
-      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr
-        bundle \"8.18\" --argstr job \"ssprove\" \\\n   --dry-run 2>&1 > /dev/null)\n
-        echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
-        s/.*/built/\") >> $GITHUB_OUTPUT\n"
+      name: Checking presence of CI target for current job
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr

diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml
@@ -47,7 +47,7 @@ jobs:
       run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
       name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
@@ -101,7 +101,7 @@ jobs:
       run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
       name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
@@ -176,7 +176,7 @@ jobs:
       run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
       name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr

diff --git a/.github/workflows/nix-action-8.20.yml b/.github/workflows/nix-action-8.20.yml
@@ -47,7 +47,7 @@ jobs:
       run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
       name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
@@ -101,7 +101,7 @@ jobs:
       run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
       name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
@@ -176,7 +176,7 @@ jobs:
       run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
       name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr

diff --git a/.github/workflows/opam-build.yml b/.github/workflows/opam-build.yml
@@ -49,6 +49,8 @@ jobs:
       # Runs a set of commands using the runners shell
       - name: Build
         run: |
+          apt install libmpfr-dev libppl-dev
           opam repo add coq-released https://coq.inria.fr/opam/released
           opam install coq.8.18.0 coq-equations.1.3+8.18 coq-mathcomp-ssreflect.2.1.0 coq-mathcomp-analysis.1.0.0 coq-extructures.0.4.0 coq-deriving.0.2.0 coq-mathcomp-word.3.0 coq-mathcomp-zify.1.5.0+2.0+8.16
+          opam pin jasmin.dev git+https://github.com/jasmin-lang/jasmin.git#main
           opam exec -- make -j4
diff --git a/.nix/config.nix b/.nix/config.nix
@@ -53,18 +53,21 @@
     mathcomp.job = false;
     mathcomp.override.version = "2.1.0";
     mathcomp-analysis.override.version = "1.0.0";
+    jasmin.override.version = "2024.07.2";
   };
   bundles."8.19".coqPackages = {
     coq.override.version = "8.19";
     mathcomp.job = false;
     mathcomp.override.version = "2.2.0";
     mathcomp-analysis.override.version = "1.0.0";
+    jasmin.override.version = "2024.07.2";
   };
   bundles."8.20".coqPackages = {
     coq.override.version = "8.20";
     mathcomp.job = false;
     mathcomp.override.version = "2.2.0";
     mathcomp-analysis.override.version = "1.2.0";
+    jasmin.override.version = "2024.07.2";
   };
 
   bundles."8.18".push-branches = ["main"];

diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix
@@ -1 +1 @@
-"78d95509824be9e3339c1c0ee19f9c085f32b23e"
+"23abc2d7903983f4fd414288677d6b421d412cd6"
diff --git a/.nix/coq-overlays/SSProve/default.nix → .nix/coq-overlays/ssprove/default.nix b/.nix/coq-overlays/SSProve/default.nix → .nix/coq-overlays/ssprove/default.nix
@@ -7,6 +7,7 @@
 , mathcomp-zify
 , extructures
 , deriving
+, jasmin
 }:
 
 (mkCoqDerivation {
@@ -42,7 +43,8 @@
                            mathcomp-word
                            mathcomp-zify
                            extructures
-                           deriving];
+                           deriving
+                           jasmin];
 
   meta = with lib; {
     description = "SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq";

diff --git a/flake.nix b/flake.nix
@@ -7,7 +7,9 @@
     let
       ssprovePkg = { lib, mkCoqDerivation, coq
                   , equations, extructures, deriving
-                  , mathcomp-analysis, mathcomp-ssreflect }:
+                  , mathcomp-analysis, mathcomp-ssreflect
+                  , mathcomp-word, mathcomp-zify
+                  , mathcomp-experimental-reals, jasmin }:
         mkCoqDerivation {
           pname = "ssprove";
           owner = "SSProve";
@@ -19,6 +21,10 @@
             mathcomp-ssreflect
             deriving
             extructures
+            mathcomp-word
+            mathcomp-zify
+            mathcomp-experimental-reals
+            jasmin
           ];
           meta = {
             description = "A foundational framework for modular cryptographic proofs in Coq ";

diff --git a/theories/Jasmin/examples/add1.v b/theories/Jasmin/examples/add1.v
@@ -16,7 +16,17 @@ Import ListNotations.
 Local Open Scope string.
 
 
+Section Test.
+Context `{AsmOp : asmOp}.
 
+From Coq Require Import PrimInt63.
+
+Import FunName.
+Definition f : funname.
+Proof.
+    unfold funname.
+    Transparent t.
+    exact 1%uint63.
 
 Definition ssprove_jasmin_prog : uprog.
 Proof.
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		"78d95509824be9e3339c1c0ee19f9c085f32b23e"
		"23abc2d7903983f4fd414288677d6b421d412cd6"