Coq proof lib

.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
+                }
+            ]
+        }
+    ]
+}

.github/workflows/coq-hacspec-lib.yml

@@ -0,0 +1,100 @@
+
+name: Hacspec - Coq Lib
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build:
+    # the OS must be GNU/Linux to be able to use the docker-coq-action
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        image:
+          - 'coqorg/coq:8.18'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v3
+      - uses: DeterminateSystems/nix-installer-action@main
+      - uses: DeterminateSystems/magic-nix-cache-action@main
+      - name: Build
+        run: nix build -L
+
+      - name: Install the toolchain
+        run: |
+          nix profile install nixpkgs#yq
+          nix profile install .#rustc
+          nix profile install .
+      - name: Install tomlq
+        run: cargo install --git https://github.com/Techcable/tomlq
+
+      - name: Set up environment
+        run: |
+          echo "::group::Setting up problem matcher"
+          echo "::add-matcher::./.github/coq-errors.json"
+          echo "::endgroup::"
+      - name: Build Coq-Hacspec lib
+        uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'opam/coq-hacspec.opam'
+          custom_image: ${{ matrix.image }}
+
+      - name: Run Coq on Tests
+        working-directory: tests
+        run: |
+          paths=$(tomlq -r '.workspace.members | .[]' Cargo.toml)
+          for cratePath in $paths; do
+            crate=$(tomlq -r '.package.name' "$cratePath/Cargo.toml")
+            for skip in $SKIPLIST; do
+              if [[ "$skip" == "$crate" || "$skip" == "$crate-$backend" ]]; then
+                echo "⛔ $crate [$backend] (skipping)"
+                continue 2
+              fi
+            done
+            for backend in coq; do
+              echo "::group::$crate [$backend]"
+              cargo hax -C -p "$crate" \; into "$backend"
+              coqc $cratePath/proofs/coq/extraction/*.v
+              echo "::endgroup::"
+            done
+          done
+        env:
+          SKIPLIST: |
+            enum-struct-variant
+            literals
+            slices
+            naming
+            if-let
+            enum-repr
+            pattern-or
+            side-effects
+            v1-lib
+            mut_arg
+            fnmut
+            mut-ref-functionalization
+            generics
+            loops
+            even
+            odd
+            never-type
+            attributes
+            attribute-opaque
+            raw-attributes
+            traits
+            reordering
+            nested-derefs
+            minimal
+            basic-structs
+            ping-pong
+            noise-kkpsk0
+            fn-to-letfun
+            include-flag
+            recursion
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo

dune-project

@@ -0,0 +1,24 @@
+(lang dune 3.8)
+(using coq 0.8)
+(generate_opam_files true)
+(name coq-hacspec)
+(opam_file_location inside_opam_directory)
+
+(package
+ (name coq-hacspec)
+ (synopsis "A short synopsis")
+ (description "A longer description")
+ (maintainers "Lasse Letager Hansen<[email protected]>")
+ (authors "Lasse Letager Hansen<[email protected]>")
+ (depends
+        ocaml
+        dune
+        (base (>= "0.16.2"))
+	(coq (>= "8.18.0"))
+        coq-compcert
+        coq-coqprime
+        coq-quickchick
+        )
+ (tags
+  (topics "to describe" your project)))
+