Skip to content

Commit

Permalink
[dune] Enable ppx_bisect
Browse files Browse the repository at this point in the history
The way to run this is:
```
BISECT_ENABLE=yes make -f Makefile.dune test-suite
bisect-ppx-report -I _build/default -html coq-coverage `find . -name 'bisect*.out'
```

Note that support for bisect is still not very optimal
c.f. ocaml/dune#57 , and in particular
support for incremental runs is kinda broken, so running from a clean
tree is recommended for now.
  • Loading branch information
ejgallego committed Oct 30, 2019
1 parent 28ea499 commit d91c904
Show file tree
Hide file tree
Showing 17 changed files with 18 additions and 1 deletion.
3 changes: 2 additions & 1 deletion clib/dune
Original file line number Diff line number Diff line change
Expand Up @@ -4,5 +4,6 @@
(public_name coq.clib)
(wrapped false)
(modules_without_implementation cSig)
(libraries str unix threads))
(preprocess (pps bisect_ppx -conditional -no-comment-parsing))
(libraries str unix threads bisect_ppx.runtime))

1 change: 1 addition & 0 deletions engine/dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,5 @@
(synopsis "Coq's Tactic Engine")
(public_name coq.engine)
(wrapped false)
(preprocess (pps bisect_ppx -conditional -no-comment-parsing))
(libraries library))
1 change: 1 addition & 0 deletions gramlib/dune
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
(library
(name gramlib)
(public_name coq.gramlib)
(preprocess (pps bisect_ppx -conditional -no-comment-parsing))
(libraries coq.lib))
1 change: 1 addition & 0 deletions interp/dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,5 @@
(synopsis "Coq's Syntactic Interpretation for AST [notations, implicits]")
(public_name coq.interp)
(wrapped false)
(preprocess (pps bisect_ppx -conditional -no-comment-parsing))
(libraries pretyping))
1 change: 1 addition & 0 deletions kernel/dune
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
(public_name coq.kernel)
(wrapped false)
(modules (:standard \ genOpcodeFiles uint63_31 uint63_63))
(preprocess (pps bisect_ppx -conditional -no-comment-parsing))
(libraries lib byterun dynlink))

(executable
Expand Down
1 change: 1 addition & 0 deletions lib/dune
Original file line number Diff line number Diff line change
Expand Up @@ -4,4 +4,5 @@
(public_name coq.lib)
(wrapped false)
(modules_without_implementation xml_datatype)
(preprocess (pps bisect_ppx -conditional -no-comment-parsing))
(libraries coq.clib coq.config))
1 change: 1 addition & 0 deletions library/dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
(synopsis "Coq's Loadable Libraries (vo) Support")
(public_name coq.library)
(wrapped false)
(preprocess (pps bisect_ppx -conditional -no-comment-parsing))
(libraries kernel))

(documentation
Expand Down
1 change: 1 addition & 0 deletions parsing/dune
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
(name parsing)
(public_name coq.parsing)
(wrapped false)
(preprocess (pps bisect_ppx -conditional -no-comment-parsing))
(libraries coq.gramlib interp))

(coq.pp (modules g_prim g_constr))
1 change: 1 addition & 0 deletions plugins/ltac/plugin_base.dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
(public_name coq.plugins.ltac)
(synopsis "Coq's LTAC tactic language")
(modules :standard \ tauto)
(preprocess (pps bisect_ppx -conditional -no-comment-parsing))
(libraries coq.stm))

(library
Expand Down
1 change: 1 addition & 0 deletions plugins/ssr/plugin_base.dune
Original file line number Diff line number Diff line change
Expand Up @@ -4,4 +4,5 @@
(synopsis "Coq's ssreflect plugin")
(modules_without_implementation ssrast)
(flags :standard -open Gramlib)
(preprocess (pps bisect_ppx -conditional -no-comment-parsing))
(libraries coq.plugins.ssrmatching))
1 change: 1 addition & 0 deletions pretyping/dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,5 @@
(synopsis "Coq's Type Inference Component (Pretyper)")
(public_name coq.pretyping)
(wrapped false)
(preprocess (pps bisect_ppx -conditional -no-comment-parsing))
(libraries engine))
1 change: 1 addition & 0 deletions printing/dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,5 @@
(synopsis "Coq's Term Pretty Printing Library")
(public_name coq.printing)
(wrapped false)
(preprocess (pps bisect_ppx -conditional -no-comment-parsing))
(libraries parsing proofs))
1 change: 1 addition & 0 deletions proofs/dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,5 @@
(synopsis "Coq's Higher-level Refinement Proof Engine and Top-level Proof Structure")
(public_name coq.proofs)
(wrapped false)
(preprocess (pps bisect_ppx -conditional -no-comment-parsing))
(libraries pretyping))
1 change: 1 addition & 0 deletions stm/dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,5 @@
(synopsis "Coq's Document Manager and Proof Checking Scheduler")
(public_name coq.stm)
(wrapped false)
(preprocess (pps bisect_ppx -conditional -no-comment-parsing))
(libraries vernac))
1 change: 1 addition & 0 deletions tactics/dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,5 @@
(synopsis "Coq's Core Tactics [ML implementation]")
(public_name coq.tactics)
(wrapped false)
(preprocess (pps bisect_ppx -conditional -no-comment-parsing))
(libraries printing))
1 change: 1 addition & 0 deletions user-contrib/Ltac2/plugin_base.dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,5 @@
(public_name coq.plugins.ltac2)
(synopsis "Coq's Ltac2 plugin")
(modules_without_implementation tac2expr tac2qexpr tac2types)
(preprocess (pps bisect_ppx -conditional -no-comment-parsing))
(libraries coq.plugins.ltac))
1 change: 1 addition & 0 deletions vernac/dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
(synopsis "Coq's Vernacular Language")
(public_name coq.vernac)
(wrapped false)
(preprocess (pps bisect_ppx -conditional -no-comment-parsing))
(libraries tactics parsing))

(coq.pp (modules g_proofs g_vernac))

0 comments on commit d91c904

Please sign in to comment.