[build] Add support for code coverage

Closes coq#10267

.gitlab-ci.yml

@@ -636,6 +636,30 @@ test-suite:edge:dune:dev:
 #   variables:
 #     OCAMLVER: 4.12.0+trunk
 
+test-suite:edge+coverage:
+  stage: stage-1
+  dependencies: []
+  script:
+    - ulimit -s 16384
+    - opam update
+    - opam install bisect_ppx
+    - dune build --workspace dev/dune-workspace.bisect @runtest
+    - find _build/coverage/ -name *.coverage -size 0 -exec rm {} \; # workaround truncation bug
+    - bisect-ppx-report html --source-path=_build/coverage --coverage-path=_build/coverage -o _build/coq-coverage --title="Coq's Test suite"
+    # TODO: deploy
+    # bisect-ppx-report send-to Codecov
+  variables:
+    OPAM_SWITCH: edge
+    OPAM_VARIANT: "+flambda"
+  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:

checker/dune

@@ -7,6 +7,7 @@
  (synopsis "Coq's Standalone Proof Checker")
  (modules :standard \ coqchk votour)
  (wrapped true)
+ (instrumentation (backend bisect_ppx))
  (libraries coq.kernel))
 
 (executable
@@ -16,6 +17,7 @@
  (package coq)
  (modules coqchk)
  (flags :standard -open Coq_checklib)
+ (instrumentation (backend bisect_ppx))
  (libraries coq_checklib))
 
 (executable

clib/dune

@@ -3,6 +3,7 @@
  (synopsis "Coq's Utility Library [general purpose]")
  (public_name coq.clib)
  (wrapped false)
+ (instrumentation (backend bisect_ppx))
  (modules_without_implementation cSig)
  (libraries str unix threads))
 

config/dune

@@ -1,6 +1,7 @@
 (library
  (name config)
  (synopsis "Coq Configuration Variables")
+ (instrumentation (backend bisect_ppx))
  (public_name coq.config)
  (modules :standard \ list_plugins)
  (wrapped false))

dev/dune-workspace.bisect

@@ -0,0 +1,7 @@
+(lang dune 2.7)
+
+(instrument_with bisect_ppx)
+
+(context
+ (default
+  (name coverage)))

dune-project

@@ -1,4 +1,4 @@
-(lang dune 2.5)
+(lang dune 2.7)
 (name coq)
 (using coq 0.2)
 

engine/dune

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

gramlib/dune

@@ -1,4 +1,5 @@
 (library
  (name gramlib)
  (public_name coq.gramlib)
+ (instrumentation (backend bisect_ppx))
  (libraries coq.lib))

interp/dune

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

kernel/dune

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

lib/dune

@@ -3,5 +3,6 @@
  (synopsis "Coq's Utility Library [coq-specific]")
  (public_name coq.lib)
  (wrapped false)
+ (instrumentation (backend bisect_ppx))
  (modules_without_implementation xml_datatype)
  (libraries coq.clib coq.config))

library/dune

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

parsing/dune

@@ -2,6 +2,7 @@
  (name parsing)
  (public_name coq.parsing)
  (wrapped false)
+ (instrumentation (backend bisect_ppx))
  (libraries coq.gramlib interp))
 
 (coq.pp (modules g_prim g_constr))

plugins/ltac/dune

@@ -3,13 +3,15 @@
  (public_name coq.plugins.ltac)
  (synopsis "Coq's LTAC tactic language")
  (modules :standard \ tauto)
+ (instrumentation (backend bisect_ppx))
  (libraries coq.stm))
 
 (library
  (name tauto_plugin)
  (public_name coq.plugins.tauto)
  (synopsis "Coq's tauto tactic")
  (modules tauto)
+ (instrumentation (backend 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)
+ (instrumentation (backend 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)
+ (instrumentation (backend bisect_ppx))
  (libraries engine))

printing/dune

@@ -3,4 +3,5 @@
  (synopsis "Coq's Term Pretty Printing Library")
  (public_name coq.printing)
  (wrapped false)
+ (instrumentation (backend bisect_ppx))
  (libraries parsing proofs))

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)
+ (instrumentation (backend 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)
+ (instrumentation (backend bisect_ppx))
  (libraries vernac))

tactics/dune

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

topbin/dune

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

vernac/dune

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