diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 70e04ee205f6f..35e44dee5e7c4 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -235,7 +235,7 @@ before_script: script: - set -e - echo 'start:coq.test' - - make -f Makefile.ci -j "$NJOBS" "${CI_JOB_NAME#*:}" + # - make -f Makefile.ci -j "$NJOBS" "${CI_JOB_NAME#*:}" - echo 'end:coq.test' - set +e needs: @@ -593,6 +593,28 @@ test-suite:edge+4.11+trunk+dune: expire_in: 2 week allow_failure: true +test-suite:edge+coverage: + stage: stage-1 + dependencies: [] + script: + - opam update + - opam pin add dune --dev + - opam install bisect_ppx + - dune build --workspace dev/dune-workspace.bisect @runtest + - 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+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 dependencies: diff --git a/clib/dune b/clib/dune index 10c75d6aa251c..a546b2cb388a1 100644 --- a/clib/dune +++ b/clib/dune @@ -3,6 +3,7 @@ (synopsis "Coq's Utility Library [general purpose]") (public_name coq.clib) (wrapped false) + (bisect_ppx) (modules_without_implementation cSig) (libraries str unix threads)) diff --git a/config/dune b/config/dune index bf1aa4f471b9c..5cb241c2b5509 100644 --- a/config/dune +++ b/config/dune @@ -1,6 +1,7 @@ (library (name config) (synopsis "Coq Configuration Variables") + (bisect_ppx) (public_name coq.config) (wrapped false)) diff --git a/dev/dune-workspace.bisect b/dev/dune-workspace.bisect new file mode 100644 index 0000000000000..bf84879b479f8 --- /dev/null +++ b/dev/dune-workspace.bisect @@ -0,0 +1,6 @@ +(lang dune 2.6) + +(context + (default + (name coverage) + (bisect_enabled true))) diff --git a/dune-project b/dune-project index 873d03e8ddb93..f557ba5a2e64b 100644 --- a/dune-project +++ b/dune-project @@ -1,6 +1,7 @@ -(lang dune 2.5) +(lang dune 2.6) (name coq) (using coq 0.2) +(using bisect_ppx 1.0) (formatting (enabled_for ocaml)) diff --git a/engine/dune b/engine/dune index e2b7ab9c876f9..f4e63b49f47b3 100644 --- a/engine/dune +++ b/engine/dune @@ -3,4 +3,5 @@ (synopsis "Coq's Tactic Engine") (public_name coq.engine) (wrapped false) + (bisect_ppx) (libraries library)) diff --git a/interp/dune b/interp/dune index e9ef7ba99aa3b..95ac5bc7dddf2 100644 --- a/interp/dune +++ b/interp/dune @@ -3,4 +3,5 @@ (synopsis "Coq's Syntactic Interpretation for AST [notations, implicits]") (public_name coq.interp) (wrapped false) + (bisect_ppx) (libraries pretyping)) diff --git a/kernel/dune b/kernel/dune index 5f7502ef6bd86..c7ee1bc4cba7a 100644 --- a/kernel/dune +++ b/kernel/dune @@ -4,6 +4,7 @@ (public_name coq.kernel) (wrapped false) (modules (:standard \ genOpcodeFiles uint63_31 uint63_63)) + (bisect_ppx) (libraries lib byterun dynlink)) (executable diff --git a/lib/dune b/lib/dune index 83783f9b5cf72..dd3d84124f23e 100644 --- a/lib/dune +++ b/lib/dune @@ -3,5 +3,6 @@ (synopsis "Coq's Utility Library [coq-specific]") (public_name coq.lib) (wrapped false) + (bisect_ppx) (modules_without_implementation xml_datatype) (libraries coq.clib coq.config)) diff --git a/library/dune b/library/dune index 344fad5a75f21..0a0c0e8ba2544 100644 --- a/library/dune +++ b/library/dune @@ -3,6 +3,7 @@ (synopsis "Coq's Loadable Libraries (vo) Support") (public_name coq.library) (wrapped false) + (bisect_ppx) (libraries kernel)) (documentation diff --git a/plugins/ltac/dune b/plugins/ltac/dune index 6558ecbfe81ef..4dc2bec25a8ee 100644 --- a/plugins/ltac/dune +++ b/plugins/ltac/dune @@ -3,6 +3,7 @@ (public_name coq.plugins.ltac) (synopsis "Coq's LTAC tactic language") (modules :standard \ tauto) + (bisect_ppx) (libraries coq.stm)) (library @@ -10,6 +11,7 @@ (public_name coq.plugins.tauto) (synopsis "Coq's tauto tactic") (modules tauto) + (bisect_ppx) (libraries coq.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 a117d09a16b47..264cd8d237fa3 100644 --- a/plugins/ssr/dune +++ b/plugins/ssr/dune @@ -3,6 +3,7 @@ (public_name coq.plugins.ssreflect) (synopsis "Coq's ssreflect plugin") (modules_without_implementation ssrast) + (bisect_ppx) (flags :standard -open Gramlib) (libraries coq.plugins.ssrmatching)) diff --git a/pretyping/dune b/pretyping/dune index 14bce92de10c8..8890242a445b9 100644 --- a/pretyping/dune +++ b/pretyping/dune @@ -3,4 +3,5 @@ (synopsis "Coq's Type Inference Component (Pretyper)") (public_name coq.pretyping) (wrapped false) + (bisect_ppx) (libraries engine)) diff --git a/proofs/dune b/proofs/dune index 36e979999856c..3319213b01888 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.proofs) (wrapped false) + (bisect_ppx) (libraries pretyping)) diff --git a/stm/dune b/stm/dune index c369bd00fb1c5..798f83ddb0e93 100644 --- a/stm/dune +++ b/stm/dune @@ -3,4 +3,5 @@ (synopsis "Coq's Document Manager and Proof Checking Scheduler") (public_name coq.stm) (wrapped false) + (bisect_ppx) (libraries vernac)) diff --git a/tactics/dune b/tactics/dune index 908dde52536dd..93447ac333f21 100644 --- a/tactics/dune +++ b/tactics/dune @@ -3,4 +3,5 @@ (synopsis "Coq's Core Tactics [ML implementation]") (public_name coq.tactics) (wrapped false) + (bisect_ppx) (libraries printing)) diff --git a/topbin/dune b/topbin/dune index 46052c81e524b..8b4e84bedaad3 100644 --- a/topbin/dune +++ b/topbin/dune @@ -8,6 +8,7 @@ (public_name coqtop.opt) (package coq) (modules coqtop_bin) + (bisect_ppx) (libraries coq.toplevel) (link_flags -linkall)) @@ -25,6 +26,7 @@ (public_name coqc) (package coq) (modules coqc_bin) + (bisect_ppx) (libraries coq.toplevel) (modes native byte) ; Adding -ccopt -flto to links options could be interesting, however, diff --git a/toplevel/dune b/toplevel/dune index 2d64ae303c534..d641bfa9b85ab 100644 --- a/toplevel/dune +++ b/toplevel/dune @@ -3,6 +3,7 @@ (public_name coq.toplevel) (synopsis "Coq's Interactive Shell [terminal-based]") (wrapped false) + (bisect_ppx) (libraries num coq.stm)) ; Coqlevel provides the `Num` library to plugins, we could also use ; -linkall in the plugins file, to be discussed. diff --git a/vernac/dune b/vernac/dune index ba361b137710e..19c38169e92e1 100644 --- a/vernac/dune +++ b/vernac/dune @@ -3,6 +3,7 @@ (synopsis "Coq's Vernacular Language") (public_name coq.vernac) (wrapped false) + (bisect_ppx) (libraries tactics parsing)) (coq.pp (modules g_proofs g_vernac))