Merge PR #8053: [dune] Add apidoc target using `odoc`

8 files changed, 38 insertions, 14 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 693a0b6bf0..0115ac9eff 100644
--- a/.gitlab-ci.yml
+++ b/.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-08-27-V2"
+  CACHEKEY: "bionic_coq-V2018-09-05-V1"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
@@ -275,7 +275,7 @@ doc:refman:
   dependencies:
     - build:base
 
-doc:ml-api:
+doc:ml-api:ocamldoc:
   stage: test
   dependencies:
     - build:edge
@@ -287,6 +287,19 @@ doc:ml-api:
     paths:
       - dev/ocamldoc
 
+doc:ml-api:odoc:
+  <<: *dune-template
+  stage: test
+  dependencies:
+    - build:egde:dune:dev
+  variables:
+    OPAM_SWITCH: edge
+    DUNE_TARGET: apidoc
+  artifacts:
+    name: "$CI_JOB_NAME"
+    paths:
+      - _build/default/_doc/
+
 test-suite:base:
   <<: *test-suite-template
   dependencies:
diff --git a/Makefile.dune b/Makefile.dune
index f90f555557..e04982650f 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -13,6 +13,7 @@ help:
 	@echo "  - states:  build a minimal functional coqtop"
 	@echo "  - world:   build all binaries and libraries"
 	@echo "  - release: build Coq in release mode"
+	@echo "  - apidoc:  build ML API documentation"
 	@echo "  - clean:   remove build directory and autogenerated files"
 	@echo "  - help:    show this message"
 
@@ -29,6 +30,12 @@ world: 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
+	dune build $(DUNEOPT) @doc
+	mv checker/dune.disabled checker/dune || true
+
 clean:
 	dune clean
 
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 95892ebe0a..3a179a9431 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -157,7 +157,7 @@ Currently available artifacts are:
   https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base
 
   Additionally, an experimental Dune build is provided:
-  https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_build/?job=build:edge:dune
+  https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_build/?job=build:edge:dune:dev
 
 - the Coq documentation, built in the `doc:*` jobs. When submitting
   a documentation PR, this can help reviewers checking the rendered result:
@@ -167,7 +167,10 @@ Currently available artifacts are:
   + Coq's Standard Library Documentation [master branch]
     https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=doc:refman
   + Coq's ML API Documentation [master branch]
-    https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/dev/ocamldoc/html/index.html?job=doc:ml-api
+    https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/dev/ocamldoc/html/index.html?job=doc:ml-api:ocamldoc
+
+  The dune job also provides its own API documentation using the newer `odoc` tool:
+  https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_build/default/_doc/_html/index.html?job=doc:ml-api:odoc
 
 ### GitLab and Windows
 
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 7a649591dd..8b26294d8f 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-08-27-V2"
+# CACHEKEY: "bionic_coq-V2018-09-05-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -45,12 +45,13 @@ RUN opam switch -y -j $NJOBS "${COMPILER}+32bit" && eval $(opam config env) && \
 # EDGE switch
 ENV COMPILER_EDGE="4.07.0" \
     CAMLP5_VER_EDGE="7.06" \
-    COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2"
+    COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \
+    BASE_OPAM_EDGE="odoc.1.2.0 dune-release.0.3.0"
 
 RUN opam switch -y -j $NJOBS $COMPILER_EDGE && eval $(opam config env) && \
-    opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE
+    opam install -j $NJOBS $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
 # `ci-template-flambda` with everything.
 RUN opam switch -y -j $NJOBS "${COMPILER_EDGE}+flambda" && eval $(opam config env) && \
-    opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE $CI_OPAM
+    opam install -j $NJOBS $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE $CI_OPAM
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 9cc044316b..ea38dabd5c 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -285,8 +285,8 @@ val destMeta : constr -> metavariable
 (** Destructs a variable *)
 val destVar : constr -> Id.t
 
-(** Destructs a sort. [is_Prop] recognizes the sort {% \textsf{%}Prop{% }%}, whether
-   [isprop] recognizes both {% \textsf{%}Prop{% }%} and {% \textsf{%}Set{% }%}. *)
+(** Destructs a sort. [is_Prop] recognizes the sort [Prop], whether
+   [isprop] recognizes both [Prop] and [Set]. *)
 val destSort : constr -> Sorts.t
 
 (** Destructs a casted term *)
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 9c6ef64b50..3fd40a7f42 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -12,7 +12,7 @@ open Names
 open Constr
 open Environ
 
-(** Type errors. {% \label{%}typeerrors{% }%} *)
+(** Type errors. {% \label{typeerrors} %} *)
 
 (*i Rem: NotEnoughAbstractionInFixBody should only occur with "/i" Fix
     notation i*)
diff --git a/lib/genarg.mli b/lib/genarg.mli
index bb85f99e3c..52db3df088 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -13,7 +13,7 @@
 (** The route of a generic argument, from parsing to evaluation.
 In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc.
 
-{% \begin{%}verbatim{% }%}
+{% \begin{verbatim} %}
              parsing          in_raw                            out_raw
    char stream ---> raw_object ---> raw_object generic_argument -------+
                           encapsulation                          decaps|
@@ -36,7 +36,7 @@ In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc.
     |
     V
 effective use
-{% \end{%}verbatim{% }%}
+{% \end{verbatim} %}
 
 To distinguish between the uninterpreted, globalized and
 interpreted worlds, we annotate the type [generic_argument] by a
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index e6065dda87..bf38c30a1f 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -23,7 +23,7 @@ type reduction_tactic_error =
 
 exception ReductionTacticError of reduction_tactic_error
 
-(** {6 Reduction functions associated to tactics. {% \label{%}tacred{% }%} } *)
+(** {6 Reduction functions associated to tactics. } *)
 
 (** Evaluable global reference *)