diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index d9dfd0d22b7ec..6211b5daac012 100644 --- 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 index fc2a35e0e1b3d..8d0e3522f1430 100644 --- 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 index 90f36d8bfd5c7..146795a34c188 100644 --- 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 index 7b34ecb41bc8a..f5252e29dce2d 100644 --- 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 index f0228dba47278..635e18ae21a32 100644 --- 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 new file mode 100644 index 0000000000000..6716c1bb73e39 --- /dev/null +++ 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 index f95496ded2291..d5081fac6ff18 100644 --- 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 index 62c64b0c1a7ba..d762622cbef70 100644 --- 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 index 811267cbe25de..888d1ab561e6e 100644 --- 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 index 8129fa876e402..af3e3cbd0bffe 100644 --- 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 boot lib coqrun dynlink)) (executable diff --git a/lib/dune b/lib/dune index 43ee8f7a58ccd..d3a4e795387f4 100644 --- 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 index bf90511ead9d2..ab2ded4dec9d8 100644 --- 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 index 17011d10de374..b7d170da068c4 100644 --- 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 index 9ec2b10873a6b..6dd82552fe8a9 100644 --- a/plugins/ltac/dune +++ b/plugins/ltac/dune @@ -3,6 +3,7 @@ (public_name coq-core.plugins.ltac) (synopsis "Coq's LTAC tactic language") (modules :standard \ tauto) + (instrumentation (backend bisect_ppx)) (libraries coq-core.stm)) (library @@ -10,6 +11,7 @@ (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 index 4c28776bb7f63..c716d96b2b848 100644 --- 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 index d9b5609bd46c0..a002b0c9c375c 100644 --- 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 index a24a7535ebbff..267c2e9f0be6c 100644 --- 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 index f8e7661997a8e..e9d7a4039863c 100644 --- 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 index ae9f0e94c3081..81a07a12df9ee 100644 --- 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)) diff --git a/tactics/dune b/tactics/dune index 840699eafaced..156ceeb7a9406 100644 --- 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 index a5f4539f5d371..4d82ac4fd6ce4 100644 --- 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 index 22f6a41a69d26..5225c86a39436 100644 --- 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))