From 4aaf28cc905bebf757b02ad911a6eed78714cac7 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 10 Feb 2017 15:52:24 +0100 Subject: Integration of a sphinx-based documentation generator. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- .travis.yml | 7 + INSTALL.doc | 10 + Makefile | 1 + Makefile.doc | 30 +- configure.ml | 11 +- default.nix | 11 +- doc/LICENSE | 12 +- doc/sphinx/MIGRATING | 238 ++++++ doc/sphinx/_static/UbuntuMono-Square.ttf | Bin 0 -> 38104 bytes doc/sphinx/_static/ansi-dark.css | 144 ++++ doc/sphinx/_static/ansi.css | 145 ++++ doc/sphinx/_static/coqdoc.css | 68 ++ doc/sphinx/_static/coqnotations.sty | 50 ++ doc/sphinx/_static/notations.css | 177 +++++ doc/sphinx/_static/notations.js | 43 ++ doc/sphinx/_static/pre-text.css | 29 + doc/sphinx/conf.py | 400 ++++++++++ doc/sphinx/coqdoc.css | 338 +++++++++ doc/sphinx/index.rst | 0 doc/tools/coqrst/__init__.py | 10 + doc/tools/coqrst/checkdeps.py | 39 + doc/tools/coqrst/coqdoc/__init__.py | 10 + doc/tools/coqrst/coqdoc/main.py | 86 +++ doc/tools/coqrst/coqdomain.py | 816 +++++++++++++++++++++ doc/tools/coqrst/notations/Makefile | 27 + doc/tools/coqrst/notations/TacticNotations.g | 30 + doc/tools/coqrst/notations/TacticNotations.tokens | 8 + doc/tools/coqrst/notations/TacticNotationsLexer.py | 60 ++ .../coqrst/notations/TacticNotationsLexer.tokens | 8 + .../coqrst/notations/TacticNotationsParser.py | 519 +++++++++++++ .../coqrst/notations/TacticNotationsVisitor.py | 53 ++ doc/tools/coqrst/notations/UbuntuMono-B.ttf | Bin 0 -> 191400 bytes doc/tools/coqrst/notations/UbuntuMono-Square.ttf | Bin 0 -> 38200 bytes doc/tools/coqrst/notations/__init__.py | 0 doc/tools/coqrst/notations/fontsupport.py | 81 ++ doc/tools/coqrst/notations/html.py | 65 ++ doc/tools/coqrst/notations/parsing.py | 37 + doc/tools/coqrst/notations/plain.py | 50 ++ doc/tools/coqrst/notations/regexp.py | 57 ++ doc/tools/coqrst/notations/sphinx.py | 77 ++ doc/tools/coqrst/repl/__init__.py | 0 doc/tools/coqrst/repl/ansicolors.py | 99 +++ doc/tools/coqrst/repl/coqtop.py | 98 +++ 43 files changed, 3930 insertions(+), 14 deletions(-) create mode 100644 doc/sphinx/MIGRATING create mode 100644 doc/sphinx/_static/UbuntuMono-Square.ttf create mode 100644 doc/sphinx/_static/ansi-dark.css create mode 100644 doc/sphinx/_static/ansi.css create mode 100644 doc/sphinx/_static/coqdoc.css create mode 100644 doc/sphinx/_static/coqnotations.sty create mode 100644 doc/sphinx/_static/notations.css create mode 100644 doc/sphinx/_static/notations.js create mode 100644 doc/sphinx/_static/pre-text.css create mode 100755 doc/sphinx/conf.py create mode 100644 doc/sphinx/coqdoc.css create mode 100644 doc/sphinx/index.rst create mode 100644 doc/tools/coqrst/__init__.py create mode 100644 doc/tools/coqrst/checkdeps.py create mode 100644 doc/tools/coqrst/coqdoc/__init__.py create mode 100644 doc/tools/coqrst/coqdoc/main.py create mode 100644 doc/tools/coqrst/coqdomain.py create mode 100644 doc/tools/coqrst/notations/Makefile create mode 100644 doc/tools/coqrst/notations/TacticNotations.g create mode 100644 doc/tools/coqrst/notations/TacticNotations.tokens create mode 100644 doc/tools/coqrst/notations/TacticNotationsLexer.py create mode 100644 doc/tools/coqrst/notations/TacticNotationsLexer.tokens create mode 100644 doc/tools/coqrst/notations/TacticNotationsParser.py create mode 100644 doc/tools/coqrst/notations/TacticNotationsVisitor.py create mode 100644 doc/tools/coqrst/notations/UbuntuMono-B.ttf create mode 100644 doc/tools/coqrst/notations/UbuntuMono-Square.ttf create mode 100644 doc/tools/coqrst/notations/__init__.py create mode 100755 doc/tools/coqrst/notations/fontsupport.py create mode 100644 doc/tools/coqrst/notations/html.py create mode 100644 doc/tools/coqrst/notations/parsing.py create mode 100644 doc/tools/coqrst/notations/plain.py create mode 100644 doc/tools/coqrst/notations/regexp.py create mode 100644 doc/tools/coqrst/notations/sphinx.py create mode 100644 doc/tools/coqrst/repl/__init__.py create mode 100644 doc/tools/coqrst/repl/ansicolors.py create mode 100644 doc/tools/coqrst/repl/coqtop.py diff --git a/.travis.yml b/.travis.yml index 1699568ca..d775824f0 100644 --- a/.travis.yml +++ b/.travis.yml @@ -138,6 +138,8 @@ matrix: - TEST_TARGET="test-suite" - EXTRA_CONF="-coqide opt -with-doc yes" - EXTRA_OPAM="hevea ${LABLGTK}" + before_install: &sphinx-install + - sudo pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex addons: apt: sources: @@ -158,6 +160,9 @@ matrix: - transfig - imagemagick - tipa + - python3 + - python3-pip + - python3-setuptools - env: - TEST_TARGET="test-suite" @@ -166,6 +171,7 @@ matrix: - CAMLP5_VER="${CAMLP5_VER_BE}" - EXTRA_CONF="-coqide opt -with-doc yes" - EXTRA_OPAM="num hevea ${LABLGTK_BE}" + before_install: *sphinx-install addons: apt: sources: @@ -181,6 +187,7 @@ matrix: - NATIVE_COMP="no" - EXTRA_CONF="-coqide opt -with-doc yes -flambda-opts -O3" - EXTRA_OPAM="num hevea ${LABLGTK_BE}" + before_install: *sphinx-install addons: apt: sources: diff --git a/INSTALL.doc b/INSTALL.doc index 21b21163c..b71115bfa 100644 --- a/INSTALL.doc +++ b/INSTALL.doc @@ -26,6 +26,12 @@ To produce all the documents, the following tools are needed: - convert (ImageMagick) - hevea - hacha + - Python 3 + - Sphinx 1.6.5 (http://www.sphinx-doc.org/en/stable/) + - sphinx_rtd_theme + - pexpect + - beautifulsoup4 + - Antlr4 runtime for Python 3 Under Debian based operating systems (Debian, Ubuntu, ...) a @@ -34,6 +40,10 @@ working set of packages for compiling the documentation for Coq is: texlive texlive-latex-extra texlive-math-extra texlive-fonts-extra texlive-humanities texlive-pictures latex-xcolor hevea transfig imagemagick + python3 python-pip3 + +To install the Python packages required to build the user manual, run: + pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect Compilation diff --git a/Makefile b/Makefile index 03b6e576f..c31534f36 100644 --- a/Makefile +++ b/Makefile @@ -241,6 +241,7 @@ docclean: rm -f doc/common/version.tex rm -f doc/refman/styles.hva doc/refman/cover.html doc/refman/Reference-Manual.html rm -f doc/coq.tex + rm -rf doc/sphinx/_build archclean: clean-ide optclean voclean rm -rf _build diff --git a/Makefile.doc b/Makefile.doc index 9fd93651d..a98f35a1c 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -46,6 +46,14 @@ else COQTEXOPTS:=-boot -n 72 -sl -small endif +# Sphinx-related variables +SPHINXOPTS= -j4 +SPHINXBUILD= sphinx-build +SPHINXBUILDDIR= doc/sphinx/_build + +# Internal variables. +ALLSPHINXOPTS= -d $(SPHINXBUILDDIR)/doctrees $(SPHINXOPTS) + DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ @@ -78,12 +86,18 @@ REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png) ### General rules ###################################################################### -.PHONY: doc doc-html doc-pdf doc-ps refman refman-quick tutorial +.PHONY: doc sphinxdoc-html doc-pdf doc-ps refman refman-quick tutorial .PHONY: stdlib full-stdlib rectutorial refman-html-dir INDEXURLS:=doc/refman/html/index_urls.txt -doc: refman tutorial rectutorial stdlib $(INDEXURLS) +doc: sphinx refman tutorial rectutorial stdlib $(INDEXURLS) + +sphinx: coq + $(SHOW)'SPHINXBUILD doc/sphinx' + $(HIDE)COQBIN="$(PWD)/bin" $(SPHINXBUILD) -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html + @echo + @echo "Build finished. The HTML pages are in $(SPHINXBUILDDIR)/html." doc-html:\ doc/tutorial/Tutorial.v.html doc/refman/html/index.html \ @@ -347,9 +361,11 @@ doc/RecTutorial/RecTutorial.html: doc/RecTutorial/RecTutorial.tex # Install all documentation files ###################################################################### -.PHONY: install-doc install-doc-meta install-doc-html install-doc-printable install-doc-index-urls +.PHONY: install-doc install-doc-meta install-doc-html install-doc-printable \ + install-doc-index-urls install-doc-sphinx -install-doc: install-doc-meta install-doc-html install-doc-printable install-doc-index-urls +install-doc: install-doc-meta install-doc-html install-doc-printable \ + install-doc-index-urls install-doc-sphinx install-doc-meta: $(MKDIR) $(FULLDOCDIR) @@ -380,6 +396,12 @@ install-doc-index-urls: $(MKDIR) $(FULLDATADIR) $(INSTALLLIB) $(INDEXURLS) $(FULLDATADIR) +install-doc-sphinx: + $(MKDIR) $(FULLDOCDIR)/sphinx + (for f in `cd doc/sphinx/_build; find . -type f`; do \ + $(MKDIR) $$(dirname $(FULLDOCDIR)/sphinx/$$f);\ + $(INSTALLLIB) doc/sphinx/_build/$$f $(FULLDOCDIR)/sphinx/$$f;\ + done) ########################################################################### # Documentation of the source code (using ocamldoc) diff --git a/configure.ml b/configure.ml index 435fe8626..4726831e4 100644 --- a/configure.ml +++ b/configure.ml @@ -957,15 +957,16 @@ let strip = (** * Documentation : do we have latex, hevea, ... *) +let check_sphinx_deps () = + ignore (run (which "python3") ["doc/tools/coqrst/checkdeps.py"]) + let check_doc () = let err s = die (sprintf "A documentation build was requested, but %s was not found." s); in - if not (program_in_path "latex") then err "latex"; - if not (program_in_path "hevea") then err "hevea"; - if not (program_in_path "hacha") then err "hacha"; - if not (program_in_path "fig2dev") then err "fig2dev"; - if not (program_in_path "convert") then err "convert" + if not (program_in_path "python3") then err "python3"; + if not (program_in_path "sphinx-build") then err "sphinx-build"; + check_sphinx_deps () let _ = if !prefs.withdoc then check_doc () diff --git a/default.nix b/default.nix index af2a13a84..2011bf574 100644 --- a/default.nix +++ b/default.nix @@ -22,7 +22,7 @@ # a symlink to where Coq was installed. { pkgs ? (import {}), ocamlPackages ? pkgs.ocamlPackages, - buildIde ? true, doCheck ? true }: + buildIde ? true, buildDoc ? true, doCheck ? true }: with pkgs; @@ -43,6 +43,15 @@ stdenv.mkDerivation rec { # CoqIDE dependencies ocamlPackages.lablgtk + ] else []) ++ (if buildDoc then [ + + # Sphinx doc dependencies + ocamlPackages.lablgtk + pkgconfig (python3.withPackages + (ps: [ ps.sphinx ps.sphinx_rtd_theme ps.pexpect ps.beautifulsoup4 + ps.antlr4-python3-runtime ps.sphinxcontrib-bibtex ])) + antlr4 + ] else []) ++ (if doCheck then # Test-suite dependencies diff --git a/doc/LICENSE b/doc/LICENSE index 0aa0d629e..7ae31b089 100644 --- a/doc/LICENSE +++ b/doc/LICENSE @@ -2,10 +2,14 @@ The Coq Reference Manual is a collective work from the Coq Development Team whose members are listed in the file CREDITS of the Coq source package. All related documents (the LaTeX and BibTeX sources, the embedded png files, and the PostScript, PDF and html outputs) are -copyright (c) INRIA 1999-2006. The material connected to the Reference -Manual may be distributed only subject to the terms and conditions set -forth in the Open Publication License, v1.0 or later (the latest -version is presently available at http://www.opencontent.org/openpub/). +copyright (c) INRIA 1999-2006, with the exception of the Ubuntu font files +(UbuntuMono-Square.ttf and UbuntuMono-B.ttf), derived from UbuntuMono-Regular, +which is Copyright 2010,2011 Canonical Ltd and licensed under the Ubuntu font +license, version 1.0 +(https://www.ubuntu.com/legal/terms-and-policies/font-licence). The material +connected to the Reference Manual may be distributed only subject to the terms +and conditions set forth in the Open Publication License, v1.0 or later (the +latest version is presently available at http://www.opencontent.org/openpub/). Options A and B are *not* elected. The Coq Tutorial is a work by Gérard Huet, Gilles Kahn and Christine diff --git a/doc/sphinx/MIGRATING b/doc/sphinx/MIGRATING new file mode 100644 index 000000000..fa6fe1537 --- /dev/null +++ b/doc/sphinx/MIGRATING @@ -0,0 +1,238 @@ +How to migrate the Coq Reference Manual to Sphinx +================================================= + +# Install Python3 packages (requires Python 3, python3-pip, python3-setuptools) + + * pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex + +# You may want to do this under a virtualenv, particularly if you end up with issues finding sphinxcontrib.bibtex. http://docs.python-guide.org/en/latest/dev/virtualenvs/ + + * pip3 install virtualenv + * virtualenv coqsphinxing # you may want to use -p to specify the python version + * source coqsphinxing/bin/activate # activate the virtual environment + +# After activating the virtual environment you can run the above pip3 command to install sphinx. You will have to activate the virtual environment before building the docs in your session. + +# Add this Elisp code to .emacs, if you're using emacs (recommended): + + (defun sphinx/quote-coq-refman-region (left right &optional beg end count) + (unless beg + (if (region-active-p) + (setq beg (region-beginning) end (region-end)) + (setq beg (point) end nil))) + (unless count + (setq count 1)) + (save-excursion + (goto-char (or end beg)) + (dotimes (_ count) (insert right))) + (save-excursion + (goto-char beg) + (dotimes (_ count) (insert left))) + (if (and end (characterp left)) ;; Second test handles the ::`` case + (goto-char (+ (* 2 count) end)) + (goto-char (+ count beg)))) + + (defun sphinx/coqtop (beg end) + (interactive (list (region-beginning) (region-end))) + (replace-regexp "^Coq < " " " nil beg end) + (indent-rigidly beg end -3) + (goto-char beg) + (insert ".. coqtop:: all\n\n")) + + (defun sphinx/rst-coq-action () + (interactive) + (pcase (read-char "Command?") + (?g (sphinx/quote-coq-refman-region ":g:`" "`")) + (?n (sphinx/quote-coq-refman-region ":n:`" "`")) + (?t (sphinx/quote-coq-refman-region ":token:`" "`")) + (?m (sphinx/quote-coq-refman-region ":math:`" "`")) + (?: (sphinx/quote-coq-refman-region "::`" "`")) + (?` (sphinx/quote-coq-refman-region "``" "``")) + (?c (sphinx/coqtop (region-beginning) (region-end))))) + + (global-set-key (kbd "") #'sphinx/rst-coq-action) + + With this code installed, you can hit "F12" followed by an appropriate key to do quick markup of text + (this will make more sense once you've started editing the text). + +# Fork the Coq repo, if needed: + + https://github.com/coq/coq + +# Clone the repo to your work machine + +# Add Maxime Dénès's repo as a remote: + + git remote add sphinx https://github.com/maximedenes/coq.git + + (or choose a name other than "sphinx") + + Verify with: + + git remote -v + +# Fetch from the remote + + git fetch sphinx + +# Checkout the sphinx-doc branch + + git checkout sphinx-doc + + You should pull from the repo from time to time to keep your local copy up-to-date: + + git pull sphinx sphinx-doc + + You may want to create a new branch to do your work in. + +# Choose a Reference Manual chapter to work on at + + https://docs.google.com/document/d/1Yo7dV4OI0AY9Di-lsEQ3UTmn5ygGLlhxjym7cTCMCWU + +# For each chapter, raw ReStructuredText (the Sphinx format), created by the "html2rest" utility, + is available in the directory porting/raw-rst/ + + Elsewhere, depending on the chapter, there should be an almost-empty template file already created, + which is in the location where the final version should go + +# Manually edit the .rst file, place it in the correct location + + There are small examples in sphinx/porting/, a larger example in language/gallina-extensions.rst + + (N.B.: the migration is a work-in-progress, your suggestions are welcome) + + Find the chapter you're working on from the online manual at https://coq.inria.fr/distrib/current/refman/. + At the top of the file, after the chapter heading, add: + + :Source: https://coq.inria.fr/distrib/current/refman/the-chapter-file.html + :Converted by: Your Name + + N.B.: These source and converted-by annotations should help for the migration phase. Later on, + those annotations will be removed, and contributors will be mentioned in the Coq credits. + + Remove chapter numbers + + Replace section, subsection numbers with reference labels: + + .. _some-reference-label: + + Place the label before the section or subsection, followed by a blank line. + + Note the leading underscore. Use :ref:`some_reference-label` to refer to such a label; note the leading underscore is omitted. + Many cross-references may be to other chapters. If the required label exists, use it. Otherwise, use a dummy reference of the form + `TODO-n.n.n-mnemonic` we can fixup later. Example: + + :ref:`TODO-1.3.2-definitions` + + We can grep for those TODOs, and the existing subsection number makes it easy to find in the exisyting manual. + + For the particular case of references to chapters, we can use a +convention for the cross-reference name, so no TODO is needed. + + :ref:`thegallinaspecificationlanguage` + +That is, the chapter label is the chapter title, all in lower-case, +with no spaces or punctuation. For chapters with subtitles marked with +a ":", like those for Omega and Nsatz, use just the chapter part +preceding the ":". These labels should already be in the +placeholder .rst files for each chapter. + + + You can also label other items, like grammars, with the same syntax. To refer to such labels, not involving a + section or subsection, use the syntax + + :ref:`Some link text ` + + Yes, the angle-brackets are needed here! + + For bibliographic references (those in biblio.bib), use :cite:`thecitation`. + + Grammars will get mangled by the translation. Look for "productionlist" in the examples, also see + http://www.sphinx-doc.org/en/stable/markup/para.html. + + For Coq examples that appear, look at the "coqtop" syntax in porting/tricky-bits.rst. The Sphinx + script will run coqtop on those examples, and can show the output (or not). + + The file replaces.rst contains replacement definitions for some items that are clumsy to write out otherwise. + Use + + .. include:: replaces.rst + + to gain access to those definitions in your file (you might need a path prefix). Some especially-important + replacements are |Cic|, |Coq|, |CoqIDE|, and |Gallina|, which display those names in small-caps. Please use them, + so that they're rendered consistently. + + Similarly, there are some LaTeX macros in preamble.rst that can be useful. + + Conventions: + + - Keywords and other literal text is double-backquoted (e.g. ``Module``, ``Section``, ``(``, ``,``). + + - Metavariables are single-backquotes (e.g. `term`, `ident`) + + - Use the cmd directive for Vernacular commands, like: + + .. cmd:: Set Printing All. + + Within this directive, prefix metavariables (ident, term) with @: + + .. cmd:: Add Printing Let @ident. + + There's also the "cmdv" directive for variants of a command. + + - Use the "exn" and "warn" directives for errors and warnings: + + .. exn:: Something's not right. + .. warn:: You shouldn't do that. + + - Use the "example" directive for examples + + - Use the "g" role for inline Gallina, like :g:`fun x => x` + + - Use code blocks for blocks of Gallina. You can use a double-colon at the end of a line:: + + your code here + + which prints a single colon, or put the double-colon on a newline. + +:: + + your other code here + +# Making changes to the text + + The goal of the migration is simply to change the storage format from LaTeX to ReStructuredText. The goal is not + to make any organizational or other substantive changes to the text. If you do notice nits (misspellings, wrong + verb tense, and so on), please do change them. For example, the programming language that Coq is written in is these days + called "OCaml", and there are mentions of the older name "Objective Caml" in the reference manual that should be changed. + +# Build, view the manual + + In the root directory of your local repo, run "make sphinx". You can view the result in a browser by loading the HTML file + associated with your chapter, which will be contained in the directory doc/sphinx/_build/html/ beneath the repo root directory. + Make any changes you need until there are no build warnings and the output is perfect. :-) + +# Creating pull requests + + When your changes are done, commit them, push to your fork: + + git commit -m "useful commit message" file + git push origin sphinx-doc + + (or push to another branch, if you've created one). Then go to your GitHub + fork and create a pull request against Maxime's sphinx-doc + branch. If your commit is recent, you should see a link on your + fork's code page to do that. Otherwise, you may need to go to your + branch on GitHub to do that. + +# Issues/Questions/Suggestions + + As the migration proceeds, if you have technical issues, have a more general question, or want to suggest something, please contact: + + Paul Steckler + Maxime Dénès + +# Issues + + Should the stuff in replaces.rst go in preamble.rst? + In LaTeX, some of the grammars add productions to existing nonterminals, like term ++= ... . How to indicate that? diff --git a/doc/sphinx/_static/UbuntuMono-Square.ttf b/doc/sphinx/_static/UbuntuMono-Square.ttf new file mode 100644 index 000000000..12b7c6d51 Binary files /dev/null and b/doc/sphinx/_static/UbuntuMono-Square.ttf differ 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 */ +/* +% \def\newcssclass#1#2{\expandafter\def\csname DUrole#1\endcsname ##1{#2}} +% + +\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}} + +% +% Make it easier to define new commands matching CSS classes +\newcommand{\newcssclass}[2]{% + \expandafter\def\csname DUrole#1\endcsname##1{#2} +} +% + +\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 */ +/* .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 */ +/* 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 */ +/* v documentation" by default. +#html_title = 'Coq 8.5 v8.5pl1' + +# A shorter title for the navigation bar. Default is the same as html_title. +#html_short_title = None + +# The name of an image file (relative to this directory) to place at the top +# of the sidebar. +#html_logo = None + +# The name of an image file (relative to this directory) to use as a favicon of +# the docs. This file should be a Windows icon file (.ico) being 16x16 or 32x32 +# pixels large. +#html_favicon = None + +# Add any paths that contain custom static files (such as style sheets) here, +# relative to this directory. They are copied after the builtin static files, +# so a file named "default.css" will overwrite the builtin "default.css". +html_static_path = ['_static'] + +# Add any extra paths that contain custom files (such as robots.txt or +# .htaccess) here, relative to this directory. These files are copied +# directly to the root of the documentation. +#html_extra_path = [] + +# If not None, a 'Last updated on:' timestamp is inserted at every page +# bottom, using the given strftime format. +# The empty string is equivalent to '%b %d, %Y'. +#html_last_updated_fmt = None + +# If true, SmartyPants will be used to convert quotes and dashes to +# typographically correct entities. +html_use_smartypants = False # FIXME wrap code in tags, otherwise quotesget converted in there + +# Custom sidebar templates, maps document names to template names. +#html_sidebars = {} + +# Additional templates that should be rendered to pages, maps page names to +# template names. +#html_additional_pages = {} + +# If false, no module index is generated. +#html_domain_indices = True + +# If false, no index is generated. +#html_use_index = True + +# If true, the index is split into individual pages for each letter. +#html_split_index = False + +# If true, links to the reST sources are added to the pages. +#html_show_sourcelink = True + +# If true, "Created using Sphinx" is shown in the HTML footer. Default is True. +#html_show_sphinx = True + +# If true, "(C) Copyright ..." is shown in the HTML footer. Default is True. +#html_show_copyright = True + +# If true, an OpenSearch description file will be output, and all pages will +# contain a tag referring to it. The value of this option must be the +# base URL from which the finished HTML is served. +#html_use_opensearch = '' + +# This is the file name suffix for HTML files (e.g. ".xhtml"). +#html_file_suffix = None + +# Language to be used for generating the HTML full-text search index. +# Sphinx supports the following languages: +# 'da', 'de', 'en', 'es', 'fi', 'fr', 'h', 'it', 'ja' +# 'nl', 'no', 'pt', 'ro', 'r', 'sv', 'tr', 'zh' +#html_search_language = 'en' + +# A dictionary with options for the search language support, empty by default. +# 'ja' uses this config value. +# 'zh' user can custom change `jieba` dictionary path. +#html_search_options = {'type': 'default'} + +# The name of a javascript file (relative to the configuration directory) that +# implements a search results scorer. If empty, the default will be used. +#html_search_scorer = 'scorer.js' + +# Output file base name for HTML help builder. +htmlhelp_basename = 'Coq85doc' + +# -- Options for LaTeX output --------------------------------------------- + +########################### +# Set things up for XeTeX # +########################### +latex_elements = { + 'babel': '', + 'fontenc': '', + 'inputenc': '', + 'utf8extra': '', + 'cmappkg': '', + # https://www.topbug.net/blog/2015/12/10/a-collection-of-issues-about-the-latex-output-in-sphinx-and-the-solutions/ + 'papersize': 'letterpaper', + 'classoptions': ',openany', # No blank pages + 'polyglossia' : '\\usepackage{polyglossia}', + 'unicode-math' : '\\usepackage{unicode-math}', + 'microtype' : '\\usepackage{microtype}', + "preamble": r"\usepackage{coqnotations}" +} + +from sphinx.builders.latex import LaTeXBuilder + +######## +# done # +######## + +latex_additional_files = ["_static/coqnotations.sty"] + +# Grouping the document tree into LaTeX files. List of tuples +# (source start file, target name, title, +# author, documentclass [howto, manual, or own class]). +latex_documents = [ + (master_doc, 'Coq85.tex', 'Coq 8.5 Documentation', + 'The Coq Development Team (edited by C. Pit-Claudel)', 'manual'), +] + +# The name of an image file (relative to this directory) to place at the top of +# the title page. +#latex_logo = None + +# For "manual" documents, if this is true, then toplevel headings are parts, +# not chapters. +#latex_use_parts = False + +# If true, show page references after internal links. +#latex_show_pagerefs = False + +# If true, show URL addresses after external links. +#latex_show_urls = False + +# Documents to append as an appendix to all manuals. +#latex_appendices = [] + +# If false, no module index is generated. +#latex_domain_indices = True + + +# -- Options for manual page output --------------------------------------- + +# One entry per manual page. List of tuples +# (source start file, name, description, authors, manual section). +man_pages = [ + (master_doc, 'coq85', 'Coq 8.5 Documentation', + [author], 1) +] + +# If true, show URL addresses after external links. +#man_show_urls = False + + +# -- Options for Texinfo output ------------------------------------------- + +# Grouping the document tree into Texinfo files. List of tuples +# (source start file, target name, title, author, +# dir menu entry, description, category) +texinfo_documents = [ + (master_doc, 'Coq85', 'Coq 8.5 Documentation', + author, 'Coq85', 'One line description of project.', + 'Miscellaneous'), +] + +# Documents to append as an appendix to all manuals. +#texinfo_appendices = [] + +# If false, no module index is generated. +#texinfo_domain_indices = True + +# How to display URL addresses: 'footnote', 'no', or 'inline'. +#texinfo_show_urls = 'footnote' + +# If true, do not generate a @detailmenu in the "Top" node's menu. +#texinfo_no_detailmenu = False + + +# -- Options for Epub output ---------------------------------------------- + +# Bibliographic Dublin Core info. +epub_title = project +epub_author = author +epub_publisher = author +epub_copyright = copyright + +# The basename for the epub file. It defaults to the project name. +#epub_basename = project + +# The HTML theme for the epub output. Since the default themes are not +# optimized for small screen space, using the same theme for HTML and epub +# output is usually not wise. This defaults to 'epub', a theme designed to save +# visual space. +#epub_theme = 'epub' + +# The language of the text. It defaults to the language option +# or 'en' if the language is not set. +#epub_language = '' + +# The scheme of the identifier. Typical schemes are ISBN or URL. +#epub_scheme = '' + +# The unique identifier of the text. This can be a ISBN number +# or the project homepage. +#epub_identifier = '' + +# A unique identification for the text. +#epub_uid = '' + +# A tuple containing the cover image and cover page html template filenames. +#epub_cover = () + +# A sequence of (type, uri, title) tuples for the guide element of content.opf. +#epub_guide = () + +# HTML files that should be inserted before the pages created by sphinx. +# The format is a list of tuples containing the path and title. +#epub_pre_files = [] + +# HTML files that should be inserted after the pages created by sphinx. +# The format is a list of tuples containing the path and title. +#epub_post_files = [] + +# A list of files that should not be packed into the epub file. +epub_exclude_files = ['search.html'] + +# The depth of the table of contents in toc.ncx. +#epub_tocdepth = 3 + +# Allow duplicate toc entries. +#epub_tocdup = True + +# Choose between 'default' and 'includehidden'. +#epub_tocscope = 'default' + +# Fix unsupported image types using the Pillow. +#epub_fix_images = False + +# Scale large images. +#epub_max_image_width = 0 + +# How to display URL addresses: 'footnote', 'no', or 'inline'. +#epub_show_urls = 'inline' + +# If false, no index is generated. +#epub_use_index = True + +# navtree options +navtree_shift = True diff --git a/doc/sphinx/coqdoc.css b/doc/sphinx/coqdoc.css new file mode 100644 index 000000000..a34bb81eb --- /dev/null +++ b/doc/sphinx/coqdoc.css @@ -0,0 +1,338 @@ +/************************************************************************/ +/* * The Coq Proof Assistant / The Coq Development Team */ +/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */ +/* ) */ + +.id { display: inline; } + +.id[title="constructor"] { + color: rgb(60%,0%,0%); +} + +.id[title="var"] { + color: rgb(40%,0%,40%); +} + +.id[title="variable"] { + color: rgb(40%,0%,40%); +} + +.id[title="definition"] { + color: rgb(0%,40%,0%); +} + +.id[title="abbreviation"] { + color: rgb(0%,40%,0%); +} + +.id[title="lemma"] { + color: rgb(0%,40%,0%); +} + +.id[title="instance"] { + color: rgb(0%,40%,0%); +} + +.id[title="projection"] { + color: rgb(0%,40%,0%); +} + +.id[title="method"] { + color: rgb(0%,40%,0%); +} + +.id[title="inductive"] { + color: rgb(0%,0%,80%); +} + +.id[title="record"] { + color: rgb(0%,0%,80%); +} + +.id[title="class"] { + color: rgb(0%,0%,80%); +} + +.id[title="keyword"] { + color : #cf1d1d; +/* color: black; */ +} + +/* Deprecated rules using the 'type' attribute of (not xhtml valid) */ + +.id[type="constructor"] { + color: rgb(60%,0%,0%); +} + +.id[type="var"] { + color: rgb(40%,0%,40%); +} + +.id[type="variable"] { + color: rgb(40%,0%,40%); +} + +.id[type="definition"] { + color: rgb(0%,40%,0%); +} + +.id[type="abbreviation"] { + color: rgb(0%,40%,0%); +} + +.id[type="lemma"] { + color: rgb(0%,40%,0%); +} + +.id[type="instance"] { + color: rgb(0%,40%,0%); +} + +.id[type="projection"] { + color: rgb(0%,40%,0%); +} + +.id[type="method"] { + color: rgb(0%,40%,0%); +} + +.id[type="inductive"] { + color: rgb(0%,0%,80%); +} + +.id[type="record"] { + color: rgb(0%,0%,80%); +} + +.id[type="class"] { + color: rgb(0%,0%,80%); +} + +.id[type="keyword"] { + color : #cf1d1d; +/* color: black; */ +} + +.inlinecode .id { + color: rgb(0%,0%,0%); +} + + +/* TOC */ + +#toc h2 { + padding: 10px; + background-color: rgb(60%,60%,100%); +} + +#toc li { + padding-bottom: 8px; +} + +/* Index */ + +#index { + margin: 0; + padding: 0; + width: 100%; +} + +#index #frontispiece { + margin: 1em auto; + padding: 1em; + width: 60%; +} + +.booktitle { font-size : 140% } +.authors { font-size : 90%; + line-height: 115%; } +.moreauthors { font-size : 60% } + +#index #entrance { + text-align: center; +} + +#index #entrance .spacer { + margin: 0 30px 0 30px; +} + +#index #footer { + position: absolute; + bottom: 0; +} + +.paragraph { + height: 0.75em; +} + +ul.doclist { + margin-top: 0em; + margin-bottom: 0em; +} diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst new file mode 100644 index 000000000..e69de29bb diff --git a/doc/tools/coqrst/__init__.py b/doc/tools/coqrst/__init__.py new file mode 100644 index 000000000..2dda7d921 --- /dev/null +++ b/doc/tools/coqrst/__init__.py @@ -0,0 +1,10 @@ +########################################################################## +## # The Coq Proof Assistant / The Coq Development Team ## +## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## ", "<-", "<->", "=>", "<=", ">=", "<>", "~", "/\\", "\\/", "|-", "*", "forall", "exists"] +COQDOC_HEADER = "".join("(** remove printing {} *)".format(s) for s in COQDOC_SYMBOLS) + +def coqdoc(coq_code, coqdoc_bin = os.path.join(os.getenv("COQBIN"),"coqdoc")): + """Get the output of coqdoc on coq_code.""" + fd, filename = mkstemp(prefix="coqdoc-", suffix=".v") + try: + os.write(fd, COQDOC_HEADER.encode("utf-8")) + os.write(fd, coq_code.encode("utf-8")) + os.close(fd) + return check_output([coqdoc_bin] + COQDOC_OPTIONS + [filename], timeout = 2).decode("utf-8") + finally: + os.remove(filename) + +def is_whitespace_string(elem): + return isinstance(elem, NavigableString) and elem.strip() == "" + +def strip_soup(soup, pred): + """Strip elements maching pred from front and tail of soup.""" + while soup.contents and pred(soup.contents[-1]): + soup.contents.pop() + + skip = 0 + for elem in soup.contents: + if not pred(elem): + break + skip += 1 + + soup.contents[:] = soup.contents[skip:] + +def lex(source): + """Convert source into a stream of (css_classes, token_string).""" + coqdoc_output = coqdoc(source) + soup = BeautifulSoup(coqdoc_output, "html.parser") + root = soup.find(class_='code') + strip_soup(root, is_whitespace_string) + for elem in root.children: + if isinstance(elem, NavigableString): + yield [], elem + elif elem.name == "span": + cls = "coqdoc-{}".format(elem['title']) + yield [cls], elem.string + elif elem.name == 'br': + pass + else: + raise ValueError(elem) + +def main(): + """Lex stdin (for testing purposes)""" + import sys + for classes, text in lex(sys.stdin.read()): + print(repr(text) + "\t" ' '.join(classes)) + +if __name__ == '__main__': + main() diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py new file mode 100644 index 000000000..18f32d7a8 --- /dev/null +++ b/doc/tools/coqrst/coqdomain.py @@ -0,0 +1,816 @@ +########################################################################## +## # The Coq Proof Assistant / The Coq Development Team ## +## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +##