CI: split Coq job

The coq-program job produces the extracted OCaml code in the CIL/
directory.

The coq-proof job checks all Coq proofs.

Also remove the redundant “dependencies” entries

.gitlab-ci.yml

@@ -45,27 +45,37 @@ cache dependencies:
     | xargs nix-store --query --requisites
     | cachix push jasmin'
 
-coq:
+coq-program:
   stage: prove
   variables:
     EXTRA_NIX_ARGUMENTS: --arg coqDeps true
   extends: .common
   script:
-  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -j$NIX_BUILD_CORES -C proofs'
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -j$NIX_BUILD_CORES -C proofs Makefile.coq'
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -j$NIX_BUILD_CORES -C proofs -f Makefile.coq compiler/jasmin_compiler.vo'
   - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -j$NIX_BUILD_CORES -C compiler CIL'
   artifacts:
     paths:
+    - proofs/
     - compiler/CIL/
 
+coq-proof:
+  stage: prove
+  variables:
+    EXTRA_NIX_ARGUMENTS: --arg coqDeps true
+  extends: .common
+  needs:
+  - coq-program
+  script:
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -j$NIX_BUILD_CORES -C proofs'
+
 ocaml:
   stage: build
   variables:
     EXTRA_NIX_ARGUMENTS: --arg ocamlDeps true
   extends: .common
   needs:
-  - coq
-  dependencies:
-  - coq
+  - coq-program
   script:
   - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -j$NIX_BUILD_CORES -C compiler'
   artifacts:
@@ -121,9 +131,7 @@ opam-compiler:
     EXTRA_NIX_ARGUMENTS: --arg opamDeps true
   extends: .common
   needs:
-  - coq
-  dependencies:
-  - coq
+  - coq-program
   cache:
     key:
       files:
@@ -149,9 +157,7 @@ tarball:
     TARBALL: jasmin-compiler-$CI_COMMIT_SHORT_SHA
   extends: .common
   needs:
-  - coq
-  dependencies:
-  - coq
+  - coq-program
   script:
   - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -C compiler dist DISTDIR=$TARBALL'
   artifacts:
@@ -164,8 +170,6 @@ build-from-tarball:
     TARBALL: jasmin-compiler-$CI_COMMIT_SHORT_SHA
   needs:
   - tarball
-  dependencies:
-  - tarball
   script:
   - tar xvf compiler/$TARBALL.tgz
   - nix-build -o out $TARBALL
@@ -177,10 +181,7 @@ check:
     EXTRA_NIX_ARGUMENTS: --arg testDeps true
   extends: .common
   needs:
-  - coq
-  - ocaml
-  dependencies:
-  - coq
+  - coq-program
   - ocaml
   script:
   - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run './compiler/jasminc.native -version'
@@ -192,10 +193,7 @@ libjade-compile-to-asm:
     EXTRA_NIX_ARGUMENTS: --arg testDeps true
   extends: .common
   needs:
-  - coq
-  - ocaml
-  dependencies:
-  - coq
+  - coq-program
   - ocaml
   script:
   - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run './scripts/test-libjade.sh src'
@@ -213,10 +211,7 @@ libjade-extract-to-ec:
     ECJOBS: '$(NIX_BUILD_CORES)'
   extends: .common
   needs:
-  - coq
-  - ocaml
-  dependencies:
-  - coq
+  - coq-program
   - ocaml
   script:
   - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'easycrypt why3config -why3 $WHY3_CONF'
@@ -238,10 +233,7 @@ test-extract-to-ec:
     JSJOBS: $(NIX_BUILD_CORES)
   extends: .common
   needs:
-  - coq
-  - ocaml
-  dependencies:
-  - coq
+  - coq-program
   - ocaml
   script:
   - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'easycrypt why3config -why3 $WHY3_CONF'
@@ -262,8 +254,6 @@ push-compiler-code:
     TARBALL: jasmin-compiler-$CI_COMMIT_SHORT_SHA
   needs:
   - tarball
-  dependencies:
-  - tarball
   before_script:
   - nix-env -iA nixpkgs.git
   - nix-env -iA nixpkgs.openssh

proofs/_CoqProject

@@ -56,6 +56,7 @@ compiler/dead_code.v
 compiler/dead_code_proof.v
 compiler/inline.v
 compiler/inline_proof.v
+compiler/jasmin_compiler.v
 compiler/lea.v
 compiler/lea_proof.v
 compiler/linearization.v

proofs/compiler/jasmin_compiler.v

@@ -0,0 +1,6 @@
+(** This module is meant as the minimal dependency of extracted code. *)
+Require compiler.
+Require sem.
+Require arm_params.
+Require x86_params.
+Require sem_params_of_arch_extra.

proofs/lang/extraction.v

@@ -1,12 +1,9 @@
-Require Import var compiler.
-Require sem.
-Require arm_params.
-Require x86_params.
-Require sem_params_of_arch_extra.
-Require waes.
-
-Require ExtrOcamlBasic.
-Require ExtrOcamlString.
+Require jasmin_compiler.
+(* Do not “Require” other modules from Jasmin here:
+   expand the jasmin_compiler module instead. *)
+
+From Coq Require ExtrOcamlBasic.
+From Coq Require ExtrOcamlString.
 
 (* This is a hack to force the extraction to keep the singleton here,
    This need should be removed if we add more constructor to syscall_t *)