Integration of a sphinx-based documentation generator.

The original contribution is from Clément Pit-Claudel. I updated
his code and integrated it with the Coq build system. Many improvements
by Paul Steckler (MIT).

This commit adds the infrastructure but no content.

8 files changed, 656 insertions, 0 deletions

diff --git a/doc/sphinx/_static/UbuntuMono-Square.ttf b/doc/sphinx/_static/UbuntuMono-Square.ttf
new file mode 100644
index 000000000..12b7c6d51
--- /dev/null
+++ b/doc/sphinx/_static/UbuntuMono-Square.ttf
diff --git a/doc/sphinx/_static/ansi-dark.css b/doc/sphinx/_static/ansi-dark.css
new file mode 100644
index 000000000..a564fd70b
--- /dev/null
+++ b/doc/sphinx/_static/ansi-dark.css
@@ -0,0 +1,144 @@
+/************************************************************************/
+/*         *   The Coq Proof Assistant / The Coq Development Team       */
+/*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       */
+/* <O___,, *       (see CREDITS file for the list of authors)           */
+/*   \VV/  **************************************************************/
+/*    //   *    This file is distributed under the terms of the         */
+/*         *     GNU Lesser General Public License Version 2.1          */
+/*         *     (see LICENSE file for the text of the license)         */
+/************************************************************************/
+.ansi-bold {
+    font-weight: bold;
+}
+
+.ansi-italic {
+    font-style: italic;
+}
+
+.ansi-negative {
+    filter: invert(100%);
+}
+
+.ansi-underline {
+    text-decoration: underline;
+}
+
+.ansi-no-bold {
+    font-weight: normal;
+}
+
+.ansi-no-italic {
+    font-style: normal;
+}
+
+.ansi-no-negative {
+    filter: invert(0%);
+}
+
+.ansi-no-underline {
+    text-decoration: none;
+}
+
+.ansi-black {
+    color: #000000;
+}
+
+.ansi-fg-red {
+    color: #b21717;
+}
+
+.ansi-fg-green {
+    color: #17b217;
+}
+
+.ansi-fg-yellow {
+    color: #b26717;
+}
+
+.ansi-fg-blue {
+    color: #1717b2;
+}
+
+.ansi-fg-magenta {
+    color: #b217b2;
+}
+
+.ansi-fg-cyan {
+    color: #17b2b2;
+}
+
+.ansi-fg-white {
+    color: #b2b2b2;
+}
+
+.ansi-fg-default {
+    color: #404040;
+}
+
+.ansi-fg-light-black {
+    color: #686868;
+}
+
+.ansi-fg-light-red {
+    color: #ff5454;
+}
+
+.ansi-fg-light-green {
+    color: #54ff54;
+}
+
+.ansi-fg-light-yellow {
+    color: #ffff54;
+}
+
+.ansi-fg-light-blue {
+    color: #5454ff;
+}
+
+.ansi-fg-light-magenta {
+    color: #ff54ff;
+}
+
+.ansi-fg-light-cyan {
+    color: #54ffff;
+}
+
+.ansi-fg-light-white {
+    color: #ffffff;
+}
+
+.ansi-bg-black {
+    background-color: #000000;
+}
+
+.ansi-bg-red {
+    background-color: #b21717;
+}
+
+.ansi-bg-green {
+    background-color: #17b217;
+}
+
+.ansi-bg-yellow {
+    background-color: #b26717;
+}
+
+.ansi-bg-blue {
+    background-color: #1717b2;
+}
+
+.ansi-bg-magenta {
+    background-color: #b217b2;
+}
+
+.ansi-bg-cyan {
+    background-color: #17b2b2;
+}
+
+.ansi-bg-white {
+    background-color: #b2b2b2;
+}
+
+.ansi-bg-default {
+    background-color: transparent;
+}
diff --git a/doc/sphinx/_static/ansi.css b/doc/sphinx/_static/ansi.css
new file mode 100644
index 000000000..26bd79770
--- /dev/null
+++ b/doc/sphinx/_static/ansi.css
@@ -0,0 +1,145 @@
+/************************************************************************/
+/*         *   The Coq Proof Assistant / The Coq Development Team       */
+/*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       */
+/* <O___,, *       (see CREDITS file for the list of authors)           */
+/*   \VV/  **************************************************************/
+/*    //   *    This file is distributed under the terms of the         */
+/*         *     GNU Lesser General Public License Version 2.1          */
+/*         *     (see LICENSE file for the text of the license)         */
+/************************************************************************/
+.ansi-bold {
+    font-weight: bold;
+}
+
+.ansi-italic {
+    font-style: italic;
+}
+
+.ansi-negative {
+    filter: invert(100%);
+}
+
+.ansi-underline {
+    text-decoration: underline;
+}
+
+.ansi-no-bold {
+    font-weight: normal;
+}
+
+.ansi-no-italic {
+    font-style: normal;
+}
+
+.ansi-no-negative {
+    filter: invert(0%);
+}
+
+.ansi-no-underline {
+    text-decoration: none;
+}
+
+
+.ansi-fg-black {
+    color: #babdb6;
+}
+
+.ansi-fg-red {
+    color: #a40000;
+}
+
+.ansi-fg-green {
+    color: #4e9a06;
+}
+
+.ansi-fg-yellow {
+    color: #ce5c00;
+}
+
+.ansi-fg-blue {
+    color: #204a87;
+}
+
+.ansi-fg-magenta {
+    color: #5c3566;
+}
+
+.ansi-fg-cyan {
+    color: #8f5902;
+}
+
+.ansi-fg-white {
+    color: #2e3436;
+}
+
+.ansi-fg-light-black {
+    color: #d3d7cf;
+}
+
+.ansi-fg-light-red {
+    color: #cc0000;
+}
+
+.ansi-fg-light-green {
+    color: #346604;             /* From tango.el */
+}
+
+.ansi-fg-light-yellow {
+    color: #f57900;
+}
+
+.ansi-fg-light-blue {
+    color: #3465a4;
+}
+
+.ansi-fg-light-magenta {
+    color: #75507b;
+}
+
+.ansi-fg-light-cyan {
+    color: #c14d11;
+}
+
+.ansi-fg-light-white {
+    color: #555753;
+}
+
+.ansi-fg-default {
+    color: #eeeeec;
+}
+
+.ansi-bg-black {
+    background-color: #babdb6;
+}
+
+.ansi-bg-red {
+    background-color: #a40000;
+}
+
+.ansi-bg-green {
+    background-color: #4e9a06;
+}
+
+.ansi-bg-yellow {
+    background-color: #ce5c00;
+}
+
+.ansi-bg-blue {
+    background-color: #204a87;
+}
+
+.ansi-bg-magenta {
+    background-color: #5c3566;
+}
+
+.ansi-bg-cyan {
+    background-color: #8f5902;
+}
+
+.ansi-bg-white {
+    background-color: #2e3436;
+}
+
+.ansi-bg-default {
+    background-color: transparent;
+}
diff --git a/doc/sphinx/_static/coqdoc.css b/doc/sphinx/_static/coqdoc.css
new file mode 100644
index 000000000..bbcc044a2
--- /dev/null
+++ b/doc/sphinx/_static/coqdoc.css
@@ -0,0 +1,68 @@
+/************************************************************************/
+/*         *   The Coq Proof Assistant / The Coq Development Team       */
+/*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       */
+/* <O___,, *       (see CREDITS file for the list of authors)           */
+/*   \VV/  **************************************************************/
+/*    //   *    This file is distributed under the terms of the         */
+/*         *     GNU Lesser General Public License Version 2.1          */
+/*         *     (see LICENSE file for the text of the license)         */
+/************************************************************************/
+/* Taken from CoqDoc's default stylesheet */
+
+.coqdoc-constructor {
+    color: rgb(60%,0%,0%);
+}
+
+.coqdoc-var {
+    color: rgb(40%,0%,40%);
+}
+
+.coqdoc-variable {
+    color: rgb(40%,0%,40%);
+}
+
+.coqdoc-definition {
+    color: rgb(0%,40%,0%);
+}
+
+.coqdoc-abbreviation {
+    color: rgb(0%,40%,0%);
+}
+
+.coqdoc-lemma {
+    color: rgb(0%,40%,0%);
+}
+
+.coqdoc-instance {
+    color: rgb(0%,40%,0%);
+}
+
+.coqdoc-projection {
+    color: rgb(0%,40%,0%);
+}
+
+.coqdoc-method {
+    color: rgb(0%,40%,0%);
+}
+
+.coqdoc-inductive {
+    color: rgb(0%,0%,80%);
+}
+
+.coqdoc-record {
+    color: rgb(0%,0%,80%);
+}
+
+.coqdoc-class {
+    color: rgb(0%,0%,80%);
+}
+
+.coqdoc-keyword {
+    color : #cf1d1d;
+}
+
+/* Custom additions */
+
+.coqdoc-tactic {
+    font-weight: bold;
+}
diff --git a/doc/sphinx/_static/coqnotations.sty b/doc/sphinx/_static/coqnotations.sty
new file mode 100644
index 000000000..75eac1f72
--- /dev/null
+++ b/doc/sphinx/_static/coqnotations.sty
@@ -0,0 +1,50 @@
+% The LaTeX generator wraps all custom spans in \DUrole{class}{contents}.  That
+% command then checks for another command called \DUroleclass.
+
+% Most of our CSS class names have dashes, so we need ‘\csname … \endcsname’
+
+% <magic>
+% \def\newcssclass#1#2{\expandafter\def\csname DUrole#1\endcsname ##1{#2}}
+% </magic>
+
+\RequirePackage{adjustbox}
+\RequirePackage{xcolor}
+\RequirePackage{amsmath}
+
+\definecolor{nbordercolor}{HTML}{AAAAAA}
+\definecolor{nbgcolor}{HTML}{EAEAEA}
+\definecolor{nholecolor}{HTML}{4E9A06}
+
+\newlength{\nscriptsize}
+\setlength{\nscriptsize}{0.8em}
+
+\newcommand*{\scriptsmallsquarebox}[1]{%
+  % Force width
+  \makebox[\nscriptsize]{%
+    % Force height and center vertically
+    \raisebox{\dimexpr .5\nscriptsize - .5\height \relax}[\nscriptsize][0pt]{%
+      % Cancel depth
+      \raisebox{\depth}{#1}}}}
+\newcommand*{\nscriptdecoratedbox}[2][]{\adjustbox{cfbox=nbordercolor 0.5pt 0pt,bgcolor=nbgcolor}{#2}}
+\newcommand*{\nscriptbox}[1]{\nscriptdecoratedbox{\scriptsmallsquarebox{\textbf{#1}}}}
+\newcommand*{\nscript}[2]{\text{\hspace{-.5\nscriptsize}\raisebox{-#1\nscriptsize}{\nscriptbox{\small#2}}}}
+\newcommand*{\nsup}[1]{^{\nscript{0.15}{#1}}}
+\newcommand*{\nsub}[1]{_{\nscript{0.35}{#1}}}
+\newcommand*{\nnotation}[1]{#1}
+\newcommand*{\nrepeat}[1]{\text{\adjustbox{cfbox=nbordercolor 0.5pt 2pt,bgcolor=nbgcolor}{#1\hspace{.5\nscriptsize}}}}
+\newcommand*{\nwrapper}[1]{\ensuremath{\displaystyle#1}} % https://tex.stackexchange.com/questions/310877/
+\newcommand*{\nhole}[1]{\textit{\color{nholecolor}#1}}
+
+% <magic>
+% Make it easier to define new commands matching CSS classes
+\newcommand{\newcssclass}[2]{%
+  \expandafter\def\csname DUrole#1\endcsname##1{#2}
+}
+% </magic>
+
+\newcssclass{notation-sup}{\nsup{#1}}
+\newcssclass{notation-sub}{\nsub{#1}}
+\newcssclass{notation}{\nnotation{#1}}
+\newcssclass{repeat}{\nrepeat{#1}}
+\newcssclass{repeat-wrapper}{\nwrapper{#1}}
+\newcssclass{hole}{\nhole{#1}}
diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css
new file mode 100644
index 000000000..1ae7a7cd7
--- /dev/null
+++ b/doc/sphinx/_static/notations.css
@@ -0,0 +1,177 @@
+/************************************************************************/
+/*         *   The Coq Proof Assistant / The Coq Development Team       */
+/*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       */
+/* <O___,, *       (see CREDITS file for the list of authors)           */
+/*   \VV/  **************************************************************/
+/*    //   *    This file is distributed under the terms of the         */
+/*         *     GNU Lesser General Public License Version 2.1          */
+/*         *     (see LICENSE file for the text of the license)         */
+/************************************************************************/
+.notation {
+    /* font-family: "Ubuntu Mono", "Consolas", monospace; */
+    white-space: pre-wrap;
+}
+
+.notation .notation-sup {
+    top: -0.4em;
+}
+
+.notation .notation-sub {
+    bottom: -0.4em;
+    border-radius: 1rem;
+}
+
+@font-face { /* This font has been edited to center all characters */
+  font-family: 'UbuntuMono-Square';
+  font-style: normal;
+  font-weight: 800;
+  src: local('UbuntuMono-Square'), url(./UbuntuMono-Square.ttf) format('truetype');
+}
+
+.notation .notation-sup, .notation .notation-sub {
+    background: #EAEAEA;
+    border: 1px solid #AAA;
+    color: black;
+    /* cursor: help; */
+    display: inline-block;
+    font-size: 0.5em;
+    font-weight: bolder;
+    font-family: UbuntuMono-Square, monospace;
+    height: 2em;
+    line-height: 1.6em;
+    position: absolute;
+    right: -1em; /* half of the width */
+    text-align: center;
+    width: 2em;
+}
+
+.notation .repeat {
+    background: #EAEAEA;
+    border: 1px solid #AAA;
+    display: inline-block;
+    padding-right: 0.6em; /* Space for the left half of the sub- and sup-scripts */
+    padding-left: 0.2em;
+    margin: 0.25em 0;
+}
+
+.notation .repeat-wrapper {
+    display: inline-block;
+    position: relative;
+    margin-right: 0.4em; /* Space for the right half of the sub- and sup-scripts */
+}
+
+.notation .hole {
+    color: #4e9a06;
+    font-style: italic;
+}
+
+/***********************/
+/* Small extra classes */
+/***********************/
+
+.math-preamble {
+    display: none;
+}
+
+.inline-grammar-production {
+    font-weight: bold;
+}
+
+/************************/
+/* Coqtop IO and Coqdoc */
+/************************/
+
+.coqtop dd, .ansi-bg-default {
+    background: #eeeeee !important;
+}
+
+.coqtop dd, .ansi-fg-default {
+    color: #2e3436 !important;
+}
+
+.coqtop dt {                    /* Questions */
+    background: none !important;
+    color: #333 !important;
+    font-weight: normal !important;
+    padding: 0 !important;
+    margin: 0 !important;
+}
+
+.coqtop dd {                    /* Responses */
+    padding: 0.5em;
+    margin-left: 0 !important;
+    margin-top: 0.5em !important;
+}
+
+.coqdoc, .coqtop dl {
+    margin: 12px; /* Copied from RTD theme */
+}
+
+.coqdoc {
+    display: block;
+    white-space: pre;
+}
+
+.coqtop dt, .coqtop dd {
+    border: none !important;
+    display: block !important;
+}
+
+.coqtop.coqtop-hidden, dd.coqtop-hidden, dt.coqtop-hidden { /* Overqualifying for precedence */
+    display: none !important;
+}
+
+/* FIXME: Specific to the RTD theme */
+.coqdoc, .coqtop dt, .coqtop dd, pre { /* pre added because of production lists */
+    font-family: Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace !important; /* Copied from RTD theme */
+    font-size: 12px !important; /* Copied from RTD theme */
+    line-height: 1.5 !important; /* Copied from RTD theme */
+    white-space: pre;
+}
+
+/*************/
+/* Overrides */
+/*************/
+
+.rst-content table.docutils td, .rst-content table.docutils th {
+    padding: 8px; /* Reduce horizontal padding */
+    border-left: none;
+    border-right: none;
+}
+
+/* We can't display nested blocks otherwise */
+code, .rst-content tt, .rst-content code {
+    background: transparent !important;
+    border: none !important;
+    font-size: inherit !important;
+}
+
+code {
+    padding: 0 !important;      /* This padding doesn't make sense without a border */
+}
+
+dt > .property {
+    margin-right: 0.25em;
+}
+
+.icon-home:visited {
+  color: #FFFFFF;
+}
+
+/* FIXME: Specific to the RTD theme */
+a:visited {
+    color: #2980B9;
+}
+
+/* Pygments for Coq is confused by ‘…’ */
+code span.error {
+    background: inherit !important;
+    line-height: inherit !important;
+    margin-bottom: 0 !important;
+    padding: 0 !important;
+}
+
+/* Red is too aggressive */
+.rst-content tt.literal, .rst-content tt.literal, .rst-content code.literal {
+    color: inherit !important;
+}
diff --git a/doc/sphinx/_static/notations.js b/doc/sphinx/_static/notations.js
new file mode 100644
index 000000000..eb7f211e8
--- /dev/null
+++ b/doc/sphinx/_static/notations.js
@@ -0,0 +1,43 @@
+/************************************************************************/
+/*         *   The Coq Proof Assistant / The Coq Development Team       */
+/*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       */
+/* <O___,, *       (see CREDITS file for the list of authors)           */
+/*   \VV/  **************************************************************/
+/*    //   *    This file is distributed under the terms of the         */
+/*         *     GNU Lesser General Public License Version 2.1          */
+/*         *     (see LICENSE file for the text of the license)         */
+/************************************************************************/
+function annotateSup(marker) {
+    switch (marker) {
+    case "?":
+        return "This block is optional.";
+    case "*":
+        return "This block is optional, and may be repeated.";
+    case "+":
+        return "This block may be repeated.";
+    }
+}
+
+function annotateSub(separator) {
+    return "Use “" + separator + "” to separate repetitions of this block.";
+}
+
+// function translatePunctuation(original) {
+//     var mappings = { ",": "⸴" }; // ，
+//     return mappings[original] || original;
+// }
+
+function annotateNotations () {
+    $(".repeat-wrapper > sup")
+        .attr("data-hint", function() {
+            return annotateSup($(this).text());
+        }).addClass("hint--top hint--rounded");
+
+    $(".repeat-wrapper > sub")
+        .attr("data-hint", function() {
+            return annotateSub($(this).text());
+        }).addClass("hint--bottom hint--rounded");
+    //.text(function(i, text) { return translatePunctuation(text); });
+}
+
+$(annotateNotations);
diff --git a/doc/sphinx/_static/pre-text.css b/doc/sphinx/_static/pre-text.css
new file mode 100644
index 000000000..38d81abef
--- /dev/null
+++ b/doc/sphinx/_static/pre-text.css
@@ -0,0 +1,29 @@
+/************************************************************************/
+/*         *   The Coq Proof Assistant / The Coq Development Team       */
+/*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       */
+/* <O___,, *       (see CREDITS file for the list of authors)           */
+/*   \VV/  **************************************************************/
+/*    //   *    This file is distributed under the terms of the         */
+/*         *     GNU Lesser General Public License Version 2.1          */
+/*         *     (see LICENSE file for the text of the license)         */
+/************************************************************************/
+/* Formatting for PRE (literal) text in .rst files */
+
+.line-block {
+    background-color: rgb(80%,90%,80%);
+    margin: 0px;
+    margin-top: 0px;
+    margin-right: 16px;
+    margin-bottom: 20px;
+    padding-left: 4px;
+    padding-top: 4px;
+    padding-bottom: 4px;
+}
+
+.line-block cite {
+    font-size: 90%;
+}
+
+.pre {
+    font-size: 90%;
+}