[dune] [doc] Support for building the reference manual with Dune.

We just call Sphinx, and generate a promoted install file for the
refman package. This should go away once Dune allows to have full
directories as targets.

.gitlab-ci.yml

@@ -283,6 +283,21 @@ doc:refman:
   dependencies:
     - build:base
 
+doc:refman:dune:
+  <<: *dune-template
+  dependencies:
+    - build:base
+  stage: test
+  dependencies:
+    - build:egde:dune:dev
+  variables:
+    OPAM_SWITCH: edge
+    DUNE_TARGET: refman
+  artifacts:
+    name: "$CI_JOB_NAME"
+    paths:
+      - _build/default/doc/sphinx/_build/html
+
 doc:ml-api:odoc:
   stage: test
   dependencies:

Makefile.dune

@@ -1,7 +1,7 @@
 # -*- mode: makefile -*-
 # Dune Makefile for Coq
 
-.PHONY: help voboot states world watch check quickbyte quickopt test-suite release apidoc ocheck ireport clean bootstrap bootstrap-build
+.PHONY: help voboot states world watch check quickbyte quickopt test-suite release refman apidoc ocheck ireport clean bootstrap bootstrap-build
 
 # use DUNEOPT=--display=short for a more verbose build
 # DUNEOPT=--display=short
@@ -18,6 +18,7 @@ help:
 	@echo "  - quickopt:   build main ML files [coqtop + plugins + ide + printers] using the optimizing compiler"
 	@echo "  - test-suite: run Coq's test suite"
 	@echo "  - release: build Coq in release mode"
+	@echo "  - refman:  build Coq's reference manual"
 	@echo "  - apidoc:  build ML API documentation"
 	@echo "  - ocheck:  build for all supported OCaml versions [requires OPAM]"
 	@echo "  - ireport: build with optimized flambda settings and emit an inline report"
@@ -62,6 +63,9 @@ test-suite: voboot
 release: voboot
 	dune build $(DUNEOPT) -p coq
 
+refman: voboot
+	dune build @refman
+
 apidoc: voboot
 	dune build $(DUNEOPT) @doc
 

config/dune

@@ -7,7 +7,7 @@
 ; Dune doesn't use configure's output, but it is still necessary for
 ; some Coq files to work; will be fixed in the future.
 (rule
- (targets coq_config.ml Makefile)
+ (targets coq_config.ml coq_config.py Makefile)
  (mode fallback)
  (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX))
  (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no))))

coq-refman.opam

@@ -0,0 +1,22 @@
+opam-version: "1.2"
+maintainer: "The Coq development team <coqdev@inria.fr>"
+authors: "The Coq development team, INRIA, CNRS, and contributors."
+homepage: "https://coq.inria.fr/"
+bug-reports: "https://github.com/coq/coq/issues"
+dev-repo: "https://github.com/coq/coq.git"
+license: "LGPL-2.1"
+
+available: [ ocaml-version >= "4.02.3" ]
+
+depends: [
+  "dune"      { build }
+  "coq"       { build }
+]
+
+build-env: [
+  [ COQ_CONFIGURE_PREFIX = "%{prefix}" ]
+]
+
+build: [
+  [ "dune" "build" "@refman" ]
+]

doc/tools/coqrst/coqdoc/main.py

@@ -35,7 +35,7 @@
 
 def coqdoc(coq_code, coqdoc_bin=None):
     """Get the output of coqdoc on coq_code."""
-    coqdoc_bin = coqdoc_bin or os.path.join(os.getenv("COQBIN"), "coqdoc")
+    coqdoc_bin = coqdoc_bin or os.path.join(os.getenv("COQBIN") or "", "coqdoc")
     fd, filename = mkstemp(prefix="coqdoc-", suffix=".v")
     if platform.system().startswith("CYGWIN"):
         # coqdoc currently doesn't accept cygwin style paths in the form "/cygdrive/c/..."

dune

@@ -40,3 +40,35 @@
  (name runtest)
  (package coqide-server)
  (deps test-suite/summary.log))
+
+; Waiting for dune#1377
+; (install
+;  (section doc)
+;  (package coq-refman)
+;  (files
+;    (doc/sphinx/_build/html/index.html as refman/html/index.html)))
+
+; This will hopefully be available soon, see
+; https://github.com/ocaml/dune/issues/1377
+; (rule
+;   (targets doc/sphinx/_build/html/
+
+(alias
+ (name refman)
+ (deps
+  ; We could use finer dependencies here.
+  ; theories/Init/Prelude.vo
+  ; config/coq_config.py
+  ; tools/coqdoc/coqdoc.css
+  ; @rgrinberg mentions that this should be supported.
+  ; %{bin:coqdoc}
+  ; Must find a solution for the _static folder
+  ; doc/sphinx/_static/
+  (package coq)
+  (source_tree doc/sphinx)
+  (source_tree doc/tools))
+ (action (progn
+          ; This will force us to build coqdoc for now
+          (run coqdoc)
+          (run sphinx-build -j4 -b html -d doc/sphinx/_build/doctrees doc/sphinx doc/sphinx/_build/html))))
+