[build] Add support for code coverage

Closes coq#10267
ejgallego · Dec 6, 2022 · e2d2db1 · e2d2db1
1 parent 756c560
commit e2d2db1
Show file tree

Hide file tree

Showing 22 changed files with 52 additions and 3 deletions.
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
@@ -19,7 +19,7 @@ variables:
   # $DATE is so we can tell what's what in the image list
   # 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-V2022-10-13-2c0347368a"
+  CACHEKEY: "bionic_coq-V2022-10-18-24a491071a"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
 
   # By default, jobs run in the base switch; override to select another switch
@@ -528,6 +528,28 @@ test-suite:edge:dev:
     expire_in: 2 week
   allow_failure: true
 
+test-suite:edge+coverage:
+  stage: build
+  script:
+    - ulimit -s 16384
+    - make dunestrap
+    - 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.boot 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,9 +63,9 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
         i386 env CC='gcc -m32' opam install zarith.1.11 && \
         opam install $BASE_OPAM
 
-# EDGE switch
+# EDGE switch, dune 2.9.1 requires OCaml 4.14, (lablgtk 3.1.2 requies OCaml 4.09)
 ENV COMPILER_EDGE="4.14.0" \
-    BASE_OPAM_EDGE="dune.2.9.3 dune-release.1.6.1 ocamlfind.1.9.1 odoc.2.0.2" \
+    BASE_OPAM_EDGE="dune.2.9.3 dune-release.1.6.1 ocamlfind.1.9.1 odoc.2.0.2 bisect_ppx.2.8.1" \
     CI_OPAM_EDGE="elpi.1.16.5 ppx_import.1.10.0 cmdliner.1.1.1 sexplib.v0.15.1 ppx_sexp_conv.v0.15.1 ppx_hash.v0.15.0 ppx_compare.v0.15.0 ppx_deriving_yojson.3.7.0 yojson.1.7.0" \
     COQIDE_OPAM_EDGE="lablgtk3-sourceview3.3.1.2"
 

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/engine/dune b/engine/dune
@@ -5,4 +5,5 @@
  (wrapped false)
  ; until ocaml/dune#4892 fixed
  ; (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 gramlib))
diff --git a/kernel/dune b/kernel/dune
@@ -5,6 +5,7 @@
  (wrapped false)
  (modules_without_implementation values)
  (modules (:standard \ genOpcodeFiles uint63_31 uint63_63 float64_31 float64_63))
+ (instrumentation (backend bisect_ppx))
  (libraries boot 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.boot 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
@@ -5,4 +5,5 @@
  (wrapped false)
  ; until ocaml/dune#4892 fixed
  ; (private_modules dag proofBlockDelimiter tQueue vcs workerPool)
+ (instrumentation (backend bisect_ppx))
  (libraries sysinit coqworkmgrapi))
diff --git a/tactics/dune b/tactics/dune
@@ -5,4 +5,5 @@
  (wrapped false)
  ; until ocaml/dune#4892 fixed
  ; (private_modules btermdn dn)
+ (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 findlib.dynload))
 
 (executable
@@ -23,6 +24,7 @@
  (public_name coqc)
  (package coq-core)
  (modules coqc_bin)
+ (instrumentation (backend bisect_ppx))
  (libraries coq-core.toplevel findlib.dynload)
  (modes native byte))
  ; Adding -ccopt -flto to links options could be interesting, however,

diff --git a/vernac/dune b/vernac/dune
@@ -5,6 +5,7 @@
  (wrapped false)
  ; until ocaml/dune#4892 fixed
  ; (private_modules comProgramFixpoint egramcoq)
+ (instrumentation (backend bisect_ppx))
  (libraries tactics parsing findlib.dynload))
 
 (coq.pp (modules g_proofs g_vernac))