WIP

.github/workflows/extract_and_run_coq.yml

@@ -6,12 +6,38 @@ jobs:
     runs-on: ubuntu-latest
     container:
       image: coqorg/coq:8.18.0-ocaml-4.13.1-flambda
+    permissions:
+      contents: write
     steps:
-    - uses: actions/checkout@v3
-    - name: Build
+    - name: Checkout code
+      uses: actions/checkout@v3
+    - uses: actions/setup-node@v4
+      with:
+        node-version: 18
+    - uses: dtolnay/[email protected]
+    - run: cargo install --path cli/driver && cargo install --path cli/subcommands
+    - name: opam setup
       run: |
         export HOME=/home/coq
         export PATH=$HOME/.cargo/bin:$PATH
         env
         opam switch 4.13.1+flambda
         eval $(opam env)
+    - run: opam install . --deps-only
+      working-directory: engine
+    - run: |
+        opam exec -- dune build
+        opam exec -- dune install
+      working-directory: engine
+    - name: Build
+      working-directory: examples/coverage
+      run: |
+        sudo apt-get install jq -y
+        ./setup.sh
+        curl -sL https://deb.nodesource.com/setup_16.x -o /tmp/nodesource_setup.sh
+        sudo bash /tmp/nodesource_setup.sh
+        cargo hax into coq
+        cd proofs/coq/extraction
+        sed 's/_impl_f_/_f_/' < Coverage_Test_instance.v > Coverage_Test_instance.v
+        coq_makefile -f _CoqProject -o Makefile
+        make

engine/utils/ppx_generate_features/ppx_generate_features.ml

@@ -195,8 +195,7 @@ let expand ~(ctxt : Expansion_context.Extension.t) (features : string list) :
         end
 
         module type MAPPER = sig
-          val map :
-            'a 'b. (Span.t -> 'a -> 'b) -> Enumeration.t -> Span.t -> 'a -> 'b
+          val map : 'a 'b. (Span.t -> 'a -> 'b) -> Enumeration.t -> Span.t -> 'a -> 'b
         end
 
         module Map (S : T) (Mapper : MAPPER) =