[build] Add support for code coverage

Closes coq#10267
ejgallego · Aug 17, 2021 · 8e903cf · 8e903cf
1 parent 23a8a7e
commit 8e903cf
Show file tree

Hide file tree

Showing 23 changed files with 52 additions and 3 deletions.
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
@@ -20,7 +20,7 @@ variables:
   # Format: $IMAGE-V$DATE-$hash
   # The $hash is the first 10 characters of the md5 of the Dockerfile. e.g.
   # echo $(md5sum dev/ci/docker/bionic_coq/Dockerfile | head -c 10)
-  CACHEKEY: "bionic_coq-V2021-07-23-66f5817edb"
+  CACHEKEY: "bionic_coq-V2021-08-18-712ebd97ce"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
@@ -594,6 +594,28 @@ test-suite:edge:dune:dev:
 #   variables:
 #     OCAMLVER: 4.12.0+trunk
 
+test-suite:edge+coverage:
+  stage: stage-1
+  dependencies: []
+  script:
+    - ulimit -s 16384
+    - dune build --instrument-with bisect_ppx --workspace dev/dune-workspace.bisect @runtest
+    - find _build/coverage/ -name *.coverage -size 0 -exec rm {} \; # workaround truncated coverage file 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
   needs:

diff --git a/checker/dune b/checker/dune
@@ -7,6 +7,7 @@
  (synopsis "Coq's Standalone Proof Checker")
  (modules :standard \ coqchk votour)
  (wrapped true)
+ (instrumentation (backend bisect_ppx))
  (libraries coq-core.kernel))
 
 (executable
@@ -17,6 +18,7 @@
  (package coq-core)
  (modules coqchk)
  (flags :standard -open Coq_checklib)
+ (instrumentation (backend bisect_ppx))
  (libraries coq_checklib))
 
 (executable

diff --git a/clib/dune b/clib/dune
@@ -3,5 +3,6 @@
  (synopsis "Coq's Utility Library [general purpose]")
  (public_name coq-core.clib)
  (wrapped false)
+ (instrumentation (backend bisect_ppx))
  (modules_without_implementation cSig)
  (libraries str unix threads))
diff --git a/config/dune b/config/dune
@@ -1,6 +1,7 @@
 (library
  (name config)
  (synopsis "Coq Configuration Variables")
+ (instrumentation (backend bisect_ppx))
  (public_name coq-core.config)
  (modules :standard \ list_plugins)
  (wrapped false))

diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
@@ -63,7 +63,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
 
 # EDGE switch, dune 2.8 is required for OCaml 4.12
 ENV COMPILER_EDGE="4.12.0" \
-    BASE_OPAM_EDGE="dune.2.8.5 dune-release.1.4.0"
+    BASE_OPAM_EDGE="dune.2.8.5 dune-release.1.4.0 bisect_ppx.2.6.0"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
 # `ci-template-flambda` with everything.

diff --git a/dev/dune-workspace.bisect b/dev/dune-workspace.bisect
@@ -0,0 +1,5 @@
+(lang dune 2.7)
+
+(context
+ (default
+  (name coverage)))
diff --git a/dune-project b/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.5)
+(lang dune 2.7)
 (name coq)
 (using coq 0.2)
 

diff --git a/engine/dune b/engine/dune
@@ -4,4 +4,5 @@
  (public_name coq-core.engine)
  (wrapped false)
  (private_modules univSubst)
+ (instrumentation (backend bisect_ppx))
  (libraries library))
diff --git a/gramlib/dune b/gramlib/dune
@@ -1,4 +1,5 @@
 (library
  (name gramlib)
  (public_name coq-core.gramlib)
+ (instrumentation (backend bisect_ppx))
  (libraries coq-core.lib))
diff --git a/interp/dune b/interp/dune
@@ -3,4 +3,5 @@
  (synopsis "Coq's Syntactic Interpretation for AST [notations, implicits]")
  (public_name coq-core.interp)
  (wrapped false)
+ (instrumentation (backend bisect_ppx))
  (libraries zarith pretyping))
diff --git a/kernel/dune b/kernel/dune
@@ -4,6 +4,7 @@
  (public_name coq-core.kernel)
  (wrapped false)
  (modules (:standard \ genOpcodeFiles uint63_31 uint63_63 float64_31 float64_63))
+ (instrumentation (backend bisect_ppx))
  (libraries lib coqrun dynlink))
 
 (executable

diff --git a/lib/dune b/lib/dune
@@ -3,5 +3,6 @@
  (synopsis "Coq's Utility Library [coq-specific]")
  (public_name coq-core.lib)
  (wrapped false)
+ (instrumentation (backend bisect_ppx))
  (modules_without_implementation xml_datatype)
  (libraries coq-core.clib coq-core.config))
diff --git a/library/dune b/library/dune
@@ -3,6 +3,7 @@
  (synopsis "Coq's Loadable Libraries (vo) Support")
  (public_name coq-core.library)
  (wrapped false)
+ (instrumentation (backend bisect_ppx))
  (libraries kernel))
 
 (documentation

diff --git a/parsing/dune b/parsing/dune
@@ -2,6 +2,7 @@
  (name parsing)
  (public_name coq-core.parsing)
  (wrapped false)
+ (instrumentation (backend bisect_ppx))
  (libraries coq-core.gramlib interp))
 
 (coq.pp (modules g_prim g_constr))
diff --git a/plugins/ltac/dune b/plugins/ltac/dune
@@ -3,13 +3,15 @@
  (public_name coq-core.plugins.ltac)
  (synopsis "Coq's LTAC tactic language")
  (modules :standard \ tauto)
+ (instrumentation (backend bisect_ppx))
  (libraries coq-core.stm))
 
 (library
  (name tauto_plugin)
  (public_name coq-core.plugins.tauto)
  (synopsis "Coq's tauto tactic")
  (modules tauto)
+ (instrumentation (backend bisect_ppx))
  (libraries coq-core.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))
diff --git a/plugins/ssr/dune b/plugins/ssr/dune
@@ -3,6 +3,7 @@
  (public_name coq-core.plugins.ssreflect)
  (synopsis "Coq's ssreflect plugin")
  (modules_without_implementation ssrast)
+ (instrumentation (backend bisect_ppx))
  (flags :standard -open Gramlib)
  (libraries coq-core.plugins.ssrmatching))
 

diff --git a/pretyping/dune b/pretyping/dune
@@ -3,4 +3,5 @@
  (synopsis "Coq's Type Inference Component (Pretyper)")
  (public_name coq-core.pretyping)
  (wrapped false)
+ (instrumentation (backend bisect_ppx))
  (libraries engine))
diff --git a/printing/dune b/printing/dune
@@ -3,4 +3,5 @@
  (synopsis "Coq's Term Pretty Printing Library")
  (public_name coq-core.printing)
  (wrapped false)
+ (instrumentation (backend bisect_ppx))
  (libraries parsing proofs))
diff --git a/proofs/dune b/proofs/dune
@@ -3,4 +3,5 @@
  (synopsis "Coq's Higher-level Refinement Proof Engine and Top-level Proof Structure")
  (public_name coq-core.proofs)
  (wrapped false)
+ (instrumentation (backend bisect_ppx))
  (libraries pretyping))
diff --git a/stm/dune b/stm/dune
@@ -4,4 +4,5 @@
  (public_name coq-core.stm)
  (wrapped false)
  (private_modules dag proofBlockDelimiter tQueue vcs workerPool)
+ (instrumentation (backend bisect_ppx))
  (libraries sysinit))
diff --git a/tactics/dune b/tactics/dune
@@ -4,4 +4,5 @@
  (public_name coq-core.tactics)
  (wrapped false)
  (private_modules btermdn dnet dn term_dnet)
+ (instrumentation (backend bisect_ppx))
  (libraries printing))
diff --git a/topbin/dune b/topbin/dune
@@ -8,6 +8,7 @@
  (public_name coqtop.opt)
  (package coq-core)
  (modules coqtop_bin)
+ (instrumentation (backend bisect_ppx))
  (libraries coq-core.toplevel)
  (link_flags -linkall))
 
@@ -25,6 +26,7 @@
  (public_name coqc)
  (package coq-core)
  (modules coqc_bin)
+ (instrumentation (backend bisect_ppx))
  (libraries coq-core.toplevel)
  (modes native byte)
  ; Adding -ccopt -flto to links options could be interesting, however,

diff --git a/vernac/dune b/vernac/dune
@@ -4,6 +4,7 @@
  (public_name coq-core.vernac)
  (wrapped false)
  (private_modules comProgramFixpoint egramcoq)
+ (instrumentation (backend bisect_ppx))
  (libraries tactics parsing))
 
 (coq.pp (modules g_proofs g_vernac))