aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-09-28 17:31:03 +0200
committerEmilio Jesus Gallego Arias2018-09-28 17:36:49 +0200
commit834bd20dc5d6024933e7f859ad5e697fc8b27b9d (patch)
tree4e3a7819dc1697316053d883ac9d4e09af2eac45
parent0bcbc990dcebce2e66f10aba462c9fed2c2eda06 (diff)
[dune] Pack checker to avoid [odoc] problems + build doc for plugins.
We also build documentation for plugins, for example Ltac_plugin is often used in other plugins.
-rw-r--r--Makefile.dune5
-rw-r--r--checker/dune22
2 files changed, 15 insertions, 12 deletions
diff --git a/Makefile.dune b/Makefile.dune
index 81afa5bb91..1e401a57b9 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -34,11 +34,8 @@ watch: voboot
release: voboot
dune build $(DUNEOPT) -p coq
-apidoc:
- # Ugly workaround for https://github.com/ocaml/odoc/issues/148
- mv checker/dune checker/dune.disabled || true
+apidoc: voboot
dune build $(DUNEOPT) @doc
- mv checker/dune.disabled checker/dune || true
clean:
dune clean
diff --git a/checker/dune b/checker/dune
index d918f853dd..d520171f98 100644
--- a/checker/dune
+++ b/checker/dune
@@ -3,24 +3,30 @@
(rule (copy %{project_root}/kernel/esubst.ml esubst.ml))
(rule (copy %{project_root}/kernel/esubst.mli esubst.mli))
+; Careful with bug https://github.com/ocaml/odoc/issues/148
+;
+; If we don't pack checker we will have a problem here due to
+; duplicate module names in the whole build.
(library
- (name checker)
- (public_name coq.checker)
+ (name checklib)
+ (public_name coq.checklib)
(synopsis "Coq's Standalone Proof Checker")
- (modules values analyze names esubst)
- (wrapped false)
+ (modules :standard \ main votour)
+ (modules_without_implementation cic)
+ (wrapped true)
(libraries coq.lib))
(executable
(name main)
(public_name coqchk)
- (modules :standard \ votour values analyze names esubst)
- (modules_without_implementation cic)
- (libraries coq.checker))
+ (modules main)
+ (flags :standard -open Checklib)
+ (libraries coq.checklib))
(executable
(name votour)
(public_name votour)
(modules votour)
- (libraries coq.checker))
+ (flags :standard -open Checklib)
+ (libraries coq.checklib))