Remove jasmin

cryspen · Mar 18, 2024 · 62e71e6 · 62e71e6
1 parent 25563f0
commit 62e71e6
Show file tree

Hide file tree

Showing 19 changed files with 46 additions and 21 deletions.
diff --git a/.github/coq-errors.json b/.github/coq-errors.json
@@ -0,0 +1,20 @@
+{
+    "problemMatcher": [
+        {
+            "owner": "coq",
+            "pattern": [
+                {
+                    "regexp": "^File \"([^\"].*)\", line (\\d+), characters (\\d+)-(\\d+):$",
+                    "file": 1,
+                    "line": 2,
+                    "column": 3
+                },
+                {
+                    "regexp": "^(Error|Warning): (.*)$",
+                    "severity": 1,
+                    "message": 2
+                }
+            ]
+        }
+    ]
+}
diff --git a/.github/workflows/coq-hacspec-ssprove-lib.yml b/.github/workflows/coq-hacspec-ssprove-lib.yml
@@ -1,6 +1,4 @@
-# This file was generated from `meta.yml`, please do not edit manually.
-# Follow the instructions on https://github.com/coq-community/templates to regenerate.
-name: Docker CI
+name: Hacspec - Coq, SSProve Lib
 
 on:
   schedule:
@@ -23,11 +21,19 @@ jobs:
       fail-fast: false
     steps:
       - uses: actions/checkout@v3
+      - name: Set up environment
+        run: |
+          echo "::group::Setting up problem matcher"
+          echo "::add-matcher::./.github/coq-errors.json"
+          echo "::endgroup::"
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'opam/coq-hacspec-ssprove.opam'
           custom_image: ${{ matrix.image }}
-
+      - after_script: |
+          startGroup "Run ssprove coq library tests"
+            make test
+          endGroup "Run ssprove coq library tests"
 
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme

diff --git a/engine/dune-project b/engine/dune-project
@@ -47,7 +47,7 @@
         zarith_stubs_js
 
         ; F*-specific dependencies
-        batteries
+        (batteries (<= "3.7.2"))
         zarith
         stdint
         ppxlib

diff --git a/engine/hax-engine.opam b/engine/hax-engine.opam
@@ -34,7 +34,7 @@ depends: [
   "js_of_ocaml"
   "js_of_ocaml-ppx"
   "zarith_stubs_js"
-  "batteries"
+  "batteries" {<= "3.7.2"}
   "zarith"
   "stdint"
   "ppxlib"

diff --git a/proof-libs/coq/ssprove/src/ConCertLib.v b/proof-libs/coq/ssprove/src/ConCertLib.v
@@ -9,7 +9,7 @@ Import PackageNotation.
 From extructures Require Import ord fset fmap.
 
 From mathcomp Require Import ssrZ word.
-From Jasmin Require Import word.
+From Crypt Require Import jasmin_word.
 
 From Coq Require Import ZArith List.
 Import List.ListNotations.

diff --git a/proof-libs/coq/ssprove/src/Hacspec_Lib.v b/proof-libs/coq/ssprove/src/Hacspec_Lib.v
@@ -15,7 +15,7 @@ Import PackageNotation.
 From extructures Require Import ord fset fmap.
 
 From mathcomp Require Import ssrZ word.
-From Jasmin Require Import word.
+From Crypt Require Import jasmin_word.
 
 From Coq Require Import ZArith List.
 Import List.ListNotations.

diff --git a/proof-libs/coq/ssprove/src/Hacspec_Lib_Coercions.v b/proof-libs/coq/ssprove/src/Hacspec_Lib_Coercions.v
@@ -15,7 +15,7 @@ Import PackageNotation.
 From extructures Require Import ord fset fmap.
 
 From mathcomp Require Import ssrZ word.
-From Jasmin Require Import word.
+From Crypt Require Import jasmin_word.
 
 From Coq Require Import ZArith List.
 Import List.ListNotations.

diff --git a/proof-libs/coq/ssprove/src/Hacspec_Lib_Controlflow.v b/proof-libs/coq/ssprove/src/Hacspec_Lib_Controlflow.v
@@ -15,7 +15,7 @@ Import PackageNotation.
 From extructures Require Import ord fset fmap.
 
 From mathcomp Require Import ssrZ word.
-From Jasmin Require Import word.
+From Crypt Require Import jasmin_word.
 
 From Coq Require Import ZArith List.
 Import List.ListNotations.

diff --git a/proof-libs/coq/ssprove/src/Hacspec_Lib_Eq.v b/proof-libs/coq/ssprove/src/Hacspec_Lib_Eq.v
@@ -15,7 +15,7 @@ Import PackageNotation.
 From extructures Require Import ord fset fmap.
 
 From mathcomp Require Import ssrZ word.
-From Jasmin Require Import word.
+From Crypt Require Import jasmin_word.
 
 From Coq Require Import ZArith List.
 Import List.ListNotations.

diff --git a/proof-libs/coq/ssprove/src/Hacspec_Lib_Integers.v b/proof-libs/coq/ssprove/src/Hacspec_Lib_Integers.v
@@ -15,7 +15,7 @@ Import PackageNotation.
 From extructures Require Import ord fset fmap.
 
 From mathcomp Require Import ssrZ word.
-From Jasmin Require Import word.
+From Crypt Require Import jasmin_word.
 
 From Coq Require Import ZArith List.
 Import List.ListNotations.

diff --git a/proof-libs/coq/ssprove/src/Hacspec_Lib_Loops.v b/proof-libs/coq/ssprove/src/Hacspec_Lib_Loops.v
@@ -15,7 +15,7 @@ Import PackageNotation.
 From extructures Require Import ord fset fmap.
 
 From mathcomp Require Import ssrZ word.
-From Jasmin Require Import word.
+From Crypt Require Import jasmin_word.
 
 From Coq Require Import ZArith List.
 Import List.ListNotations.

diff --git a/proof-libs/coq/ssprove/src/Hacspec_Lib_Ltac.v b/proof-libs/coq/ssprove/src/Hacspec_Lib_Ltac.v
@@ -15,7 +15,7 @@ Import PackageNotation.
 From extructures Require Import ord fset fmap.
 
 From mathcomp Require Import ssrZ word.
-From Jasmin Require Import word.
+From Crypt Require Import jasmin_word.
 
 From Coq Require Import ZArith List.
 Import List.ListNotations.

diff --git a/proof-libs/coq/ssprove/src/Hacspec_Lib_Monad.v b/proof-libs/coq/ssprove/src/Hacspec_Lib_Monad.v
@@ -15,7 +15,7 @@ Import PackageNotation.
 From extructures Require Import ord fset fmap.
 
 From mathcomp Require Import ssrZ word.
-From Jasmin Require Import word.
+From Crypt Require Import jasmin_word.
 
 From Coq Require Import ZArith List.
 Import List.ListNotations.

diff --git a/proof-libs/coq/ssprove/src/Hacspec_Lib_Natmod.v b/proof-libs/coq/ssprove/src/Hacspec_Lib_Natmod.v
@@ -15,7 +15,7 @@ Import PackageNotation.
 From extructures Require Import ord fset fmap.
 
 From mathcomp Require Import ssrZ word.
-From Jasmin Require Import word.
+From Crypt Require Import jasmin_word.
 
 From Coq Require Import ZArith List.
 Import List.ListNotations.

diff --git a/proof-libs/coq/ssprove/src/Hacspec_Lib_Notation.v b/proof-libs/coq/ssprove/src/Hacspec_Lib_Notation.v
@@ -15,7 +15,7 @@ Import PackageNotation.
 From extructures Require Import ord fset fmap.
 
 From mathcomp Require Import ssrZ word.
-From Jasmin Require Import word.
+From Crypt Require Import jasmin_word.
 
 From Coq Require Import ZArith List.
 Import List.ListNotations.

diff --git a/proof-libs/coq/ssprove/src/Hacspec_Lib_Pre.v b/proof-libs/coq/ssprove/src/Hacspec_Lib_Pre.v
@@ -17,7 +17,7 @@ From extructures Require Import ord fset fmap.
 Require Import ChoiceEquality.
 
 From mathcomp Require Import ssrZ word.
-From Jasmin Require Import word.
+From Crypt Require Import jasmin_word.
 
 From Coq Require Import ZArith List.
 Import ListNotations.

diff --git a/proof-libs/coq/ssprove/src/Hacspec_Lib_Seq.v b/proof-libs/coq/ssprove/src/Hacspec_Lib_Seq.v
@@ -15,7 +15,7 @@ Import PackageNotation.
 From extructures Require Import ord fset fmap.
 
 From mathcomp Require Import ssrZ word.
-From Jasmin Require Import word.
+From Crypt Require Import jasmin_word.
 
 From Coq Require Import ZArith List.
 Import List.ListNotations.

diff --git a/proof-libs/coq/ssprove/src/Hacspec_Lib_TODO.v b/proof-libs/coq/ssprove/src/Hacspec_Lib_TODO.v
@@ -15,7 +15,7 @@ Import PackageNotation.
 From extructures Require Import ord fset fmap.
 
 From mathcomp Require Import ssrZ word.
-From Jasmin Require Import word.
+From Crypt Require Import jasmin_word.
 
 From Coq Require Import ZArith List.
 Import List.ListNotations.

diff --git a/proof-libs/coq/ssprove/src/LocationUtility.v b/proof-libs/coq/ssprove/src/LocationUtility.v
@@ -6,7 +6,6 @@ Import PackageNotation.
 From Crypt Require Import pkg_interpreter.
 From extructures Require Import ord fset fmap.
 Require Import Hacspec_Lib_Comparable.
-From Jasmin Require Import xseq.
 Require Import Coq.Logic.FunctionalExtensionality.
 Import List.ListNotations.