[build] Add support for code coverage

Closes coq#10267

.gitlab-ci.yml

@@ -235,7 +235,7 @@ before_script:
   script:
     - set -e
     - echo 'start:coq.test'
-    - make -f Makefile.ci -j "$NJOBS" "${CI_JOB_NAME#*:}"
+    # - make -f Makefile.ci -j "$NJOBS" "${CI_JOB_NAME#*:}"
     - echo 'end:coq.test'
     - set +e
   needs:
@@ -593,6 +593,28 @@ test-suite:edge+4.11+trunk+dune:
     expire_in: 2 week
   allow_failure: true
 
+test-suite:edge+coverage:
+  stage: stage-1
+  dependencies: []
+  script:
+    - opam update
+    - opam pin add dune --dev
+    - opam install bisect_ppx
+    - dune build --workspace dev/dune-workspace.bisect @runtest
+    - bisect-ppx-report -I _build/coverage -html _build/coq-coverage `find . -name 'bisect*.out'
+    # TODO: deploy
+    # bisect-ppx-report send-to Codecov
+  variables:
+    OPAM_SWITCH: edge
+  artifacts:
+    name: "$CI_JOB_NAME.logs"
+    when: always
+    paths:
+      - _build/log
+      - _build/coq-coverage
+    expire_in: 2 week
+  allow_failure: true
+
 test-suite:base+async:
   extends: .test-suite-template
   dependencies:

dev/dune-workspace.bisect

@@ -0,0 +1,6 @@
+(lang dune 2.6)
+
+(context
+ (default
+  (name coverage)
+  (bisect_enabled true)))

dune-project

@@ -1,6 +1,7 @@
-(lang dune 2.5)
+(lang dune 2.6)
 (name coq)
 (using coq 0.2)
+(using bisect_ppx 1.0)
 
 (formatting
  (enabled_for ocaml))

engine/dune

@@ -3,4 +3,5 @@
  (synopsis "Coq's Tactic Engine")
  (public_name coq.engine)
  (wrapped false)
+ (bisect_ppx)
  (libraries library))

interp/dune

@@ -3,4 +3,5 @@
  (synopsis "Coq's Syntactic Interpretation for AST [notations, implicits]")
  (public_name coq.interp)
  (wrapped false)
+ (bisect_ppx)
  (libraries pretyping))

kernel/dune

@@ -4,6 +4,7 @@
  (public_name coq.kernel)
  (wrapped false)
  (modules (:standard \ genOpcodeFiles uint63_31 uint63_63))
+ (bisect_ppx)
  (libraries lib byterun dynlink))
 
 (executable

library/dune

@@ -3,6 +3,7 @@
  (synopsis "Coq's Loadable Libraries (vo) Support")
  (public_name coq.library)
  (wrapped false)
+ (bisect_ppx)
  (libraries kernel))
 
 (documentation

plugins/ltac/dune

@@ -3,13 +3,15 @@
  (public_name coq.plugins.ltac)
  (synopsis "Coq's LTAC tactic language")
  (modules :standard \ tauto)
+ (bisect_ppx)
  (libraries coq.stm))
 
 (library
  (name tauto_plugin)
  (public_name coq.plugins.tauto)
  (synopsis "Coq's tauto tactic")
  (modules tauto)
+ (bisect_ppx)
  (libraries coq.plugins.ltac))
 
 (coq.pp (modules extratactics g_tactic  g_rewrite g_eqdecide g_auto g_obligations g_ltac profile_ltac_tactics coretactics g_class extraargs))

plugins/ssr/dune

@@ -3,6 +3,7 @@
  (public_name coq.plugins.ssreflect)
  (synopsis "Coq's ssreflect plugin")
  (modules_without_implementation ssrast)
+ (bisect_ppx)
  (flags :standard -open Gramlib)
  (libraries coq.plugins.ssrmatching))
 

pretyping/dune

@@ -3,4 +3,5 @@
  (synopsis "Coq's Type Inference Component (Pretyper)")
  (public_name coq.pretyping)
  (wrapped false)
+ (bisect_ppx)
  (libraries engine))

proofs/dune

@@ -3,4 +3,5 @@
  (synopsis "Coq's Higher-level Refinement Proof Engine and Top-level Proof Structure")
  (public_name coq.proofs)
  (wrapped false)
+ (bisect_ppx)
  (libraries pretyping))

stm/dune

@@ -3,4 +3,5 @@
  (synopsis "Coq's Document Manager and Proof Checking Scheduler")
  (public_name coq.stm)
  (wrapped false)
+ (bisect_ppx)
  (libraries vernac))

tactics/dune

@@ -3,4 +3,5 @@
  (synopsis "Coq's Core Tactics [ML implementation]")
  (public_name coq.tactics)
  (wrapped false)
+ (bisect_ppx)
  (libraries printing))

topbin/dune

@@ -8,6 +8,7 @@
  (public_name coqtop.opt)
  (package coq)
  (modules coqtop_bin)
+ (bisect_ppx)
  (libraries coq.toplevel)
  (link_flags -linkall))
 
@@ -25,6 +26,7 @@
  (public_name coqc)
  (package coq)
  (modules coqc_bin)
+ (bisect_ppx)
  (libraries coq.toplevel)
  (modes native byte)
  ; Adding -ccopt -flto to links options could be interesting, however,

toplevel/dune

@@ -3,6 +3,7 @@
  (public_name coq.toplevel)
  (synopsis "Coq's Interactive Shell [terminal-based]")
  (wrapped false)
+ (bisect_ppx)
  (libraries num coq.stm))
 ; Coqlevel provides the `Num` library to plugins, we could also use
 ; -linkall in the plugins file, to be discussed.

vernac/dune

@@ -3,6 +3,7 @@
  (synopsis "Coq's Vernacular Language")
  (public_name coq.vernac)
  (wrapped false)
+ (bisect_ppx)
  (libraries tactics parsing))
 
 (coq.pp (modules g_proofs g_vernac))