diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index e8ee0c537b83e..4a12e04307970 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -593,6 +593,34 @@ test-suite:edge+4.11+trunk+dune: expire_in: 2 week allow_failure: true +test-suite:edge+coverage: + stage: stage-1 + dependencies: [] + script: + - ulimit -s 16384 + - opam update + - opam remove opam-format dune-release # Broken so it seems + - opam pin add -n dune-configurator --dev + - opam pin add -n dune-private-libs --dev + - opam pin add dune --dev + - opam install bisect_ppx + - dune build --workspace dev/dune-workspace.bisect @runtest + - find _build/coverage/ -name *.coverage -size 0 -exec rm {} \; # workaround truncation 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 dependencies: diff --git a/checker/dune b/checker/dune index af7d4f2923a9e..61aff64dedf28 100644 --- a/checker/dune +++ b/checker/dune @@ -7,6 +7,7 @@ (synopsis "Coq's Standalone Proof Checker") (modules :standard \ coqchk votour) (wrapped true) + (bisect_ppx) (libraries coq.kernel)) (executable @@ -16,6 +17,7 @@ (package coq) (modules coqchk) (flags :standard -open Coq_checklib) + (bisect_ppx) (libraries coq_checklib)) (executable 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/gramlib/dune b/gramlib/dune index 8ca6aff25a5b4..2e93414da62d0 100644 --- a/gramlib/dune +++ b/gramlib/dune @@ -1,4 +1,5 @@ (library (name gramlib) (public_name coq.gramlib) + (bisect_ppx) (libraries coq.lib)) 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/parsing/dune b/parsing/dune index 8a31434101d40..78415940449ef 100644 --- a/parsing/dune +++ b/parsing/dune @@ -2,6 +2,7 @@ (name parsing) (public_name coq.parsing) (wrapped false) + (bisect_ppx) (libraries coq.gramlib interp)) (coq.pp (modules g_prim g_constr)) 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/printing/dune b/printing/dune index 3392342165568..48c5abf3ba2f4 100644 --- a/printing/dune +++ b/printing/dune @@ -3,4 +3,5 @@ (synopsis "Coq's Term Pretty Printing Library") (public_name coq.printing) (wrapped false) + (bisect_ppx) (libraries parsing proofs)) 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))