[doc] [api] Remove `ocamldoc` support in favor of `odoc`

This PR removes support for `ocamldoc` in favor of `odoc`.

Following a recent discussion in OCaml's discord, it turns out that
basically all the ecosystem has migrated to odoc, thus we follow suit
and may focus on `odoc` for Coq's ML API documentation.

10 files changed, 6 insertions, 405 deletions

diff --git a/.gitignore b/.gitignore
index 0ab6e25852..39ef20970d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -113,8 +113,6 @@ doc/stdlib/index-list.html
 doc/tutorial/Tutorial.v.out
 doc/RecTutorial/RecTutorial.html
 doc/RecTutorial/RecTutorial.ps
-dev/ocamldoc/*.html
-dev/ocamldoc/*.css
 
 # .mll files
 
@@ -160,13 +158,6 @@ checker/names.mli
 checker/esubst.ml
 checker/esubst.mli
 
-# mlis documentation
-
-dev/ocamldoc/html/
-dev/ocamldoc/coq.*
-dev/ocamldoc/ocamldoc.sty
-dev/myinclude
-
 # emacs save files
 *~
 \#*\#
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index dae412923b..34deeb3f18 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -275,18 +275,6 @@ doc:refman:
   dependencies:
     - build:base
 
-doc:ml-api:ocamldoc:
-  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
-
 doc:ml-api:odoc:
   stage: test
   dependencies:
diff --git a/Makefile b/Makefile
index 2e4f46272e..a15870faca 100644
--- a/Makefile
+++ b/Makefile
@@ -193,11 +193,11 @@ META.coq: META.coq.in
 # Cleaning
 ###########################################################################
 
-.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean devdocclean alienclean
+.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean alienclean
 
-clean: objclean cruftclean depclean docclean devdocclean camldevfilesclean
+clean: objclean cruftclean depclean docclean camldevfilesclean
 
-cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean devdocclean
+cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean
 
 objclean: archclean indepclean
 
@@ -276,12 +276,6 @@ timingclean:
 	  -o -name "time-of-build-before.log" -o -name "time-of-build-after.log" \
 	  -o -name "time-of-build-pretty.log" -o -name "time-of-build-both.log" \) -exec rm -f {} +
 
-devdocclean:
-	find . \( -name '*.dep.ps' -o -name '*.dot' \) -exec rm -f {} +
-	rm -f $(OCAMLDOCDIR)/*.log $(OCAMLDOCDIR)/*.aux $(OCAMLDOCDIR)/*.toc
-	rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex
-	rm -f $(OCAMLDOCDIR)/html/*.html
-
 # Ensure that every compiled file around has a known source file.
 # This should help preventing weird compilation failures caused by leftover
 # compiled files after deleting or moving some source files.
diff --git a/Makefile.doc b/Makefile.doc
index db52607612..1184cc186b 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -209,85 +209,6 @@ install-doc-sphinx:
 		$(INSTALLLIB) doc/sphinx/_build/$$f $(FULLDOCDIR)/sphinx/$$f;\
 	done)
 
-###########################################################################
-# Documentation of the source code (using ocamldoc)
-###########################################################################
-
-OCAMLDOCDIR=dev/ocamldoc
-
-DOCMLLIBS= $(CORECMA:.cma=_MLLIB_DEPENDENCIES) $(PLUGINSCMO:.cmo=_MLPACK_DEPENDENCIES)
-DOCMLS=$(foreach lib,$(DOCMLLIBS),$(addsuffix .ml, $($(lib))))
-
-DOCMLIS=$(wildcard $(addsuffix /*.mli, $(SRCDIRS)))
-
-# Defining options to generate dependencies graphs
-DOT=dot
-ODOCDOTOPTS=-dot -dot-reduce
-
-.PHONY: source-doc mli-doc ml-doc
-
-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 $(OCAMLDOC_CAML_FLAGS) \
-	$(DOCMLIS) -noheader -t "Coq mlis documentation" \
-	-intro $(OCAMLDOCDIR)/docintro -o $@.tmp
-	$(SHOW)'OCAMLDOC utf8 fix'
-	$(HIDE)$(OCAMLDOCDIR)/fix-ocamldoc-utf8 $@.tmp
-	$(HIDE)cat $(OCAMLDOCDIR)/header.tex $@.tmp > $@
-	rm $@.tmp
-
-mli-doc: $(DOCMLIS:.mli=.cmi)
-	$(SHOW)'OCAMLDOC -html'
-	$(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 $(OCAMLDOC_CAML_FLAGS) \
-	$(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot
-
-%_dep.png: %.dot
-	$(DOT) -Tpng $< -o $@
-
-%_types.dot: %.mli
-	$(OCAMLFIND) ocamldoc $(OCAMLDOC_CAML_FLAGS) $(ODOCDOTOPTS) -dot-types -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: kernel/copcodes.cmi
-	$(SHOW)'OCAMLDOC -html'
-	$(HIDE)mkdir -p $(OCAMLDOCDIR)/html/implementation
-	$(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
-
-parsing/parsing.dot : | parsing/parsing.mllib.d
-	$(OCAMLDOC_MLLIBD)
-
-grammar/grammar.dot : | grammar/grammar.mllib.d
-	$(OCAMLDOC_MLLIBD)
-
-tactics/tactics.dot: | tactics/tactics.mllib.d ltac/ltac.mllib.d
-	$(OCAMLDOC_MLLIBD)
-
-%.dot: %.mli
-	$(OCAMLFIND) ocamldoc $(OCAMLDOC_CAML_FLAGS) $(ODOCDOTOPTS) -o $@ $<
-
-$(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex
-	$(SHOW)'PDFLATEX $*.tex'
-	$(HIDE)(cd $(OCAMLDOCDIR) ; pdflatex -interaction=batchmode $*.tex && pdflatex -interaction=batchmode $*.tex)
-	$(HIDE)(cd doc/tools/; ./show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log)
-
 # For emacs:
 # Local Variables:
 # mode: makefile
diff --git a/dev/README.md b/dev/README.md
index 4642aaf06d..d9fdd230d3 100644
--- a/dev/README.md
+++ b/dev/README.md
@@ -34,9 +34,8 @@
 | [`dev/doc/release-process.md`](doc/release-process.md) | Process of creating a new Coq release |
 
 
-## Documentation of ML interfaces using ocamldoc ( `dev/ocamldoc/html`)
-`make mli-doc` in coq root directory.
-
+## Documentation of ML interfaces using `odoc` ( `_build/default/_doc`)
+`make -f Makefile.dune apidoc` in coq root directory.
 
 ## Other development tools (`dev/tools`)
 
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 3a179a9431..24952eb5b7 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -167,10 +167,7 @@ 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: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
+    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/ocamldoc/docintro b/dev/ocamldoc/docintro
deleted file mode 100644
index 33d20fc818..0000000000
--- a/dev/ocamldoc/docintro
+++ /dev/null
@@ -1,49 +0,0 @@
-{!indexlist}
-
-This is Coq, a proof assistant for the Calculus of Inductive Constructions.
-This document describes the implementation of Coq.
-It has been automatically generated from the source of
-Coq using {{:http://caml.inria.fr/}ocamldoc}.
-The source files are organized in several directories ordered like that:
-
-{ol {- Utility libraries : lib
-
-describes the various utility libraries used in the code
-of Coq.}
-{- Kernel : kernel
-
-describes the Coq kernel, which is a type checker for the Calculus
-of Inductive Constructions.}
-{- Library : library
-
-describes the Coq library, which is made of two parts:
-- a general mechanism to keep a trace of all operations and of
-    the state of the system, with backtrack capabilities;
-- a global environment for the CCI, with functions to export and 
-    import compiled modules.
-
-}
-{- Pretyping : pretyping
-
-}
-{- Front abstract syntax of terms : interp
-
-describes the translation from Coq context-dependent
-front abstract syntax of terms {v constr_expr v} to and from the
-context-free, untyped, globalized form of constructions {v glob_constr v}.}
-{- Parsers and printers : parsing
-
-describes the implementation of the Coq parsers and printers.}
-{- Proof engine : proofs
-
-describes the Coq proof engine, which is also called
-the ``refiner'', since it provides a way to build terms by successive
-refining steps. Those steps are either primitive rules or higher-level
-tactics.}
-{- Tacticts : tactics
-
-describes the Coq main tactics.}
-{- Toplevel : toplevel
-
-describes the highest modules of the Coq system.}
-}
diff --git a/dev/ocamldoc/fix-ocamldoc-utf8 b/dev/ocamldoc/fix-ocamldoc-utf8
deleted file mode 100755
index fe2e0c1155..0000000000
--- a/dev/ocamldoc/fix-ocamldoc-utf8
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/sh
-
-# This reverts automatic translation of latin1 accentuated letters by ocamldoc
-# Usage: fix-ocamldoc-utf8 file
-
-sed -i -e 's/\\`a/\d224/g' -e "s/\\\^a/\d226/g" -e "s/\\\'e/\d233/g" -e 's/\\`e/\d232/g' -e "s/\\\^e/\d234/g" -e 's/\\\"e/\d235/g' -e "s/\\\^o/\d244/g" -e 's/\\\"o/\d246/g' -e "s/\\\^i/\d238/g" -e 's/\\\"i/\d239/g' -e 's/\\`u/\d249/g' -e "s/\\\^u/\d251/g" -e "s/\\\c{c}/\d231/g" $1
diff --git a/dev/ocamldoc/header.tex b/dev/ocamldoc/header.tex
deleted file mode 100644
index 4091f8144f..0000000000
--- a/dev/ocamldoc/header.tex
+++ /dev/null
@@ -1,14 +0,0 @@
-\documentclass[11pt]{article} 
-\usepackage[utf8x]{inputenc} 
-\usepackage[T1]{fontenc} 
-\usepackage{textcomp}
-\usepackage{tipa}
-\usepackage{textgreek}
-\usepackage{fullpage} 
-\usepackage{url} 
-\usepackage{ocamldoc}
-\title{Coq mlis documentation}
-\begin{document}
-\maketitle
-\tableofcontents
-\vspace{0.2cm}
diff --git a/dev/ocamldoc/html/style.css b/dev/ocamldoc/html/style.css
deleted file mode 100644
index c2c45b6297..0000000000
--- a/dev/ocamldoc/html/style.css
+++ /dev/null
@@ -1,220 +0,0 @@
-a:visited {

-  color: #416DFF; text-decoration: none; 

-}

-

-a:link {

-  color: #416DFF; text-decoration: none;

-}

-

-a:hover {

-  color: Red; text-decoration: none; background-color: #5FFF88

-}

-

-a:active {

-  color: Red; text-decoration: underline; 

-}

-

-.keyword {

-  font-weight: bold; color: Red 

-}

-

-.keywordsign {

-  color: #C04600 

-}

-

-.superscript {

-  font-size: 8 

-}

-

-.subscript {

-  font-size: 8 

-}

-

-.comment {

-  color: Green 

-}

-

-.constructor {

-  color: Blue 

-}

-

-.type {

-  color: #5C6585 

-}

-

-.string {

-  color: Maroon 

-}

-

-.warning {

-  color: Red; font-weight: bold 

-}

-

-.info {

-  margin-left: 3em; margin-right: 3em 

-}

-

-.param_info {

-  margin-top: 4px; margin-left: 3em; margin-right: 3em 

-}

-

-.code {

-  color: #465F91; 

-}

-

-h1 {

-  font-size: 20pt; text-align: center; 

-}

-

-h5, h6, div.h7, div.h8, div.h9 {

-  font-size: 20pt;

-  border: 1px solid #000000;

-  margin-top: 5px;

-  margin-bottom: 2px;

-  text-align: center;

-  padding: 2px;

-}

-

-h5 {

-  background-color: #90FDFF;

-}

-

-h6 {

-  background-color: #016699;

-  color: white;

-}

-

-div.h7 {

-  background-color: #E0FFFF;

-}

-

-div.h8 {

-  background-color: #F0FFFF;

-}

-

-div.h9 {

-  background-color: #FFFFFF;

-}

-

-.typetable, .indextable, .paramstable {

-  border-style: hidden;

-}

-

-.paramstable {

-  padding: 5pt 5pt;

-}

-

-body {

-  background-color: white;

-}

-

-tr {

-  background-color: white;

-}

-

-td.typefieldcomment {

-  background-color: #FFFFFF;

-  font-size: smaller;

-}

-

-pre {

-  margin-bottom: 4px;

-}

-

-div.sig_block {

-  margin-left: 2em;

-}

-

-

-h2 {

-  font-family: Arial, Helvetica, sans-serif;

-  font-size: 16pt;

-  font-weight: normal;

-  border-bottom: 1px solid #dadada;

-  border-top: 1px solid #dadada;

-  color: #101010;

-  background: #eeeeff;

-  margin: 25px 0px 10px 0px;

-  padding: 1px 1px 1px 1px;

-}

-

-h3 {

-  font-family: Arial, Helvetica, sans-serif;

-  font-size: 12pt;

-  color: #016699;

-  font-weight: bold;

-  padding: 15px 0 0 0ex;

-  margin: 5px 0 0 0;

-}

-

-h4 {

-  font-family: Arial, Helvetica, sans-serif;

-  font-size: 10pt;

-  color: #016699;

-  padding: 15px 0 0 0ex;

-  margin: 5px 0 0 0;

-}

-

-/* Here starts the overwrite of default rules to give a better look */

-

-body {

-  font-family: Calibri, Georgia, Garamond, Baskerville, serif;

-  font-size: 12pt;

-  background-color: white;

-}

-

-a:link, a {

-  color: #6895c3 !important;

-}

-

-a:hover {

-  color: #2F4459 !important;

-  background-color: white;

-}

-

-hr {

-  height: 1px;

-  color: #016699;

-  background-color: #016699;

-  border-width: 0;

-}

-

-h1, h1 a:link, h1 a:visited, h1 a {

-  font-family: Cambria, Georgia, Garamond, Baskerville, serif;

-  color: #016699;

-}

-

-.navbar {

-  float: left;

-}

-

-.navbar a, .navbar a:link, .navbar a:visited {

-  color: #016699;

-  font-family: Arial, Helvetica, sans-serif;

-  font-weight: bold;

-  font-size: 80%;

-}

-

-.keyword {

-  color: #c13939;

-}

-

-.constructor {

-  color: #3c8f7e;

-}

-

-pre, code {

-  font-family: "DejaVu Sans Mono", "Bitstream Vera Mono", "Courrier New", monospace;

-  white-space: normal;

-  font-size: 9pt;

-  font-weight: bold;

-}

-

-.type br {

-  display: none;

-}

-

-.info {

-  margin-left: 1em;

-  font-size: 12pt;

-}