[build] Add support for code coverage

Closes coq#10267
ejgallego · Mar 19, 2024 · 69b5b8a · 69b5b8a
1 parent c61c078
commit 69b5b8a
Show file tree

Hide file tree

Showing 22 changed files with 51 additions and 2 deletions.
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
@@ -37,7 +37,7 @@ variables:
   # echo $(md5sum dev/ci/docker/old_ubuntu_lts/Dockerfile | head -c 10)
   # echo $(md5sum dev/ci/docker/edge_ubuntu/Dockerfile | head -c 10)
   BASE_CACHEKEY: "old_ubuntu_lts-V2024-01-08-011994e15c"
-  EDGE_CACHEKEY: "edge_ubuntu-V2024-02-08-3ed9c93d7c"
+  EDGE_CACHEKEY: "edge_ubuntu-V2024-02-08-314a65abcb"
   BASE_IMAGE: "$CI_REGISTRY_IMAGE:$BASE_CACHEKEY"
   EDGE_IMAGE: "$CI_REGISTRY_IMAGE:$EDGE_CACHEKEY"
 
@@ -538,6 +538,28 @@ test-suite:base: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
@@ -8,6 +8,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
@@ -18,6 +19,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/edge_ubuntu/Dockerfile b/dev/ci/docker/edge_ubuntu/Dockerfile
@@ -39,7 +39,7 @@ ENV NJOBS="2" \
 ENV COMPILER="4.14.1" \
     BASE_OPAM="zarith.1.13 ounit2.2.2.6" \
     CI_OPAM="ocamlgraph.2.0.0 cppo.1.6.9" \
-    BASE_OPAM_EDGE="dune.3.14.0 dune-build-info.3.14.0 dune-release.2.0.0 ocamlfind.1.9.6 odoc.2.3.1" \
+    BASE_OPAM_EDGE="dune.3.14.0 dune-build-info.3.14.0 dune-release.2.0.0 ocamlfind.1.9.6 odoc.2.3.1 bisect_ppx.2.8.3" \
     CI_OPAM_EDGE="elpi.1.18.1 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.2.1.0 uri.4.2.0 ppx_yojson_conv.v0.15.1 ppx_inline_test.v0.15.1 ppx_assert.v0.15.0 ppx_optcomp.v0.15.0 lsp.1.16.2 sel.0.4.0" \
     COQIDE_OPAM_EDGE="lablgtk3-sourceview3.3.1.3"
 

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
@@ -2,4 +2,5 @@
  (name gramlib)
  (public_name coq-core.gramlib)
  (modules_without_implementation plexing)
+ (instrumentation (backend bisect_ppx))
  (libraries coq-core.lib))
diff --git a/interp/dune b/interp/dune
@@ -4,4 +4,5 @@
  (public_name coq-core.interp)
  (wrapped false)
  (modules_without_implementation constrexpr notation_term)
+ (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 declarations entries)
  (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,6 +3,7 @@
  (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
@@ -3,6 +3,7 @@
  (public_name coq-core.parsing)
  (wrapped false)
  (modules_without_implementation notation_gram)
+ (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.vernac))
 
 (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
@@ -4,4 +4,5 @@
  (public_name coq-core.pretyping)
  (wrapped false)
  (modules_without_implementation locus pattern glob_term ltac_pretype)
+ (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
@@ -4,4 +4,5 @@
  (public_name coq-core.proofs)
  (wrapped false)
  (modules_without_implementation tactypes)
+ (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 coqworkmgrlib))
diff --git a/tactics/dune b/tactics/dune
@@ -6,4 +6,5 @@
  (modules_without_implementation genredexpr)
  ; 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 exe byte))
  ; Adding -ccopt -flto to links options could be interesting, however,

diff --git a/vernac/dune b/vernac/dune
@@ -6,6 +6,7 @@
  (modules_without_implementation vernacexpr)
  ; 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))