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

This is a reduced version of coq#8503 as to provide a way to build the
reference manual with Dune.

Dune 1.6 supports (experimentally) directories as targets, thus we
introduce a rule that will call `sphinx` to build the manual.

This only provides build, however generation of `.install` rules is
not done, it will be hopefully addressed in coq#8503.

Note that we set `expire: 1 month` for all the artifacts we build with
Dune. IMHO this makes most sense as not to abuse Gitlab's hosting,
however of course we could consider a different deployment strategy if
wanted.

.gitlab-ci.yml

@@ -9,7 +9,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-V2018-11-08-V1"
+  CACHEKEY: "bionic_coq-V2018-12-05-V1"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
@@ -89,18 +89,37 @@ after_script:
 
     - set +e
 
+# Template for building Coq + stdlib, typical use: overload the switch
 .dune-template: &dune-template
-  dependencies: []
   stage: build
+  dependencies: []
+  script:
+    - set -e
+    - make -f Makefile.dune world
+    - set +e
+  variables:
+    OPAM_SWITCH: edge
   artifacts:
     name: "$CI_JOB_NAME"
     paths:
       - _build/
     expire_in: 1 week
+
+.dune-ci-template: &dune-ci-template
+  stage: test
+  dependencies:
+    - build:egde:dune:dev
   script:
     - set -e
+    - echo 'start:coq.test'
     - make -f Makefile.dune "$DUNE_TARGET"
+    - echo 'end:coq.test'
     - set +e
+  variables: &dune-ci-template-vars
+    OPAM_SWITCH: edge
+  artifacts: &dune-ci-template-artifacts
+    name: "$CI_JOB_NAME"
+    expire_in: 1 month
 
 # every non build job must set dependencies otherwise all build
 # artifacts are used together and we may get some random Coq. To that
@@ -221,9 +240,6 @@ build:edge+flambda:
 
 build:egde:dune:dev:
   <<: *dune-template
-  variables:
-    OPAM_SWITCH: edge
-    DUNE_TARGET: world
 
 build:base+async:
   <<: *build-template
@@ -291,15 +307,23 @@ doc:refman:
   dependencies:
     - build:base
 
+doc:refman:dune:
+  <<: *dune-ci-template
+  variables:
+    <<: *dune-ci-template-vars
+    DUNE_TARGET: refman-html
+  artifacts:
+    <<: *dune-ci-template-artifacts
+    paths:
+      - _build/default/doc/sphinx_build/html
+
 doc:ml-api:odoc:
-  stage: test
-  dependencies:
-    - build:egde:dune:dev
-  script: make -f Makefile.dune apidoc
+  <<: *dune-ci-template
   variables:
-    OPAM_SWITCH: edge
+    <<: *dune-ci-template-vars
+    DUNE_TARGET: apidoc
   artifacts:
-    name: "$CI_JOB_NAME"
+    <<: *dune-ci-template-artifacts
     paths:
       - _build/default/_doc/
 

Makefile.dune

@@ -1,7 +1,10 @@
 # -*- mode: makefile -*-
 # Dune Makefile for Coq
 
-.PHONY: help voboot states world watch check quickbyte quickopt test-suite release apidoc ocheck ireport clean
+.PHONY: help voboot states world watch check          # Main developer targets
+.PHONY: quickbyte quickopt                            # Partial / quick developer targets
+.PHONY: test-suite refman-html apidoc release         # Accesory targets
+.PHONY: ocheck ireport clean                          # Maintenance targets
 
 # use DUNEOPT=--display=short for a more verbose build
 # DUNEOPT=--display=short
@@ -10,15 +13,20 @@ BUILD_CONTEXT=_build/default
 
 help:
 	@echo "Welcome to Coq's Dune-based build system. Targets are:"
-	@echo "  - states:  build a minimal functional coqtop"
-	@echo "  - world:   build all binaries and libraries"
-	@echo "  - watch:   build all binaries and libraries [continuous build]"
-	@echo "  - check:   build all ML files as fast as possible [requires Dune >= 1.5.0]"
-	@echo "  - quickbyte:  build main ML files [coqtop + plugins + ide + printers] using the bytecode compiler"
-	@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 "  - apidoc:  build ML API documentation"
+	@echo ""
+	@echo "  - states: build a minimal functional coqtop"
+	@echo "  - world:  build all binaries and libraries"
+	@echo "  - watch:  build all binaries and libraries [continuous build]"
+	@echo "  - check:  build all ML files as fast as possible"
+	@echo ""
+	@echo "  - quickbyte: build main ML files [coqtop + plugins + ide + printers] using the bytecode compiler"
+	@echo "  - quickopt:  build main ML files [coqtop + plugins + ide + printers] using the optimizing compiler"
+	@echo ""
+	@echo "  - test-suite:  run Coq's test suite"
+	@echo "  - refman-html: build Coq's reference manual [HTML version]"
+	@echo "  - apidoc:      build ML API documentation"
+	@echo "  - release:     build Coq in release mode"
+	@echo ""
 	@echo "  - ocheck:  build for all supported OCaml versions [requires OPAM]"
 	@echo "  - ireport: build with optimized flambda settings and emit an inline report"
 	@echo "  - clean:   remove build directory and autogenerated files"
@@ -55,12 +63,15 @@ quickopt: voboot
 test-suite: voboot
 	dune runtest $(DUNEOPT)
 
-release: voboot
-	dune build $(DUNEOPT) -p coq
+refman-html: voboot
+	dune build @refman-html
 
 apidoc: voboot
 	dune build $(DUNEOPT) @doc
 
+release: voboot
+	dune build $(DUNEOPT) -p coq
+
 ocheck: voboot
 	dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all
 

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,39 @@
+synopsis: "The Coq Proof Assistant --- Reference Manual"
+description: """
+Coq is a formal proof management system. It provides
+a formal language to write mathematical definitions, executable
+algorithms and theorems together with an environment for
+semi-interactive development of machine-checked proofs.
+
+This package provides the Coq Reference Manual.
+"""
+opam-version: "2.0"
+maintainer: "The Coq development team <[email protected]>"
+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: "Open Publication License"
+
+depends: [
+  "dune"      { build }
+  "coq"       { build }
+]
+
+build-env: [
+  [ COQ_CONFIGURE_PREFIX = "%{prefix}" ]
+]
+
+build: [
+  [ "dune" "build" "@refman" "-j" jobs ]
+]
+
+# Would be better to have a *-conf package?
+depexts: [
+  [ "sphinx" ]
+  [ "sphinx_rtd_theme" ]
+  [ "beautifulsoup4" ]
+  [ "antlr4-python3-runtime"]
+  [ "pexpect" ]
+  [ "sphinxcontrib-bibtex" ]
+]

dev/ci/docker/bionic_coq/Dockerfile

@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-11-08-V1"
+# CACHEKEY: "bionic_coq-V2018-12-05-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -37,7 +37,7 @@ ENV COMPILER="4.05.0"
 # Common OPAM packages.
 # `num` does not have a version number as the right version to install varies
 # with the compiler version.
-ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.4.0 ounit.2.0.8 odoc.1.3.0" \
+ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.1 ounit.2.0.8 odoc.1.3.0" \
     CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.

dev/doc/build-system.dune.md

@@ -10,9 +10,9 @@ Coq can now be built using [Dune](https://github.com/ocaml/dune).
 
 ## Quick Start
 
-Dune >= 1.5.0 is recommended, see `dune-project` for the minimum
-required version; type `dune build` to build the base Coq
-libraries. No call to `./configure` is needed.
+Usually, using the latest version of Dune is recommended, see
+`dune-project` for the minimum required version; type `dune build` to
+build the base Coq libraries. No call to `./configure` is needed.
 
 Dune will get confused if it finds leftovers of in-tree compilation,
 so please be sure your tree is clean from objects files generated by
@@ -63,11 +63,16 @@ ml files in quick mode.
 Dune also provides targets for documentation, testing, and release
 builds, please see below.
 
-## Documentation and test targets
+## Documentation and testing targets
 
 Coq's test-suite can be run with `dune runtest`.
 
-The documentation target is not implemented in Dune yet.
+There is preliminary support to build the API documentation and
+reference manual in HTML format, use `dune build {@doc,@refman-html}`
+to generate them.
+
+So far these targets will build the documentation artifacts, however
+no install rules are generated yet.
 
 ## Developer shell
 

doc/dune

@@ -0,0 +1,24 @@
+(rule
+ (targets sphinx_build)
+ (deps
+  ; We could use finer dependencies here so the build is faster:
+  ;
+  ; - vo files: generated by sphinx after parsing the doc, promoted,
+  ; - Static files:
+  ;   + %{bin:coqdoc} etc...
+  ;   + config/coq_config.py
+  ;   + tools/coqdoc/coqdoc.css
+  (package coq)
+  (source_tree sphinx)
+  (source_tree tools))
+ (action (run sphinx-build -j4 -b html -d sphinx_build/doctrees sphinx sphinx_build/html)))
+
+(alias
+ (name refman-html)
+ (deps sphinx_build))
+
+; The install target still needs more work.
+; (install
+;  (section doc)
+;  (package coq-refman)
+;  (files sphinx_build))

doc/sphinx/dune

@@ -0,0 +1 @@
+(dirs :standard _static)

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", ""), "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-project

@@ -1,3 +1,2 @@
-(lang dune 1.4)
-
+(lang dune 1.6)
 (name coq)