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

Ack-by: SkySkimmer
Reviewed-by: ejgallego

5 files changed, 59 insertions, 22 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 4a053ec03f..5b343a23c5 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -426,7 +426,16 @@ doc:refman:dune:
   artifacts:
     paths:
       - _build/log
-      - _build/default/doc/sphinx_build/html
+      - _build/default/doc/refman-html
+
+doc:refman-pdf:dune:
+  extends: .dune-ci-template
+  variables:
+    DUNE_TARGET: refman-pdf
+  artifacts:
+    paths:
+      - _build/log
+      - _build/default/doc/refman-pdf
 
 doc:stdlib:dune:
   extends: .dune-ci-template
diff --git a/Makefile.dune b/Makefile.dune
index 499ad0d16b..0520d43da9 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -4,7 +4,7 @@
 .PHONY: help voboot states world watch check          # Main developer targets
 .PHONY: coq coqide coqide-server                      # Package targets
 .PHONY: quickbyte quickopt quickide                   # Partial / quick developer targets
-.PHONY: refman-html stdlib-html apidoc                # Documentation targets
+.PHONY: refman-html refman-pdf stdlib-html apidoc     # Documentation targets
 .PHONY: test-suite release                            # Accessory targets
 .PHONY: fmt ocheck ireport clean                      # Maintenance targets
 
@@ -32,6 +32,7 @@ help:
 	@echo ""
 	@echo "  - test-suite:  run Coq's test suite"
 	@echo "  - refman-html: build Coq's reference manual [HTML version]"
+	@echo "  - refman-pdf:  build Coq's reference manual [PDF version]"
 	@echo "  - stdlib-html: build Coq's Stdlib documentation [HTML version]"
 	@echo "  - apidoc:      build ML API documentation"
 	@echo "  - release:     build Coq in release mode"
@@ -92,6 +93,9 @@ test-suite: voboot
 refman-html: voboot
 	dune build @refman-html
 
+refman-pdf: voboot
+	dune build @refman-pdf
+
 stdlib-html: voboot
 	dune build @stdlib-html
 
diff --git a/coq-refman.opam b/coq-doc.opam
index 937c4b08d3..2f4072955f 100644
--- a/coq-refman.opam
+++ b/coq-doc.opam
@@ -27,7 +27,7 @@ build-env: [
 ]
 
 build: [
-  [ "dune" "build" "@refman" "-j" jobs ]
+  [ "dune" "build" "-p" name "-j" jobs ]
 ]
 
 # Would be better to have a *-conf package?
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))