diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index b22593c151187..e992e74f04fd3 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -16,7 +16,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-10-01-7c5b78d50f" + CACHEKEY: "bionic_coq-V2021-11-03-bec9b3e909" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -567,6 +567,27 @@ test-suite:edge:dune:dev: # variables: # OCAMLVER: 4.12.0+trunk +test-suite:edge+coverage: + stage: build + 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 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 9f96aa190ee73..518e3c05390b8 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 97f7ae0728d32..720686e9c63e7 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -62,8 +62,8 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ opam install $BASE_OPAM # EDGE switch, dune 2.8 is required for OCaml 4.12 -ENV COMPILER_EDGE="4.13.0" \ - BASE_OPAM_EDGE="dune.2.9.1 dune-release.1.5.0" +ENV COMPILER_EDGE="4.13.1" \ + BASE_OPAM_EDGE="dune.2.9.1 dune-release.1.5.1 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 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/dune-project b/dune-project index 251fbd92aabb9..9ec912cc9ce87 100644 --- 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 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 793ce48ea300f..1f9a5894c96b2 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)) diff --git a/kernel/dune b/kernel/dune index 88d059e725b69..b38a205ade49a 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 5f3bc811d9041..239e280be9be3 100644 --- a/tactics/dune +++ b/tactics/dune @@ -5,4 +5,5 @@ (wrapped false) ; until ocaml/dune#4892 fixed ; (private_modules btermdn dnet dn term_dnet) + (instrumentation (backend bisect_ppx)) (libraries printing)) diff --git a/topbin/dune b/topbin/dune index 36d8b1ba9b465..b93bad9f4567e 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) (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 index 90010b58946ac..be3fbae930318 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)) (coq.pp (modules g_proofs g_vernac))