From cb16f994e14073ab5731beeffc05ea114001d8e1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 2 Oct 2018 21:38:55 +0200
Subject: [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.
---
 dev/README.md                  |   5 +-
 dev/ci/README.md               |   5 +-
 dev/ocamldoc/docintro          |  49 ---------
 dev/ocamldoc/fix-ocamldoc-utf8 |   6 --
 dev/ocamldoc/header.tex        |  14 ---
 dev/ocamldoc/html/style.css    | 220 -----------------------------------------
 6 files changed, 3 insertions(+), 296 deletions(-)
 delete mode 100644 dev/ocamldoc/docintro
 delete mode 100755 dev/ocamldoc/fix-ocamldoc-utf8
 delete mode 100644 dev/ocamldoc/header.tex
 delete mode 100644 dev/ocamldoc/html/style.css

(limited to 'dev')

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;
-}
-- 
cgit v1.2.3