Merge PR #11855: Build and install refman with Dune.

Ack-by: SkySkimmer
Reviewed-by: ejgallego

2 files changed, 43 insertions, 19 deletions

diff --git a/doc/dune b/doc/dune
index 02ca33b682..4210c0a482 100644
--- a/doc/dune
+++ b/doc/dune
@@ -1,5 +1,10 @@
 (rule
- (targets sphinx_build)
+ (targets unreleased.rst)
+ (deps (source_tree changelog))
+ (action (with-stdout-to %{targets} (bash "cat changelog/00-title.rst changelog/*/*.rst"))))
+
+(alias
+ (name refman-deps)
  (deps
   ; We could use finer dependencies here so the build is faster:
   ;
@@ -10,23 +15,34 @@
   ;   + tools/coqdoc/coqdoc.css
   (package coq)
   (source_tree sphinx)
-  (source_tree tools)
+  (source_tree tools/coqrst)
   unreleased.rst
-  (env_var SPHINXWARNOPT))
- (action
-  (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html)))
+  (env_var SPHINXWARNOPT)))
 
-(alias
- (name refman-html)
- (deps sphinx_build))
+(rule
+ (targets refman-html)
+ (alias refman-html)
+ (package coq-doc)
+ (deps (alias refman-deps))
+ (action
+  (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b html sphinx %{targets})))
 
 (rule
- (targets unreleased.rst)
- (deps (source_tree changelog))
- (action (with-stdout-to %{targets} (bash "cat changelog/00-title.rst changelog/*/*.rst"))))
+ (targets refman-pdf)
+ (alias refman-pdf)
+ (package coq-doc)
+ (deps (alias refman-deps))
+ (action
+  (progn
+   (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b latex sphinx %{targets})
+   (chdir %{targets} (run make)))))
+
+; Installable directories are not yet fully supported by Dune.  See
+; ocaml/dune#1868.  Yet, this makes coq-doc.install a valid target to
+; generate the whole Coq documentation.  And the result under
+; _build/install/default/doc/coq-doc looks just right!
 
-; The install target still needs more work.
-; (install
-;  (section doc)
-;  (package coq-refman)
-;  (files sphinx_build))
+(install
+ (files (refman-html as html/refman) (refman-pdf as pdf/refman))
+ (section doc)
+ (package coq-doc))
diff --git a/doc/stdlib/dune b/doc/stdlib/dune
index 093c7a62b2..0b6ca5f178 100644
--- a/doc/stdlib/dune
+++ b/doc/stdlib/dune
@@ -13,6 +13,8 @@
 
 (rule
   (targets html)
+  (alias stdlib-html)
+  (package coq-doc)
   (deps
    ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg
    (source_tree %{project_root}/theories)
@@ -31,6 +33,12 @@
     (progn (cat %{header}) (cat index-list.html) (cat %{footer})))
    (run cp _index.html html/index.html))))
 
-(alias
- (name stdlib-html)
- (deps html))
+; Installable directories are not yet fully supported by Dune.  See
+; ocaml/dune#1868.  Yet, this makes coq-doc.install a valid target to
+; generate the whole Coq documentation.  And the result under
+; _build/install/default/doc/coq-doc looks just right!
+
+(install
+ (files (html as html/stdlib))
+ (section doc)
+ (package coq-doc))