[doc] Build ML API documentation artifact.

This is not optimal for we have to rebuild the `.cmi` as
`ocamldoc` cannot yet use the `_install_ci/` directory.

Overall the `mli` documentation is in a sorry state, however, I think
this is a first step in order to improve it.

Note that the `ml-doc` target seems broken in OCaml 4.07.0, needs
investigation.

cc: #7155

5 files changed, 56 insertions, 19 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index f42d13e4c1..3e08aa58bb 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -93,7 +93,7 @@ after_script:
 # purpose, we add a spurious dependency `not-a-real-job` that must be
 # overridden otherwise the CI will fail.
 
-.doc-templare: &doc-template
+.doc-template: &doc-template
   stage: test
   dependencies:
     - not-a-real-job
@@ -245,11 +245,23 @@ pkg:nix:
     paths:
       - nix-build-coq.drv-0/*/test-suite/logs
 
-documentation:
+doc:refman:
   <<: *doc-template
   dependencies:
     - build:base
 
+doc:ml-api:
+  stage: test
+  dependencies:
+    - build:edge
+  script:
+    - ./configure -warn-error yes -prefix "$(pwd)/_install_ci"
+    - make mli-doc source-doc # ml-doc [broken in 4.07.0]
+  artifacts:
+    name: "$CI_JOB_NAME"
+    paths:
+      - dev/ocamldoc
+
 test-suite:base:
   <<: *test-suite-template
   dependencies:
diff --git a/Makefile.doc b/Makefile.doc
index 1b1198c1f2..0dcf9daf27 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -218,9 +218,11 @@ ODOCDOTOPTS=-dot -dot-reduce
 
 source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf
 
+OCAMLDOC_CAML_FLAGS=-rectypes -I +threads $(MLINCLUDES)
+
 $(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi)
 	$(SHOW)'OCAMLDOC -latex -o $@'
-	$(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP5LIB) $(MLINCLUDES)\
+	$(HIDE)$(OCAMLFIND) ocamldoc -latex $(OCAMLDOC_CAML_FLAGS) \
 	$(DOCMLIS) -noheader -t "Coq mlis documentation" \
 	-intro $(OCAMLDOCDIR)/docintro -o $@.tmp
 	$(SHOW)'OCAMLDOC utf8 fix'
@@ -230,31 +232,31 @@ $(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi)
 
 mli-doc: $(DOCMLIS:.mli=.cmi)
 	$(SHOW)'OCAMLDOC -html'
-	$(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP5LIB) $(MLINCLUDES) \
+	$(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html $(OCAMLDOC_CAML_FLAGS) \
 	$(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \
 	-t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
 	-css-style style.css
 
 ml-dot: $(MLFILES)
-	$(OCAMLFIND) ocamldoc -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP5LIB) $(MLINCLUDES) \
+	$(OCAMLFIND) ocamldoc -dot -dot-reduce $(OCAMLDOC_CAML_FLAGS) \
 	$(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot
 
 %_dep.png: %.dot
 	$(DOT) -Tpng $< -o $@
 
 %_types.dot: %.mli
-	$(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $<
+	$(OCAMLFIND) ocamldoc $(OCAMLDOC_CAML_FLAGS) $(ODOCDOTOPTS) -dot-types -o $@ $<
 
-OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
+OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc $(OCAMLDOC_CAML_FLAGS) $(ODOCDOTOPTS) -o $@ \
   $(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib))))
 
 %.dot: | %.mllib.d
 	$(OCAMLDOC_MLLIBD)
 
-ml-doc:
+ml-doc: kernel/copcodes.cmi
 	$(SHOW)'OCAMLDOC -html'
 	$(HIDE)mkdir -p $(OCAMLDOCDIR)/html/implementation
-	$(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) \
+	$(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html $(OCAMLDOC_CAML_FLAGS) \
 	$(DOCMLS) -d $(OCAMLDOCDIR)/html/implementation -colorize-code \
 	-t "Coq mls documentation" \
 	-css-style ../style.css
@@ -269,7 +271,7 @@ tactics/tactics.dot: | tactics/tactics.mllib.d ltac/ltac.mllib.d
 	$(OCAMLDOC_MLLIBD)
 
 %.dot: %.mli
-	$(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $<
+	$(OCAMLFIND) ocamldoc $(OCAMLDOC_CAML_FLAGS) $(ODOCDOTOPTS) -o $@ $<
 
 $(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex
 	$(SHOW)'PDFLATEX $*.tex'
diff --git a/clib/cList.mli b/clib/cList.mli
index ed468cb977..39d9a5e535 100644
--- a/clib/cList.mli
+++ b/clib/cList.mli
@@ -289,8 +289,8 @@ sig
 
   val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
   (** [share_tails l1 l2] returns [(l1',l2',l)] such that [l1] is
-      [l1'@l] and [l2] is [l2'@l] and [l] is maximal amongst all such
-      decompositions*)
+      [l1'\@l] and [l2] is [l2'\@l] and [l] is maximal amongst all such
+      decompositions *)
 
   (** {6 Association lists} *)
 
diff --git a/dev/ci/README.md b/dev/ci/README.md
index a814e4914e..b4ea6838bf 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -136,12 +136,35 @@ rebuilding Coq. In one job, Coq is built with `./configure -prefix _install_ci`
 and `make install` is run, then the `_install_ci` directory
 persists to and is used by the next jobs.
 
-Artifacts can also be downloaded from the GitLab repository.
-Currently, available artifacts are:
+### Artifacts
+
+Build artifacts from GitLab can be linked / downloaded in a systematic
+way, see [GitLab's documentation](https://docs.gitlab.com/ce/user/project/pipelines/job_artifacts.html#downloading-the-latest-job-artifacts)
+for more information. For example, to access the documentation of the
+`master` branch, you can do:
+
+https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman
+
+Browsing artifacts is also possible:
+https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base
+
+Above, you can replace `master` and `job` by the desired GitLab branch and job name.
+
+Currently available artifacts are:
+
 - the Coq executables and stdlib, in four copies varying in
-  architecture and OCaml version used to build Coq.
-- the Coq documentation, built in the `documentation` job. When submitting
-  a documentation PR, this can help reviewers checking the rendered result.
+  architecture and OCaml version used to build Coq:
+  https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base
+
+- the Coq documentation, built in the `doc:*` jobs. When submitting
+  a documentation PR, this can help reviewers checking the rendered result:
+
+  + Coq's Reference Manual [master branch]
+    https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman
+  + 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
 
 ### GitLab and Windows
 
@@ -168,6 +191,6 @@ but if you wish to save more time you can skip the job by setting
 
 This means you will need to change its value when the Docker image
 needs to be updated. You can do so for a single pipeline by starting
-it through the web interface..
+it through the web interface.
 
 See also [`docker/README.md`](docker/README.md).
diff --git a/doc/README.md b/doc/README.md
index 3e70bc443d..47507de52d 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -10,7 +10,7 @@ The documentation of the latest released version is available on the Coq
 web site at [coq.inria.fr/documentation](http://coq.inria.fr/documentation).
 
 Additionally, you can view the documentation for the current master version at
-<https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=documentation>.
+<https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman>.
 
 The reference manual is written is reStructuredText and compiled
 using Sphinx. See [`sphinx/README.rst`](sphinx/README.rst)