diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-02-10 15:52:24 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 15:12:51 +0100 |
| commit | 4aaf28cc905bebf757b02ad911a6eed78714cac7 (patch) | |
| tree | 91322ece8b35fc82247938d8a5dc0e70cd22597b | |
| parent | 1505304e856091e10ff3511edecb9cf7c20974b2 (diff) | |
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.
43 files changed, 3930 insertions, 14 deletions
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 @@ -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 <nixpkgs> {}), 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 "<f12>") #'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 <label-name>` + + 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 <steck@stecksoft.com> + Maxime Dénès <maxime.denes@inria.fr> + +# 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 Binary files differnew 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%; +} diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py new file mode 100755 index 000000000..0bff41a25 --- /dev/null +++ b/doc/sphinx/conf.py @@ -0,0 +1,400 @@ +#!/usr/bin/env python3 +# -*- coding: utf-8 -*- +########################################################################## +## # 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) ## +########################################################################## +# +# Coq 8.5 documentation build configuration file, created by +# sphinx-quickstart on Wed May 11 11:23:13 2016. +# +# This file is execfile()d with the current directory set to its +# containing dir. +# +# Note that not all possible configuration values are present in this +# autogenerated file. +# +# All configuration values have a default; values that are commented out +# serve to show the default. + +import sys +import os + +# Increase recursion limit for sphinx +sys.setrecursionlimit(1500) + +# If extensions (or modules to document with autodoc) are in another directory, +# add these directories to sys.path here. If the directory is relative to the +# documentation root, use os.path.abspath to make it absolute, like shown here. +sys.path.append(os.path.abspath('../tools/')) + +# -- General configuration ------------------------------------------------ + +# If your documentation needs a minimal Sphinx version, state it here. +#needs_sphinx = '1.0' + +# Add any Sphinx extension module names here, as strings. They can be +# extensions coming with Sphinx (named 'sphinx.ext.*') or your custom +# ones. +extensions = [ + 'sphinx.ext.mathjax', + 'sphinx.ext.todo', + 'sphinxcontrib.bibtex', + 'coqrst.coqdomain' +] + +# Add any paths that contain templates here, relative to this directory. +templates_path = ['_templates'] + +# The suffix(es) of source filenames. +# You can specify multiple suffix as a list of string: +# source_suffix = ['.rst', '.md'] +source_suffix = '.rst' + +# The encoding of source files. +#source_encoding = 'utf-8-sig' + +# The master toctree document. +master_doc = 'index' + +# General information about the project. +project = 'Coq' +copyright = '2016, Inria' +author = 'The Coq Development Team' + +# The version info for the project you're documenting, acts as replacement for +# |version| and |release|, also used in various other places throughout the +# built documents. +# +# The short X.Y version. +version = '8.7' +# The full version, including alpha/beta/rc tags. +release = '8.7.dev' + +# The language for content autogenerated by Sphinx. Refer to documentation +# for a list of supported languages. +# +# This is also used if you do content translation via gettext catalogs. +# Usually you set "language" from the command line for these cases. +language = None + +# There are two options for replacing |today|: either, you set today to some +# non-false value, then it is used: +#today = '' +# Else, today_fmt is used as the format for a strftime call. +#today_fmt = '%B %d, %Y' + +# List of patterns, relative to source directory, that match files and +# directories to ignore when looking for source files. +# This patterns also effect to html_static_path and html_extra_path +exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store'] + +# The reST default role (used for this markup: `text`) to use for all +# documents. +#default_role = None + +# Use the Coq domain +primary_domain = 'coq' + +# If true, '()' will be appended to :func: etc. cross-reference text. +#add_function_parentheses = True + +# If true, the current module name will be prepended to all description +# unit titles (such as .. function::). +#add_module_names = True + +# If true, sectionauthor and moduleauthor directives will be shown in the +# output. They are ignored by default. +#show_authors = False + +# The name of the Pygments (syntax highlighting) style to use. +pygments_style = 'sphinx' +highlight_language = 'text' + +# A list of ignored prefixes for module index sorting. +#modindex_common_prefix = [] + +# If true, keep warnings as "system message" paragraphs in the built documents. +#keep_warnings = False + +# If true, `todo` and `todoList` produce output, else they produce nothing. +todo_include_todos = False + +# Extra warnings, including undefined references +nitpicky = False + +# -- Options for HTML output ---------------------------------------------- + +# The theme to use for HTML and HTML Help pages. See the documentation for +# a list of builtin themes. +html_theme = 'sphinx_rtd_theme' +# html_theme = 'agogo' +# html_theme = 'alabaster' +# html_theme = 'haiku' +# html_theme = 'bizstyle' + +# Theme options are theme-specific and customize the look and feel of a theme +# further. For a list of options available for each theme, see the +# documentation. +#html_theme_options = {} + +# Add any paths that contain custom themes here, relative to this directory. +import sphinx_rtd_theme +html_theme_path = [sphinx_rtd_theme.get_html_theme_path()] + +# The name for this set of Sphinx documents. +# "<project> v<release> 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 <code> 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 <link> 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 */ +/* <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) */ +/************************************************************************/ +body { padding: 0px 0px; + margin: 0px 0px; + background-color: white } + +#page { display: block; + padding: 0px; + margin: 0px; + padding-bottom: 10px; } + +#header { display: block; + position: relative; + padding: 0; + margin: 0; + vertical-align: middle; + border-bottom-style: solid; + border-width: thin } + +#header h1 { padding: 0; + margin: 0;} + + +/* Contents */ + +#main{ display: block; + padding: 10px; + font-family: sans-serif; + font-size: 100%; + line-height: 100% } + +#main h1 { line-height: 95% } /* allow for multi-line headers */ + +#main a.idref:visited {color : #416DFF; text-decoration : none; } +#main a.idref:link {color : #416DFF; text-decoration : none; } +#main a.idref:hover {text-decoration : none; } +#main a.idref:active {text-decoration : none; } + +#main a.modref:visited {color : #416DFF; text-decoration : none; } +#main a.modref:link {color : #416DFF; text-decoration : none; } +#main a.modref:hover {text-decoration : none; } +#main a.modref:active {text-decoration : none; } + +#main .keyword { color : #cf1d1d } +#main { color: black } + +.section { background-color: rgb(60%,60%,100%); + padding-top: 13px; + padding-bottom: 13px; + padding-left: 3px; + margin-top: 5px; + margin-bottom: 5px; + font-size : 175% } + +h2.section { background-color: rgb(80%,80%,100%); + padding-left: 3px; + padding-top: 12px; + padding-bottom: 10px; + font-size : 130% } + +h3.section { background-color: rgb(90%,90%,100%); + padding-left: 3px; + padding-top: 7px; + padding-bottom: 7px; + font-size : 115% } + +h4.section { +/* + background-color: rgb(80%,80%,80%); + max-width: 20em; + padding-left: 5px; + padding-top: 5px; + padding-bottom: 5px; +*/ + background-color: white; + padding-left: 0px; + padding-top: 0px; + padding-bottom: 0px; + font-size : 100%; + font-weight : bold; + text-decoration : underline; + } + +#main .doc { margin: 0px; + font-family: sans-serif; + font-size: 100%; + line-height: 125%; + max-width: 40em; + color: black; + padding: 10px; + background-color: #90bdff } + +.inlinecode { + display: inline; +/* font-size: 125%; */ + color: #666666; + font-family: monospace } + +.doc .inlinecode { + display: inline; + font-size: 120%; + color: rgb(30%,30%,70%); + font-family: monospace } + +.doc .inlinecode .id { + color: rgb(30%,30%,70%); +} + +.inlinecodenm { + display: inline; + color: #444444; +} + +.doc .code { + display: inline; + font-size: 120%; + color: rgb(30%,30%,70%); + font-family: monospace } + +.comment { + display: inline; + font-family: monospace; + color: rgb(50%,50%,80%); +} + +.code { + display: block; +/* padding-left: 15px; */ + font-size: 110%; + font-family: monospace; + } + +table.infrule { + border: 0px; + margin-left: 50px; + margin-top: 10px; + margin-bottom: 10px; +} + +td.infrule { + font-family: monospace; + text-align: center; +/* color: rgb(35%,35%,70%); */ + padding: 0px; + line-height: 100%; +} + +tr.infrulemiddle hr { + margin: 1px 0 1px 0; +} + +.infrulenamecol { + color: rgb(60%,60%,60%); + font-size: 80%; + padding-left: 1em; + padding-bottom: 0.1em +} + +/* Pied de page */ + +#footer { font-size: 65%; + font-family: sans-serif; } + +/* Identifiers: <span class="id" title="...">) */ + +.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 <span> (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 --- /dev/null +++ b/doc/sphinx/index.rst 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 ## +## <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) ## +########################################################################## +"""Utilities for documenting Coq in Sphinx""" diff --git a/doc/tools/coqrst/checkdeps.py b/doc/tools/coqrst/checkdeps.py new file mode 100644 index 000000000..11f95c4e9 --- /dev/null +++ b/doc/tools/coqrst/checkdeps.py @@ -0,0 +1,39 @@ +########################################################################## +## # 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) ## +########################################################################## +from __future__ import print_function +import sys + +def eprint(*args, **kwargs): + print(*args, file=sys.stderr, **kwargs) + +def missing_dep(dep): + eprint('Cannot find %s (needed to build documentation)' % dep) + eprint('You can run `pip3 install %s` to install it.' % dep) + sys.exit(1) + +try: + import sphinx_rtd_theme +except: + missing_dep('sphinx_rtd_theme') + +try: + import pexpect +except: + missing_dep('pexpect') + +try: + import antlr4 +except: + missing_dep('antlr4-python3-runtime') + +try: + import bs4 +except: + missing_dep('beautifulsoup4') diff --git a/doc/tools/coqrst/coqdoc/__init__.py b/doc/tools/coqrst/coqdoc/__init__.py new file mode 100644 index 000000000..a89a548e2 --- /dev/null +++ b/doc/tools/coqrst/coqdoc/__init__.py @@ -0,0 +1,10 @@ +########################################################################## +## # 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) ## +########################################################################## +from .main import * diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py new file mode 100644 index 000000000..d464f75bb --- /dev/null +++ b/doc/tools/coqrst/coqdoc/main.py @@ -0,0 +1,86 @@ +########################################################################## +## # 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) ## +########################################################################## +""" +Use CoqDoc to highlight Coq snippets +==================================== + +Pygment's Coq parser isn't the best; instead, use coqdoc to highlight snippets. +Only works for full, syntactically valid sentences; on shorter snippets, coqdoc +swallows parts of the input. + +Works by reparsing coqdoc's output into the output that Sphinx expects from a +lexer. +""" + +import os +from tempfile import mkstemp +from subprocess import check_output + +from bs4 import BeautifulSoup +from bs4.element import NavigableString + +COQDOC_OPTIONS = ['--body-only', '--no-glob', '--no-index', '--no-externals', + '-s', '--html', '--stdout', '--utf8'] + +COQDOC_SYMBOLS = ["->", "<-", "<->", "=>", "<=", ">=", "<>", "~", "/\\", "\\/", "|-", "*", "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 ## +## <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) ## +########################################################################## +"""A Coq domain for Sphinx. + +Currently geared towards Coq's manual, rather than Coq source files, but one +could imagine extending it. +""" + +# pylint: disable=too-few-public-methods + +import re +from itertools import chain +from collections import defaultdict + +from docutils import nodes, utils +from docutils.transforms import Transform +from docutils.parsers.rst import Directive, directives +from docutils.parsers.rst.roles import code_role #, set_classes +from docutils.parsers.rst.directives.admonitions import BaseAdmonition + +from sphinx import addnodes +from sphinx.roles import XRefRole +from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode +from sphinx.directives import ObjectDescription +from sphinx.domains import Domain, ObjType, Index +from sphinx.ext.mathbase import MathDirective, displaymath + +from . import coqdoc +from .repl import ansicolors +from .repl.coqtop import CoqTop +from .notations.sphinx import sphinxify +from .notations.plain import stringify_with_ellipses + +def parse_notation(notation, source, line, rawtext=None): + """Parse notation and wrap it in an inline node""" + node = nodes.inline(rawtext or notation, '', *sphinxify(notation), classes=['notation']) + node.source, node.line = source, line + return node + +def highlight_using_coqdoc(sentence): + """Lex sentence using coqdoc, and yield inline nodes for each token""" + tokens = coqdoc.lex(utils.unescape(sentence, 1)) + for classes, value in tokens: + yield nodes.inline(value, value, classes=classes) + +def make_target(objtype, targetid): + """Create a target to an object of type objtype and id targetid""" + return "coq:{}.{}".format(objtype, targetid) + +class CoqObject(ObjectDescription): + """A generic Coq object; all Coq objects are subclasses of this. + + The fields and methods to override are listed at the top of this class' + implementation. Each object supports the :name: option, which gives an + explicit name to link to. + + See the documentation of CoqDomain for high-level information. + """ + + # The semantic domain in which this object lives. + # It matches exactly one of the roles used for cross-referencing. + subdomain = None + + # The suffix to use in indices for objects of this type + index_suffix = None + + # The annotation to add to headers of objects of this type + annotation = None + + def _name_from_signature(self, signature): # pylint: disable=no-self-use, unused-argument + """Convert a signature into a name to link to. + + Returns None by default, in which case no name will be automatically + generated. + """ + return None + + def _render_signature(self, signature, signode): + """Render a signature, placing resulting nodes into signode.""" + raise NotImplementedError(self) + + option_spec = { + # One can give an explicit name to each documented object + 'name': directives.unchanged + } + + def _subdomain(self): + if self.subdomain is None: + raise ValueError() + return self.subdomain + + def handle_signature(self, signature, signode): + """Prefix signature with the proper annotation, then render it using + _render_signature. + + :returns: the name given to the resulting node, if any + """ + if self.annotation: + annotation = self.annotation + ' ' + signode += addnodes.desc_annotation(annotation, annotation) + self._render_signature(signature, signode) + return self._name_from_signature(signature) + + @property + def _index_suffix(self): + if self.index_suffix: + return " " + self.index_suffix + + def _record_name(self, name, target_id): + """Record a name, mapping it to target_id + + Warns if another object of the same name already exists. + """ + names_in_subdomain = self.env.domaindata['coq']['objects'][self._subdomain()] + # Check that two objects in the same domain don't have the same name + if name in names_in_subdomain: + self.state_machine.reporter.warning( + 'Duplicate Coq object: {}; other is at {}'.format( + name, self.env.doc2path(names_in_subdomain[name][0])), + line=self.lineno) + names_in_subdomain[name] = (self.env.docname, self.objtype, target_id) + + def _add_target(self, signode, name): + """Register a link target ‘name’, pointing to signode.""" + targetid = make_target(self.objtype, nodes.make_id(name)) + if targetid not in self.state.document.ids: + signode['ids'].append(targetid) + signode['names'].append(name) + signode['first'] = (not self.names) + self.state.document.note_explicit_target(signode) + self._record_name(name, targetid) + return targetid + + def _add_index_entry(self, name, target): + """Add name (with target) to the main index.""" + index_text = name + self._index_suffix + self.indexnode['entries'].append(('single', index_text, target, '', None)) + + def run(self): + """Small extension of the parent's run method, handling user-provided names.""" + [idx, node] = super().run() + custom_name = self.options.get("name") + if custom_name: + self.add_target_and_index(custom_name, "", node.children[0]) + return [idx, node] + + def add_target_and_index(self, name, _, signode): + """Create a target and an index entry for name""" + if name: + target = self._add_target(signode, name) + self._add_index_entry(name, target) + return target + +class PlainObject(CoqObject): + """A base class for objects whose signatures should be rendered literaly.""" + def _render_signature(self, signature, signode): + signode += addnodes.desc_name(signature, signature) + +class NotationObject(CoqObject): + """A base class for objects whose signatures should be rendered as nested boxes.""" + def _render_signature(self, signature, signode): + position = self.state_machine.get_source_and_line(self.lineno) + tacn_node = parse_notation(signature, *position) + signode += addnodes.desc_name(signature, '', tacn_node) + +class TacticObject(PlainObject): + """An object to represent Coq tactics""" + subdomain = "tac" + index_suffix = "(tactic)" + annotation = None + +class GallinaObject(PlainObject): + """An object to represent Coq theorems""" + subdomain = "thm" + index_suffix = "(theorem)" + annotation = "Theorem" + +class VernacObject(NotationObject): + """An object to represent Coq commands""" + subdomain = "cmd" + index_suffix = "(command)" + annotation = "Command" + + def _name_from_signature(self, signature): + return stringify_with_ellipses(signature) + +class VernacVariantObject(VernacObject): + """An object to represent variants of Coq commands""" + index_suffix = "(command variant)" + annotation = "Variant" + +class TacticNotationObject(NotationObject): + """An object to represent Coq tactic notations""" + subdomain = "tacn" + index_suffix = "(tactic notation)" + annotation = None + +class TacticNotationVariantObject(TacticNotationObject): + """An object to represent variants of Coq tactic notations""" + index_suffix = "(tactic variant)" + annotation = "Variant" + +class OptionObject(NotationObject): + """An object to represent variants of Coq options""" + subdomain = "opt" + index_suffix = "(option)" + annotation = "Option" + + def _name_from_signature(self, signature): + return stringify_with_ellipses(signature) + +class ExceptionObject(NotationObject): + """An object to represent Coq errors.""" + subdomain = "exn" + index_suffix = "(error)" + annotation = "Error" + # Uses “exn” since “err” already is a CSS class added by “writer_aux”. + + # Generate names automatically + def _name_from_signature(self, signature): + return stringify_with_ellipses(signature) + +class WarningObject(NotationObject): + """An object to represent Coq warnings.""" + subdomain = "warn" + index_suffix = "(warn)" + annotation = "Warning" + + # Generate names automatically + def _name_from_signature(self, signature): + return stringify_with_ellipses(signature) + +def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]): + #pylint: disable=unused-argument, dangerous-default-value + """And inline role for notations""" + notation = utils.unescape(text, 1) + position = inliner.reporter.get_source_and_line(lineno) + return [nodes.literal(rawtext, '', parse_notation(notation, *position, rawtext=rawtext))], [] + +def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]): + #pylint: disable=dangerous-default-value + """And inline role for Coq source code""" + options['language'] = 'Coq' + return code_role(role, rawtext, text, lineno, inliner, options, content) + ## Too heavy: + ## Forked from code_role to use our custom tokenizer; this doesn't work for + ## snippets though: for example CoqDoc swallows the parentheses around this: + ## “(a: A) (b: B)” + # set_classes(options) + # classes = ['code', 'coq'] + # code = utils.unescape(text, 1) + # node = nodes.literal(rawtext, '', *highlight_using_coqdoc(code), classes=classes) + # return [node], [] + +# TODO pass different languages? +LtacRole = GallinaRole = VernacRole = coq_code_role + +class CoqtopDirective(Directive): + """A reST directive to describe interactions with Coqtop. + + Usage:: + + .. coqtop:: (options)+ + + Coq code to send to coqtop + + Example:: + + .. coqtop:: in reset undo + + Print nat. + Definition a := 1. + + Here is a list of permissible options: + + Display + - ‘all’: Display input and output + - ‘in’: Display only input + - ‘out’: Display only output + - ‘none’: Display neither (useful for setup commands) + Behaviour + - ‘reset’: Send a `Reset Initial` command before running this block + - ‘undo’: Send an `Undo n` (n=number of sentences) command after running + all the commands in this block + """ + has_content = True + required_arguments = 0 + optional_arguments = 1 + final_argument_whitespace = True + + def run(self): + # Uses a ‘container’ instead of a ‘literal_block’ to disable + # Pygments-based post-processing (we could also set rawsource to '') + content = '\n'.join(self.content) + options = self.arguments[0].split() if self.arguments else ['in'] + if 'all' in options: + options.extend(['in', 'out']) + node = nodes.container(content, coqtop_options = list(set(options)), + classes=['coqtop', 'literal-block']) + self.add_name(node) + return [node] + +class CoqdocDirective(Directive): + """A reST directive to display Coqtop-formatted source code""" + # TODO implement this as a Pygments highlighter? + has_content = True + required_arguments = 0 + optional_arguments = 0 + final_argument_whitespace = True + + def run(self): + # Uses a ‘container’ instead of a ‘literal_block’ to disable + # Pygments-based post-processing (we could also set rawsource to '') + content = '\n'.join(self.content) + node = nodes.inline(content, '', *highlight_using_coqdoc(content)) + wrapper = nodes.container(content, node, classes=['coqdoc', 'literal-block']) + return [wrapper] + +class ExampleDirective(BaseAdmonition): + """A reST directive for examples""" + node_class = nodes.admonition + + def run(self): + # ‘BaseAdmonition’ checks whether ‘node_class’ is ‘nodes.admonition’, + # and uses arguments[0] as the title in that case (in other cases, the + # title is unset, and it is instead set in the HTML visitor). + assert not self.arguments # Arguments have been parsed as content + self.arguments = ['Example'] + self.options['classes'] = ['admonition', 'note'] + return super().run() + +class PreambleDirective(MathDirective): + r"""A reST directive for hidden math. + + Mostly useful to let MathJax know about `\def`s and `\newcommand`s + """ + def run(self): + self.options['nowrap'] = True + [node] = super().run() + node['classes'] = ["math-preamble"] + return [node] + +class InferenceDirective(Directive): + r"""A small example of what directives let you do in Sphinx. + + Usage:: + + .. inference:: name + + \n-separated premisses + ---------------------- + conclusion + + Example:: + + .. inference:: Prod-Pro + + \WTEG{T}{s} + s \in \Sort + \WTE{\Gamma::(x:T)}{U}{\Prop} + ----------------------------- + \WTEG{\forall~x:T,U}{\Prop} + """ + required_arguments = 1 + optional_arguments = 0 + has_content = True + + def make_math_node(self, latex): + node = displaymath() + node['latex'] = latex + node['label'] = None # Otherwise equations are numbered + node['nowrap'] = False + node['docname'] = self.state.document.settings.env.docname + node['number'] = None + return node + + @staticmethod + def prepare_latex_operand(op): + # TODO: Could use a fancier inference class in LaTeX + return '%\n\\hspace{3em}%\n'.join(op.strip().splitlines()) + + def prepare_latex(self, content): + parts = re.split('^ *----+ *$', content, flags=re.MULTILINE) + if len(parts) != 2: + raise self.error('Expected two parts in ‘inference’ directive, separated by a rule (----).') + + top, bottom = tuple(InferenceDirective.prepare_latex_operand(p) for p in parts) + return "%\n".join(("\\frac{", top, "}{", bottom, "}")) + + def run(self): + self.assert_has_content() + + title = self.arguments[0] + content = '\n'.join(self.content) + latex = self.prepare_latex(content) + math_node = self.make_math_node(latex) + + tid = nodes.make_id(title) + target = nodes.target('', '', ids=['inference-' + tid]) + self.state.document.note_explicit_target(target) + + term, desc = nodes.term('', title), nodes.description('', math_node) + dli = nodes.definition_list_item('', term, desc) + dl = nodes.definition_list(content, target, dli) + set_source_info(self, dl) + return [dl] + +class AnsiColorsParser(): + """Parse ANSI-colored output from Coqtop into Sphinx nodes.""" + + # Coqtop's output crashes ansi.py, because it contains a bunch of extended codes + # This class is a fork of the original ansi.py, released under a BSD license in sphinx-contribs + + COLOR_PATTERN = re.compile('\x1b\\[([^m]+)m') + + def __init__(self): + self.new_nodes, self.pending_nodes = [], [] + + def _finalize_pending_nodes(self): + self.new_nodes.extend(self.pending_nodes) + self.pending_nodes = [] + + def _add_text(self, raw, beg, end): + if beg < end: + text = raw[beg:end] + if self.pending_nodes: + self.pending_nodes[-1].append(nodes.Text(text)) + else: + self.new_nodes.append(nodes.inline('', text)) + + def colorize_str(self, raw): + """Parse raw (an ANSI-colored output string from Coqtop) into Sphinx nodes.""" + last_end = 0 + for match in AnsiColorsParser.COLOR_PATTERN.finditer(raw): + self._add_text(raw, last_end, match.start()) + last_end = match.end() + classes = ansicolors.parse_ansi(match.group(1)) + if 'ansi-reset' in classes: + self._finalize_pending_nodes() + else: + node = nodes.inline() + self.pending_nodes.append(node) + node['classes'].extend(classes) + self._add_text(raw, last_end, len(raw)) + self._finalize_pending_nodes() + return self.new_nodes + +class CoqtopBlocksTransform(Transform): + """Filter handling the actual work for the coqtop directive + + Adds coqtop's responses, colorizes input and output, and merges consecutive + coqtop directives for better visual rendition. + """ + default_priority = 10 + + @staticmethod + def is_coqtop_block(node): + return isinstance(node, nodes.Element) and 'coqtop_options' in node + + @staticmethod + def split_sentences(source): + """Split Coq sentences in source. Could be improved.""" + return re.split(r"(?<=(?<!\.)\.)\s+", source) + + @staticmethod + def parse_options(options): + """Parse options according to the description in CoqtopDirective.""" + opt_undo = 'undo' in options + opt_reset = 'reset' in options + opt_all, opt_none = 'all' in options, 'none' in options + opt_input, opt_output = opt_all or 'in' in options, opt_all or 'out' in options + + unexpected_options = list(set(options) - set(('reset', 'undo', 'all', 'none', 'in', 'out'))) + if unexpected_options: + raise ValueError("Unexpected options for .. coqtop:: {}".format(unexpected_options)) + elif (opt_input or opt_output) and opt_none: + raise ValueError("Inconsistent options for .. coqtop:: ‘none’ with ‘in’, ‘out’, or ‘all’") + elif opt_reset and opt_undo: + raise ValueError("Inconsistent options for .. coqtop:: ‘undo’ with ‘reset’") + + return opt_undo, opt_reset, opt_input and not opt_none, opt_output and not opt_none + + @staticmethod + def block_classes(should_show, contents=None): + """Compute classes to add to a node containing contents. + + :param should_show: Whether this node should be displayed""" + is_empty = contents is not None and re.match(r"^\s*$", contents) + if is_empty or not should_show: + return ['coqtop-hidden'] + else: + return [] + + @staticmethod + def make_rawsource(pairs, opt_input, opt_output): + blocks = [] + for sentence, output in pairs: + output = AnsiColorsParser.COLOR_PATTERN.sub("", output).strip() + if opt_input: + blocks.append(sentence) + if output and opt_output: + blocks.append(re.sub("^", " ", output, flags=re.MULTILINE) + "\n") + return '\n'.join(blocks) + + def add_coqtop_output(self): + """Add coqtop's responses to a Sphinx AST + + Finds nodes to process using is_coqtop_block.""" + with CoqTop(color=True) as repl: + for node in self.document.traverse(CoqtopBlocksTransform.is_coqtop_block): + options = node['coqtop_options'] + opt_undo, opt_reset, opt_input, opt_output = self.parse_options(options) + + if opt_reset: + repl.sendone("Reset Initial.") + pairs = [] + for sentence in self.split_sentences(node.rawsource): + pairs.append((sentence, repl.sendone(sentence))) + if opt_undo: + repl.sendone("Undo {}.".format(len(pairs))) + + dli = nodes.definition_list_item() + for sentence, output in pairs: + # Use Coqdoq to highlight input + in_chunks = highlight_using_coqdoc(sentence) + dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(opt_input)) + # Parse ANSI sequences to highlight output + out_chunks = AnsiColorsParser().colorize_str(output) + dli += nodes.definition(output, *out_chunks, classes=self.block_classes(opt_output, output)) + node.clear() + node.rawsource = self.make_rawsource(pairs, opt_input, opt_output) + node['classes'].extend(self.block_classes(opt_input or opt_output)) + node += nodes.inline('', '', classes=['coqtop-reset'] * opt_reset) + node += nodes.definition_list(node.rawsource, dli) + + @staticmethod + def merge_coqtop_classes(kept_node, discarded_node): + discarded_classes = discarded_node['classes'] + if not 'coqtop-hidden' in discarded_classes: + kept_node['classes'] = [c for c in kept_node['classes'] + if c != 'coqtop-hidden'] + + def merge_consecutive_coqtop_blocks(self): + """Merge consecutive divs wrapping lists of Coq sentences; keep ‘dl’s separate.""" + for node in self.document.traverse(CoqtopBlocksTransform.is_coqtop_block): + if node.parent: + for sibling in node.traverse(include_self=False, descend=False, + siblings=True, ascend=False): + if CoqtopBlocksTransform.is_coqtop_block(sibling): + self.merge_coqtop_classes(node, sibling) + node.extend(sibling.children) + node.parent.remove(sibling) + sibling.parent = None + else: + break + + def apply(self): + self.add_coqtop_output() + self.merge_consecutive_coqtop_blocks() + +class CoqSubdomainsIndex(Index): + """Index subclass to provide subdomain-specific indices. + + Just as in the original manual, we want to have separate indices for each + Coq subdomain (tactics, commands, options, etc)""" + + name, localname, shortname, subdomains = None, None, None, None # Must be overwritten + + def generate(self, docnames=None): + content = defaultdict(list) + items = chain(*(self.domain.data['objects'][subdomain].items() + for subdomain in self.subdomains)) + + for itemname, (docname, _, anchor) in sorted(items, key=lambda x: x[0].lower()): + if docnames and docname not in docnames: + continue + + entries = content[itemname[0].lower()] + entries.append([itemname, 0, docname, anchor, '', '', '']) + + collapse = False + content = sorted(content.items()) + return content, collapse + +class CoqVernacIndex(CoqSubdomainsIndex): + name, localname, shortname, subdomains = "cmdindex", "Command Index", "commands", ["cmd"] + +class CoqTacticIndex(CoqSubdomainsIndex): + name, localname, shortname, subdomains = "tacindex", "Tactic Index", "tactics", ["tac", "tacn"] + +class CoqOptionIndex(CoqSubdomainsIndex): + name, localname, shortname, subdomains = "optindex", "Option Index", "options", ["opt"] + +class CoqGallinaIndex(CoqSubdomainsIndex): + name, localname, shortname, subdomains = "thmindex", "Gallina Index", "theorems", ["thm"] + +class CoqExceptionIndex(CoqSubdomainsIndex): + name, localname, shortname, subdomains = "exnindex", "Error Index", "errors", ["exn"] + +class CoqWarningIndex(CoqSubdomainsIndex): + name, localname, shortname, subdomains = "warnindex", "Warning Index", "warnings", ["warn"] + +class IndexXRefRole(XRefRole): + """A link to one of our domain-specific indices.""" + lowercase = True, + innernodeclass = nodes.inline + warn_dangling = True + + def process_link(self, env, refnode, has_explicit_title, title, target): + if not has_explicit_title: + index = CoqDomain.find_index_by_name(target) + if index: + title = index.localname + return title, target + +def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, content=[]): + """An inline role to declare grammar productions that are not in fact included + in a `productionlist` directive. + + Useful to informally introduce a production, as part of running text + """ + #pylint: disable=dangerous-default-value, unused-argument + env = inliner.document.settings.env + targetid = 'grammar-token-{}'.format(text) + target = nodes.target('', '', ids=[targetid]) + inliner.document.note_explicit_target(target) + code = nodes.literal(rawtext, text, role=typ.lower()) + node = nodes.inline(rawtext, '', target, code, classes=['inline-grammar-production']) + set_role_source_info(inliner, lineno, node) + env.domaindata['std']['objects']['token', text] = env.docname, targetid + return [node], [] + +class CoqDomain(Domain): + """A domain to document Coq code. + + Sphinx has a notion of “domains”, used to tailor it to a specific language. + Domains mostly consist in descriptions of the objects that we wish to + describe (for Coq, this includes tactics, tactic notations, options, + exceptions, etc.), as well as domain-specific roles and directives. + + Each domain is responsible for tracking its objects, and resolving + references to them. In the case of Coq, this leads us to define Coq + “subdomains”, which classify objects into categories in which names must be + unique. For example, a tactic and a theorem may share a name, but two + tactics cannot be named the same. + """ + + name = 'coq' + label = 'Coq' + + object_types = { + # ObjType (= directive type) → (Local name, *xref-roles) + 'cmd': ObjType('cmd', 'cmd'), + 'cmdv': ObjType('cmdv', 'cmd'), + 'tac': ObjType('tac', 'tac'), + 'tacn': ObjType('tacn', 'tacn'), + 'tacv': ObjType('tacv', 'tacn'), + 'opt': ObjType('opt', 'opt'), + 'thm': ObjType('thm', 'thm'), + 'exn': ObjType('exn', 'exn'), + 'warn': ObjType('warn', 'warn'), + 'index': ObjType('index', 'index', searchprio=-1) + } + + directives = { + # Note that some directives live in the same semantic subdomain; ie + # there's one directive per object type, but some object types map to + # the same role. + 'cmd': VernacObject, + 'cmdv': VernacVariantObject, + 'tac': TacticObject, + 'tacn': TacticNotationObject, + 'tacv': TacticNotationVariantObject, + 'opt': OptionObject, + 'thm': GallinaObject, + 'exn': ExceptionObject, + 'warn': WarningObject, + } + + roles = { + # Each of these roles lives in a different semantic “subdomain” + 'cmd': XRefRole(), + 'tac': XRefRole(), + 'tacn': XRefRole(), + 'opt': XRefRole(), + 'thm': XRefRole(), + 'exn': XRefRole(), + 'warn': XRefRole(), + # This one is special + 'index': IndexXRefRole(), + # These are used for highlighting + 'notation': NotationRole, + 'gallina': GallinaRole, + 'ltac': LtacRole, + 'n': NotationRole, + 'g': GallinaRole, + 'l': LtacRole, #FIXME unused? + } + + indices = [CoqVernacIndex, CoqTacticIndex, CoqOptionIndex, CoqGallinaIndex, CoqExceptionIndex, CoqWarningIndex] + + data_version = 1 + initial_data = { + # Collect everything under a key that we control, since Sphinx adds + # others, such as “version” + 'objects' : { # subdomain → name → docname, objtype, targetid + 'cmd': {}, + 'tac': {}, + 'tacn': {}, + 'opt': {}, + 'thm': {}, + 'exn': {}, + 'warn': {}, + } + } + + @staticmethod + def find_index_by_name(targetid): + for index in CoqDomain.indices: + if index.name == targetid: + return index + + def get_objects(self): + # Used for searching and object inventories (intersphinx) + for _, objects in self.data['objects'].items(): + for name, (docname, objtype, targetid) in objects.items(): + yield (name, name, objtype, docname, targetid, self.object_types[objtype].attrs['searchprio']) + for index in self.indices: + yield (index.name, index.localname, 'index', "coq-" + index.name, '', -1) + + def merge_domaindata(self, docnames, otherdata): + DUP = "Duplicate declaration: '{}' also defined in '{}'.\n" + for subdomain, their_objects in otherdata['objects'].items(): + our_objects = self.data['objects'][subdomain] + for name, (docname, objtype, targetid) in their_objects.items(): + if docname in docnames: + if name in our_objects: + self.env.warn(docname, DUP.format(name, our_objects[name][0])) + our_objects[name] = (docname, objtype, targetid) + + def resolve_xref(self, env, fromdocname, builder, role, targetname, node, contnode): + # ‘target’ is the name that was written in the document + # ‘role’ is where this xref comes from; it's exactly one of our subdomains + if role == 'index': + index = CoqDomain.find_index_by_name(targetname) + if index: + return make_refnode(builder, fromdocname, "coq-" + index.name, '', contnode, index.localname) + else: + resolved = self.data['objects'][role].get(targetname) + if resolved: + (todocname, _, targetid) = resolved + return make_refnode(builder, fromdocname, todocname, targetid, contnode, targetname) + + def clear_doc(self, docname_to_clear): + for subdomain_objects in self.data['objects'].values(): + for name, (docname, _, _) in list(subdomain_objects.items()): + if docname == docname_to_clear: + del subdomain_objects[name] + +def is_coqtop_or_coqdoc_block(node): + return (isinstance(node, nodes.Element) and + ('coqtop' in node['classes'] or 'coqdoc' in node['classes'])) + +def simplify_source_code_blocks_for_latex(app, doctree, fromdocname): # pylint: disable=unused-argument + """Simplify coqdoc and coqtop blocks. + + In HTML mode, this does nothing; in other formats, such as LaTeX, it + replaces coqdoc and coqtop blocks by plain text sources, which will use + pygments if available. This prevents the LaTeX builder from getting + confused. + """ + + is_html = app.builder.tags.has("html") + for node in doctree.traverse(is_coqtop_or_coqdoc_block): + if is_html: + node.rawsource = '' # Prevent pygments from kicking in + else: + if 'coqtop-hidden' in node['classes']: + node.parent.remove(node) + else: + node.replace_self(nodes.literal_block(node.rawsource, node.rawsource, language="Coq")) + +def setup(app): + """Register the Coq domain""" + + # A few sanity checks: + subdomains = set(obj.subdomain for obj in CoqDomain.directives.values()) + assert subdomains == set(chain(*(idx.subdomains for idx in CoqDomain.indices))) + assert subdomains.issubset(CoqDomain.roles.keys()) + + # Add domain, directives, and roles + app.add_domain(CoqDomain) + app.add_role("production", GrammarProductionRole) + app.add_directive("coqtop", CoqtopDirective) + app.add_directive("coqdoc", CoqdocDirective) + app.add_directive("example", ExampleDirective) + app.add_directive("inference", InferenceDirective) + app.add_directive("preamble", PreambleDirective) + app.add_transform(CoqtopBlocksTransform) + app.connect('doctree-resolved', simplify_source_code_blocks_for_latex) + + # Add extra styles + app.add_stylesheet("ansi.css") + app.add_stylesheet("coqdoc.css") + app.add_javascript("notations.js") + app.add_stylesheet("notations.css") + app.add_stylesheet("pre-text.css") + + return {'version': '0.1', "parallel_read_safe": True} diff --git a/doc/tools/coqrst/notations/Makefile b/doc/tools/coqrst/notations/Makefile new file mode 100644 index 000000000..c017aed95 --- /dev/null +++ b/doc/tools/coqrst/notations/Makefile @@ -0,0 +1,27 @@ +########################################################################## +## # 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) ## +########################################################################## +# Parsing compact tactic notation syntax in + +TEST_INPUT="unfold {+, @qualid|@string at {+, num}}" + +python: + antlr4 -Dlanguage=Python3 -visitor -no-listener TacticNotations.g + +java: + antlr4 -Dlanguage=Java TacticNotations.g && javac TacticNotations*.java + +test: java + grun TacticNotations top -tree <<< "$(TEST_INPUT)" + +gui: java + grun TacticNotations top -gui <<< "$(TEST_INPUT)" + +sample: + cd ..; python3 -m coqnotations.driver < ../tests/tactics > ../tests/antlr-notations.html diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g new file mode 100644 index 000000000..72ae8eb6b --- /dev/null +++ b/doc/tools/coqrst/notations/TacticNotations.g @@ -0,0 +1,30 @@ +/************************************************************************/ +/* * 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) */ +/************************************************************************/ +grammar TacticNotations; + +// Terminals are not visited, so we add non-terminals for each terminal that +// needs rendering (in particular whitespace (kept in output) vs. WHITESPACE +// (discarded)). + +top: blocks EOF; +blocks: block ((whitespace)? block)*; +block: atomic | hole | repeat | curlies; +repeat: LGROUP (ATOM)? WHITESPACE blocks (WHITESPACE)? RBRACE; +curlies: LBRACE (whitespace)? blocks (whitespace)? RBRACE; +whitespace: WHITESPACE; +atomic: ATOM; +hole: ID; + +LGROUP: '{' [+*?]; +LBRACE: '{'; +RBRACE: '}'; +ATOM: ~[@{} ]+; +ID: '@' [a-zA-Z0-9_]+; +WHITESPACE: ' '+; diff --git a/doc/tools/coqrst/notations/TacticNotations.tokens b/doc/tools/coqrst/notations/TacticNotations.tokens new file mode 100644 index 000000000..4d41a3883 --- /dev/null +++ b/doc/tools/coqrst/notations/TacticNotations.tokens @@ -0,0 +1,8 @@ +LGROUP=1 +LBRACE=2 +RBRACE=3 +ATOM=4 +ID=5 +WHITESPACE=6 +'{'=2 +'}'=3 diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.py b/doc/tools/coqrst/notations/TacticNotationsLexer.py new file mode 100644 index 000000000..4cac071ac --- /dev/null +++ b/doc/tools/coqrst/notations/TacticNotationsLexer.py @@ -0,0 +1,60 @@ +# Generated from TacticNotations.g by ANTLR 4.7 +from antlr4 import * +from io import StringIO +from typing.io import TextIO +import sys + + +def serializedATN(): + with StringIO() as buf: + buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\b") + buf.write("&\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7") + buf.write("\3\2\3\2\3\2\3\3\3\3\3\4\3\4\3\5\6\5\30\n\5\r\5\16\5\31") + buf.write("\3\6\3\6\6\6\36\n\6\r\6\16\6\37\3\7\6\7#\n\7\r\7\16\7") + buf.write("$\2\2\b\3\3\5\4\7\5\t\6\13\7\r\b\3\2\5\4\2,-AA\6\2\"\"") + buf.write("BB}}\177\177\6\2\62;C\\aac|\2(\2\3\3\2\2\2\2\5\3\2\2\2") + buf.write("\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2\3\17") + buf.write("\3\2\2\2\5\22\3\2\2\2\7\24\3\2\2\2\t\27\3\2\2\2\13\33") + buf.write("\3\2\2\2\r\"\3\2\2\2\17\20\7}\2\2\20\21\t\2\2\2\21\4\3") + buf.write("\2\2\2\22\23\7}\2\2\23\6\3\2\2\2\24\25\7\177\2\2\25\b") + buf.write("\3\2\2\2\26\30\n\3\2\2\27\26\3\2\2\2\30\31\3\2\2\2\31") + buf.write("\27\3\2\2\2\31\32\3\2\2\2\32\n\3\2\2\2\33\35\7B\2\2\34") + buf.write("\36\t\4\2\2\35\34\3\2\2\2\36\37\3\2\2\2\37\35\3\2\2\2") + buf.write("\37 \3\2\2\2 \f\3\2\2\2!#\7\"\2\2\"!\3\2\2\2#$\3\2\2\2") + buf.write("$\"\3\2\2\2$%\3\2\2\2%\16\3\2\2\2\6\2\31\37$\2") + return buf.getvalue() + + +class TacticNotationsLexer(Lexer): + + atn = ATNDeserializer().deserialize(serializedATN()) + + decisionsToDFA = [ DFA(ds, i) for i, ds in enumerate(atn.decisionToState) ] + + LGROUP = 1 + LBRACE = 2 + RBRACE = 3 + ATOM = 4 + ID = 5 + WHITESPACE = 6 + + channelNames = [ u"DEFAULT_TOKEN_CHANNEL", u"HIDDEN" ] + + modeNames = [ "DEFAULT_MODE" ] + + literalNames = [ "<INVALID>", + "'{'", "'}'" ] + + symbolicNames = [ "<INVALID>", + "LGROUP", "LBRACE", "RBRACE", "ATOM", "ID", "WHITESPACE" ] + + ruleNames = [ "LGROUP", "LBRACE", "RBRACE", "ATOM", "ID", "WHITESPACE" ] + + grammarFileName = "TacticNotations.g" + + def __init__(self, input=None, output:TextIO = sys.stdout): + super().__init__(input, output) + self.checkVersion("4.7") + self._interp = LexerATNSimulator(self, self.atn, self.decisionsToDFA, PredictionContextCache()) + self._actions = None + self._predicates = None diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens new file mode 100644 index 000000000..4d41a3883 --- /dev/null +++ b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens @@ -0,0 +1,8 @@ +LGROUP=1 +LBRACE=2 +RBRACE=3 +ATOM=4 +ID=5 +WHITESPACE=6 +'{'=2 +'}'=3 diff --git a/doc/tools/coqrst/notations/TacticNotationsParser.py b/doc/tools/coqrst/notations/TacticNotationsParser.py new file mode 100644 index 000000000..357902ddb --- /dev/null +++ b/doc/tools/coqrst/notations/TacticNotationsParser.py @@ -0,0 +1,519 @@ +# Generated from TacticNotations.g by ANTLR 4.7 +# encoding: utf-8 +from antlr4 import * +from io import StringIO +from typing.io import TextIO +import sys + +def serializedATN(): + with StringIO() as buf: + buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\b") + buf.write("A\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7\4\b") + buf.write("\t\b\4\t\t\t\3\2\3\2\3\2\3\3\3\3\5\3\30\n\3\3\3\7\3\33") + buf.write("\n\3\f\3\16\3\36\13\3\3\4\3\4\3\4\3\4\5\4$\n\4\3\5\3\5") + buf.write("\5\5(\n\5\3\5\3\5\3\5\5\5-\n\5\3\5\3\5\3\6\3\6\5\6\63") + buf.write("\n\6\3\6\3\6\5\6\67\n\6\3\6\3\6\3\7\3\7\3\b\3\b\3\t\3") + buf.write("\t\3\t\2\2\n\2\4\6\b\n\f\16\20\2\2\2A\2\22\3\2\2\2\4\25") + buf.write("\3\2\2\2\6#\3\2\2\2\b%\3\2\2\2\n\60\3\2\2\2\f:\3\2\2\2") + buf.write("\16<\3\2\2\2\20>\3\2\2\2\22\23\5\4\3\2\23\24\7\2\2\3\24") + buf.write("\3\3\2\2\2\25\34\5\6\4\2\26\30\5\f\7\2\27\26\3\2\2\2\27") + buf.write("\30\3\2\2\2\30\31\3\2\2\2\31\33\5\6\4\2\32\27\3\2\2\2") + buf.write("\33\36\3\2\2\2\34\32\3\2\2\2\34\35\3\2\2\2\35\5\3\2\2") + buf.write("\2\36\34\3\2\2\2\37$\5\16\b\2 $\5\20\t\2!$\5\b\5\2\"$") + buf.write("\5\n\6\2#\37\3\2\2\2# \3\2\2\2#!\3\2\2\2#\"\3\2\2\2$\7") + buf.write("\3\2\2\2%\'\7\3\2\2&(\7\6\2\2\'&\3\2\2\2\'(\3\2\2\2()") + buf.write("\3\2\2\2)*\7\b\2\2*,\5\4\3\2+-\7\b\2\2,+\3\2\2\2,-\3\2") + buf.write("\2\2-.\3\2\2\2./\7\5\2\2/\t\3\2\2\2\60\62\7\4\2\2\61\63") + buf.write("\5\f\7\2\62\61\3\2\2\2\62\63\3\2\2\2\63\64\3\2\2\2\64") + buf.write("\66\5\4\3\2\65\67\5\f\7\2\66\65\3\2\2\2\66\67\3\2\2\2") + buf.write("\678\3\2\2\289\7\5\2\29\13\3\2\2\2:;\7\b\2\2;\r\3\2\2") + buf.write("\2<=\7\6\2\2=\17\3\2\2\2>?\7\7\2\2?\21\3\2\2\2\t\27\34") + buf.write("#\',\62\66") + return buf.getvalue() + + +class TacticNotationsParser ( Parser ): + + grammarFileName = "TacticNotations.g" + + atn = ATNDeserializer().deserialize(serializedATN()) + + decisionsToDFA = [ DFA(ds, i) for i, ds in enumerate(atn.decisionToState) ] + + sharedContextCache = PredictionContextCache() + + literalNames = [ "<INVALID>", "<INVALID>", "'{'", "'}'" ] + + symbolicNames = [ "<INVALID>", "LGROUP", "LBRACE", "RBRACE", "ATOM", + "ID", "WHITESPACE" ] + + RULE_top = 0 + RULE_blocks = 1 + RULE_block = 2 + RULE_repeat = 3 + RULE_curlies = 4 + RULE_whitespace = 5 + RULE_atomic = 6 + RULE_hole = 7 + + ruleNames = [ "top", "blocks", "block", "repeat", "curlies", "whitespace", + "atomic", "hole" ] + + EOF = Token.EOF + LGROUP=1 + LBRACE=2 + RBRACE=3 + ATOM=4 + ID=5 + WHITESPACE=6 + + def __init__(self, input:TokenStream, output:TextIO = sys.stdout): + super().__init__(input, output) + self.checkVersion("4.7") + self._interp = ParserATNSimulator(self, self.atn, self.decisionsToDFA, self.sharedContextCache) + self._predicates = None + + + + class TopContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def blocks(self): + return self.getTypedRuleContext(TacticNotationsParser.BlocksContext,0) + + + def EOF(self): + return self.getToken(TacticNotationsParser.EOF, 0) + + def getRuleIndex(self): + return TacticNotationsParser.RULE_top + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitTop" ): + return visitor.visitTop(self) + else: + return visitor.visitChildren(self) + + + + + def top(self): + + localctx = TacticNotationsParser.TopContext(self, self._ctx, self.state) + self.enterRule(localctx, 0, self.RULE_top) + try: + self.enterOuterAlt(localctx, 1) + self.state = 16 + self.blocks() + self.state = 17 + self.match(TacticNotationsParser.EOF) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + class BlocksContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def block(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(TacticNotationsParser.BlockContext) + else: + return self.getTypedRuleContext(TacticNotationsParser.BlockContext,i) + + + def whitespace(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(TacticNotationsParser.WhitespaceContext) + else: + return self.getTypedRuleContext(TacticNotationsParser.WhitespaceContext,i) + + + def getRuleIndex(self): + return TacticNotationsParser.RULE_blocks + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitBlocks" ): + return visitor.visitBlocks(self) + else: + return visitor.visitChildren(self) + + + + + def blocks(self): + + localctx = TacticNotationsParser.BlocksContext(self, self._ctx, self.state) + self.enterRule(localctx, 2, self.RULE_blocks) + self._la = 0 # Token type + try: + self.enterOuterAlt(localctx, 1) + self.state = 19 + self.block() + self.state = 26 + self._errHandler.sync(self) + _alt = self._interp.adaptivePredict(self._input,1,self._ctx) + while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER: + if _alt==1: + self.state = 21 + self._errHandler.sync(self) + _la = self._input.LA(1) + if _la==TacticNotationsParser.WHITESPACE: + self.state = 20 + self.whitespace() + + + self.state = 23 + self.block() + self.state = 28 + self._errHandler.sync(self) + _alt = self._interp.adaptivePredict(self._input,1,self._ctx) + + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + class BlockContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def atomic(self): + return self.getTypedRuleContext(TacticNotationsParser.AtomicContext,0) + + + def hole(self): + return self.getTypedRuleContext(TacticNotationsParser.HoleContext,0) + + + def repeat(self): + return self.getTypedRuleContext(TacticNotationsParser.RepeatContext,0) + + + def curlies(self): + return self.getTypedRuleContext(TacticNotationsParser.CurliesContext,0) + + + def getRuleIndex(self): + return TacticNotationsParser.RULE_block + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitBlock" ): + return visitor.visitBlock(self) + else: + return visitor.visitChildren(self) + + + + + def block(self): + + localctx = TacticNotationsParser.BlockContext(self, self._ctx, self.state) + self.enterRule(localctx, 4, self.RULE_block) + try: + self.state = 33 + self._errHandler.sync(self) + token = self._input.LA(1) + if token in [TacticNotationsParser.ATOM]: + self.enterOuterAlt(localctx, 1) + self.state = 29 + self.atomic() + pass + elif token in [TacticNotationsParser.ID]: + self.enterOuterAlt(localctx, 2) + self.state = 30 + self.hole() + pass + elif token in [TacticNotationsParser.LGROUP]: + self.enterOuterAlt(localctx, 3) + self.state = 31 + self.repeat() + pass + elif token in [TacticNotationsParser.LBRACE]: + self.enterOuterAlt(localctx, 4) + self.state = 32 + self.curlies() + pass + else: + raise NoViableAltException(self) + + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + class RepeatContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def LGROUP(self): + return self.getToken(TacticNotationsParser.LGROUP, 0) + + def WHITESPACE(self, i:int=None): + if i is None: + return self.getTokens(TacticNotationsParser.WHITESPACE) + else: + return self.getToken(TacticNotationsParser.WHITESPACE, i) + + def blocks(self): + return self.getTypedRuleContext(TacticNotationsParser.BlocksContext,0) + + + def RBRACE(self): + return self.getToken(TacticNotationsParser.RBRACE, 0) + + def ATOM(self): + return self.getToken(TacticNotationsParser.ATOM, 0) + + def getRuleIndex(self): + return TacticNotationsParser.RULE_repeat + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitRepeat" ): + return visitor.visitRepeat(self) + else: + return visitor.visitChildren(self) + + + + + def repeat(self): + + localctx = TacticNotationsParser.RepeatContext(self, self._ctx, self.state) + self.enterRule(localctx, 6, self.RULE_repeat) + self._la = 0 # Token type + try: + self.enterOuterAlt(localctx, 1) + self.state = 35 + self.match(TacticNotationsParser.LGROUP) + self.state = 37 + self._errHandler.sync(self) + _la = self._input.LA(1) + if _la==TacticNotationsParser.ATOM: + self.state = 36 + self.match(TacticNotationsParser.ATOM) + + + self.state = 39 + self.match(TacticNotationsParser.WHITESPACE) + self.state = 40 + self.blocks() + self.state = 42 + self._errHandler.sync(self) + _la = self._input.LA(1) + if _la==TacticNotationsParser.WHITESPACE: + self.state = 41 + self.match(TacticNotationsParser.WHITESPACE) + + + self.state = 44 + self.match(TacticNotationsParser.RBRACE) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + class CurliesContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def LBRACE(self): + return self.getToken(TacticNotationsParser.LBRACE, 0) + + def blocks(self): + return self.getTypedRuleContext(TacticNotationsParser.BlocksContext,0) + + + def RBRACE(self): + return self.getToken(TacticNotationsParser.RBRACE, 0) + + def whitespace(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(TacticNotationsParser.WhitespaceContext) + else: + return self.getTypedRuleContext(TacticNotationsParser.WhitespaceContext,i) + + + def getRuleIndex(self): + return TacticNotationsParser.RULE_curlies + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitCurlies" ): + return visitor.visitCurlies(self) + else: + return visitor.visitChildren(self) + + + + + def curlies(self): + + localctx = TacticNotationsParser.CurliesContext(self, self._ctx, self.state) + self.enterRule(localctx, 8, self.RULE_curlies) + self._la = 0 # Token type + try: + self.enterOuterAlt(localctx, 1) + self.state = 46 + self.match(TacticNotationsParser.LBRACE) + self.state = 48 + self._errHandler.sync(self) + _la = self._input.LA(1) + if _la==TacticNotationsParser.WHITESPACE: + self.state = 47 + self.whitespace() + + + self.state = 50 + self.blocks() + self.state = 52 + self._errHandler.sync(self) + _la = self._input.LA(1) + if _la==TacticNotationsParser.WHITESPACE: + self.state = 51 + self.whitespace() + + + self.state = 54 + self.match(TacticNotationsParser.RBRACE) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + class WhitespaceContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def WHITESPACE(self): + return self.getToken(TacticNotationsParser.WHITESPACE, 0) + + def getRuleIndex(self): + return TacticNotationsParser.RULE_whitespace + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitWhitespace" ): + return visitor.visitWhitespace(self) + else: + return visitor.visitChildren(self) + + + + + def whitespace(self): + + localctx = TacticNotationsParser.WhitespaceContext(self, self._ctx, self.state) + self.enterRule(localctx, 10, self.RULE_whitespace) + try: + self.enterOuterAlt(localctx, 1) + self.state = 56 + self.match(TacticNotationsParser.WHITESPACE) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + class AtomicContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def ATOM(self): + return self.getToken(TacticNotationsParser.ATOM, 0) + + def getRuleIndex(self): + return TacticNotationsParser.RULE_atomic + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitAtomic" ): + return visitor.visitAtomic(self) + else: + return visitor.visitChildren(self) + + + + + def atomic(self): + + localctx = TacticNotationsParser.AtomicContext(self, self._ctx, self.state) + self.enterRule(localctx, 12, self.RULE_atomic) + try: + self.enterOuterAlt(localctx, 1) + self.state = 58 + self.match(TacticNotationsParser.ATOM) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + class HoleContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def ID(self): + return self.getToken(TacticNotationsParser.ID, 0) + + def getRuleIndex(self): + return TacticNotationsParser.RULE_hole + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitHole" ): + return visitor.visitHole(self) + else: + return visitor.visitChildren(self) + + + + + def hole(self): + + localctx = TacticNotationsParser.HoleContext(self, self._ctx, self.state) + self.enterRule(localctx, 14, self.RULE_hole) + try: + self.enterOuterAlt(localctx, 1) + self.state = 60 + self.match(TacticNotationsParser.ID) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx diff --git a/doc/tools/coqrst/notations/TacticNotationsVisitor.py b/doc/tools/coqrst/notations/TacticNotationsVisitor.py new file mode 100644 index 000000000..80e69d433 --- /dev/null +++ b/doc/tools/coqrst/notations/TacticNotationsVisitor.py @@ -0,0 +1,53 @@ +# Generated from TacticNotations.g by ANTLR 4.7 +from antlr4 import * +if __name__ is not None and "." in __name__: + from .TacticNotationsParser import TacticNotationsParser +else: + from TacticNotationsParser import TacticNotationsParser + +# This class defines a complete generic visitor for a parse tree produced by TacticNotationsParser. + +class TacticNotationsVisitor(ParseTreeVisitor): + + # Visit a parse tree produced by TacticNotationsParser#top. + def visitTop(self, ctx:TacticNotationsParser.TopContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by TacticNotationsParser#blocks. + def visitBlocks(self, ctx:TacticNotationsParser.BlocksContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by TacticNotationsParser#block. + def visitBlock(self, ctx:TacticNotationsParser.BlockContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by TacticNotationsParser#repeat. + def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by TacticNotationsParser#curlies. + def visitCurlies(self, ctx:TacticNotationsParser.CurliesContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by TacticNotationsParser#whitespace. + def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by TacticNotationsParser#atomic. + def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by TacticNotationsParser#hole. + def visitHole(self, ctx:TacticNotationsParser.HoleContext): + return self.visitChildren(ctx) + + + +del TacticNotationsParser
\ No newline at end of file diff --git a/doc/tools/coqrst/notations/UbuntuMono-B.ttf b/doc/tools/coqrst/notations/UbuntuMono-B.ttf Binary files differnew file mode 100644 index 000000000..7bd666576 --- /dev/null +++ b/doc/tools/coqrst/notations/UbuntuMono-B.ttf diff --git a/doc/tools/coqrst/notations/UbuntuMono-Square.ttf b/doc/tools/coqrst/notations/UbuntuMono-Square.ttf Binary files differnew file mode 100644 index 000000000..a53a9a0f0 --- /dev/null +++ b/doc/tools/coqrst/notations/UbuntuMono-Square.ttf diff --git a/doc/tools/coqrst/notations/__init__.py b/doc/tools/coqrst/notations/__init__.py new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/doc/tools/coqrst/notations/__init__.py diff --git a/doc/tools/coqrst/notations/fontsupport.py b/doc/tools/coqrst/notations/fontsupport.py new file mode 100755 index 000000000..3402ea2aa --- /dev/null +++ b/doc/tools/coqrst/notations/fontsupport.py @@ -0,0 +1,81 @@ +#!/usr/bin/env python2 +# -*- coding: utf-8 -*- +########################################################################## +## # 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) ## +########################################################################## +"""Transform a font to center each of its characters in square bounding boxes. + +See https://stackoverflow.com/questions/37377476/ for background information. +""" + +from collections import Counter + +try: + import fontforge + import psMat +except ImportError: + print("This program requires FontForge's python bindings:") + print(" git clone https://github.com/fontforge/fontforge") + print(" cd fontforge") + print(" ./bootstrap") + print(" ./configure") + print(" make -j8") + print(" sudo make install") + raise + +def glyph_height(glyph): + _, ylo, _, yhi = glyph.boundingBox() + return yhi - ylo + +def scale_single_glyph(glyph, width, height): + """Center glyph in a box of size width*height""" + # Some glyphs (such as ‘;’) contain references (‘.’ + ‘,’), and moving the + # referenced glyphs moves them in all glyphs that reference them. + # Unlinking copies references into this glyph + glyph.unlinkThisGlyph() + # Width + deltaw = width - glyph.width + glyph.left_side_bearing += deltaw / 2 + glyph.right_side_bearing += deltaw - glyph.left_side_bearing + glyph.width = width + # Height + ylo = glyph.boundingBox()[1] + deltah = height - glyph_height(glyph) + glyph.transform(psMat.translate(0, deltah / 2.0 - ylo)) + +def avg(lst): + lst = list(lst) + return sum(lst) / float(len(lst)) + +def trim_font(fnt): + """Remove characters codes beyond 191 front fnt""" + for g in fnt.glyphs(): + if g.unicode >= 191: + fnt.removeGlyph(g) + return fnt + +def center_glyphs(src_font_path, dst_font_path, dst_name): + fnt = trim_font(fontforge.open(src_font_path)) + + size = max(max(g.width for g in fnt.glyphs()), + max(glyph_height(g) for g in fnt.glyphs())) + fnt.ascent, fnt.descent = size, 0 + for glyph in fnt.glyphs(): + scale_single_glyph(glyph, size, size) + + fnt.sfnt_names = [] + fnt.fontname = fnt.familyname = fnt.fullname = dst_name + fnt.generate(dst_font_path) + +if __name__ == '__main__': + from os.path import dirname, join, abspath + curdir = dirname(abspath(__file__)) + ubuntumono_path = join(curdir, "UbuntuMono-B.ttf") + ubuntumono_mod_path = join(curdir, "UbuntuMono-Square.ttf") + center_glyphs(ubuntumono_path, ubuntumono_mod_path, "UbuntuMono-Square") diff --git a/doc/tools/coqrst/notations/html.py b/doc/tools/coqrst/notations/html.py new file mode 100644 index 000000000..d91bbb64c --- /dev/null +++ b/doc/tools/coqrst/notations/html.py @@ -0,0 +1,65 @@ +########################################################################## +## # 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) ## +########################################################################## +"""A visitor for ANTLR notation ASTs, producing raw HTML. + +Uses the dominate package. +""" + +from dominate import tags + +from .parsing import parse +from .TacticNotationsParser import TacticNotationsParser +from .TacticNotationsVisitor import TacticNotationsVisitor + +class TacticNotationsToHTMLVisitor(TacticNotationsVisitor): + def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext): + with tags.span(_class="repeat-wrapper"): + with tags.span(_class="repeat"): + self.visitChildren(ctx) + repeat_marker = ctx.LGROUP().getText()[1] + separator = ctx.ATOM() + tags.sup(repeat_marker) + if separator: + tags.sub(separator.getText()) + + def visitCurlies(self, ctx:TacticNotationsParser.CurliesContext): + sp = tags.span(_class="curlies") + sp.add("{") + with sp: + self.visitChildren(ctx) + sp.add("}") + + def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext): + tags.span(ctx.ATOM().getText()) + + def visitHole(self, ctx:TacticNotationsParser.HoleContext): + tags.span(ctx.ID().getText()[1:], _class="hole") + + def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): + tags.span(" ") # TODO: no need for a <span> here + +def htmlize(notation): + """Translate notation to a dominate HTML tree""" + top = tags.span(_class='notation') + with top: + TacticNotationsToHTMLVisitor().visit(parse(notation)) + return top + +def htmlize_str(notation): + """Translate notation to a raw HTML document""" + # ‘pretty=True’ introduces spurious spaces + return htmlize(notation).render(pretty=False) + +def htmlize_p(notation): + """Like `htmlize`, wrapped in a ‘p’. + Does not return: instead, must be run in a dominate context. + """ + with tags.p(): + htmlize(notation) diff --git a/doc/tools/coqrst/notations/parsing.py b/doc/tools/coqrst/notations/parsing.py new file mode 100644 index 000000000..73be6f26e --- /dev/null +++ b/doc/tools/coqrst/notations/parsing.py @@ -0,0 +1,37 @@ +########################################################################## +## # 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) ## +########################################################################## +from .TacticNotationsLexer import TacticNotationsLexer +from .TacticNotationsParser import TacticNotationsParser + +from antlr4 import CommonTokenStream, InputStream + +SUBSTITUTIONS = [("@bindings_list", "{+ (@id := @val) }"), + ("@qualid_or_string", "@id|@string")] + +def substitute(notation): + """Perform common substitutions in the notation string. + + Nested notations quickly became unwieldy in the original ‘…’-based format, + so they were avoided and replaced by pointers to grammar rules. With the + new format, it's usually nicer to remove the indirection. + """ + for (src, dst) in SUBSTITUTIONS: + notation = notation.replace(src, dst) + return notation + +def parse(notation): + """Parse a notation string. + + :return: An ANTLR AST. Use one of the supplied visitors (or write your own) + to turn it into useful output. + """ + substituted = substitute(notation) + lexer = TacticNotationsLexer(InputStream(substituted)) + return TacticNotationsParser(CommonTokenStream(lexer)).top() diff --git a/doc/tools/coqrst/notations/plain.py b/doc/tools/coqrst/notations/plain.py new file mode 100644 index 000000000..5d4501892 --- /dev/null +++ b/doc/tools/coqrst/notations/plain.py @@ -0,0 +1,50 @@ +########################################################################## +## # 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) ## +########################################################################## +"""A visitor for ANTLR notation ASTs, producing plain text with ellipses. + +Somewhat-closely approximates the rendering of the original manual. +""" + +from io import StringIO + +from .parsing import parse +from .TacticNotationsParser import TacticNotationsParser +from .TacticNotationsVisitor import TacticNotationsVisitor + +class TacticNotationsToDotsVisitor(TacticNotationsVisitor): + def __init__(self): + self.buffer = StringIO() + + def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext): + separator = ctx.ATOM() + self.visitChildren(ctx) + if ctx.LGROUP().getText()[1] == "+": + spacer = (separator.getText() + " " if separator else "") + self.buffer.write(spacer + "…" + spacer) + self.visitChildren(ctx) + + def visitCurlies(self, ctx:TacticNotationsParser.CurliesContext): + self.buffer.write("{") + self.visitChildren(ctx) + self.buffer.write("}") + + def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext): + self.buffer.write(ctx.ATOM().getText()) + + def visitHole(self, ctx:TacticNotationsParser.HoleContext): + self.buffer.write("‘{}’".format(ctx.ID().getText()[1:])) + + def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): + self.buffer.write(" ") + +def stringify_with_ellipses(notation): + vs = TacticNotationsToDotsVisitor() + vs.visit(parse(notation)) + return vs.buffer.getvalue() diff --git a/doc/tools/coqrst/notations/regexp.py b/doc/tools/coqrst/notations/regexp.py new file mode 100644 index 000000000..cac6aaecb --- /dev/null +++ b/doc/tools/coqrst/notations/regexp.py @@ -0,0 +1,57 @@ +########################################################################## +## # 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) ## +########################################################################## +"""An experimental visitor for ANTLR notation ASTs, producing regular expressions.""" + +import re +from io import StringIO + +from .parsing import parse +from .TacticNotationsParser import TacticNotationsParser +from .TacticNotationsVisitor import TacticNotationsVisitor + +class TacticNotationsToRegexpVisitor(TacticNotationsVisitor): + def __init__(self): + self.buffer = StringIO() + + def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext): + separator = ctx.ATOM() + repeat_marker = ctx.LGROUP().getText()[1] + + self.buffer.write("(") + self.visitChildren(ctx) + self.buffer.write(")") + + if repeat_marker in ["?", "*"]: + self.buffer.write("?") + elif repeat_marker in ["+", "*"]: + self.buffer.write("(") + self.buffer.write(r"\s*" + re.escape(separator.getText() if separator else " ") + r"\s*") + self.visitChildren(ctx) + self.buffer.write(")*") + + def visitCurlies(self, ctx:TacticNotationsParser.CurliesContext): + self.buffer.write(r"\{") + self.visitChildren(ctx) + self.buffer.write(r"\}") + + def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext): + self.buffer.write(re.escape(ctx.ATOM().getText())) + + def visitHole(self, ctx:TacticNotationsParser.HoleContext): + self.buffer.write("([^();. \n]+)") # FIXME could allow more things + + def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): + self.buffer.write(r"\s+") + +def regexpify(notation): + """Translate notation to a Python regular expression matching it""" + vs = TacticNotationsToRegexpVisitor() + vs.visit(parse(notation)) + return vs.buffer.getvalue() diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py new file mode 100644 index 000000000..889bf70a4 --- /dev/null +++ b/doc/tools/coqrst/notations/sphinx.py @@ -0,0 +1,77 @@ +########################################################################## +## # 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) ## +########################################################################## +"""A visitor for ANTLR notation ASTs, producing Sphinx nodes. + +Unlike the HTML visitor, this produces Sphinx-friendly nodes that can be used by +all backends. If you just want HTML output, use the HTML visitor. +""" + +from .parsing import parse +from .TacticNotationsParser import TacticNotationsParser +from .TacticNotationsVisitor import TacticNotationsVisitor + +from docutils import nodes +from sphinx import addnodes + +class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): + def defaultResult(self): + return [] + + def aggregateResult(self, aggregate, nextResult): + if nextResult: + aggregate.extend(nextResult) + return aggregate + + def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext): + # Uses inline nodes instead of subscript and superscript to ensure that + # we get the right customization hooks at the LaTeX level + wrapper = nodes.inline('', '', classes=['repeat-wrapper']) + wrapper += nodes.inline('', '', *self.visitChildren(ctx), classes=["repeat"]) + + repeat_marker = ctx.LGROUP().getText()[1] + wrapper += nodes.inline(repeat_marker, repeat_marker, classes=['notation-sup']) + + separator = ctx.ATOM() + if separator: + sep = separator.getText() + wrapper += nodes.inline(sep, sep, classes=['notation-sub']) + + return [wrapper] + + def visitCurlies(self, ctx:TacticNotationsParser.CurliesContext): + sp = nodes.inline('', '', classes=["curlies"]) + sp += nodes.Text("{") + sp.extend(self.visitChildren(ctx)) + sp += nodes.Text("}") + return [sp] + + def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext): + atom = ctx.ATOM().getText() + return [nodes.inline(atom, atom)] + + def visitHole(self, ctx:TacticNotationsParser.HoleContext): + hole = ctx.ID().getText() + token_name = hole[1:] + node = nodes.inline(hole, token_name, classes=["hole"]) + return [addnodes.pending_xref(token_name, node, reftype='token', refdomain='std', reftarget=token_name)] + + def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): + return [nodes.Text(" ")] + +def sphinxify(notation): + """Translate notation into a Sphinx document tree""" + vs = TacticNotationsToSphinxVisitor() + return vs.visit(parse(notation)) + +def main(): + print(sphinxify("a := {+, b {+ c}}")) + +if __name__ == '__main__': + main() diff --git a/doc/tools/coqrst/repl/__init__.py b/doc/tools/coqrst/repl/__init__.py new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/doc/tools/coqrst/repl/__init__.py diff --git a/doc/tools/coqrst/repl/ansicolors.py b/doc/tools/coqrst/repl/ansicolors.py new file mode 100644 index 000000000..495eea910 --- /dev/null +++ b/doc/tools/coqrst/repl/ansicolors.py @@ -0,0 +1,99 @@ +########################################################################## +## # 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) ## +########################################################################## +""" +Parse Coq's ANSI output. +======================== + +Translated to Python from Coq's terminal.ml. +""" + +# pylint: disable=too-many-return-statements, too-many-branches + +def parse_color(style, offset): + color = style[offset] % 10 + if color == 0: + return ("black", 1) + elif color == 1: + return ("red", 1) + elif color == 2: + return ("green", 1) + elif color == 3: + return ("yellow", 1) + elif color == 4: + return ("blue", 1) + elif color == 5: + return ("magenta", 1) + elif color == 6: + return ("cyan", 1) + elif color == 7: + return ("white", 1) + elif color == 9: + return ("default", 1) + elif color == 8: + nxt = style[offset + 1] + if nxt == 5: + return ("index-{}".format(style[offset + 1]), 2) + elif nxt == 2: + return ("rgb-{}-{}-{}".format(*style[offset+1:offset+4]), 4) + else: + raise ValueError("{}, {}".format(style, offset)) + else: + raise ValueError() + +def parse_style(style, offset, acc): + offset = 0 + while offset < len(style): + head = style[offset] + + if head == 0: + acc.append("reset") + elif head == 1: + acc.append("bold") + elif head == 3: + acc.append("italic") + elif head == 4: + acc.append("underline") + elif head == 7: + acc.append("negative") + elif head == 22: + acc.append("no-bold") + elif head == 23: + acc.append("no-italic") + elif head == 24: + acc.append("no-underline") + elif head == 27: + acc.append("no-negative") + else: + color, suboffset = parse_color(style, offset) + offset += suboffset - 1 + if 30 <= head < 40: + acc.append("fg-{}".format(color)) + elif 40 <= head < 50: + acc.append("bg-{}".format(color)) + elif 90 <= head < 100: + acc.append("fg-light-{}".format(color)) + elif 100 <= head < 110: + acc.append("bg-light-{}".format(color)) + + offset += 1 + +def parse_ansi(code): + """Parse an ansi code into a collection of CSS classes. + + :param code: A sequence of ‘;’-separated ANSI codes. Do not include the + leading ‘^[[’ or the final ‘m’ + """ + classes = [] + parse_style([int(c) for c in code.split(';')], 0, classes) + return ["ansi-" + cls for cls in classes] + +if __name__ == '__main__': + # As produced by Coq with ‘Check nat.’ + print(parse_ansi("92;49;22;23;24;27")) diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py new file mode 100644 index 000000000..42a2f9823 --- /dev/null +++ b/doc/tools/coqrst/repl/coqtop.py @@ -0,0 +1,98 @@ +########################################################################## +## # 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) ## +########################################################################## +""" +Drive coqtop with Python! +========================= + +This module is a simple pexpect-based driver for coqtop, based on the old +REPL interface. +""" + +import os +import re + +import pexpect + +class CoqTop: + """Create an instance of coqtop. + + Use this as a context manager: no instance of coqtop is created until + you call `__enter__`. coqtop is terminated when you `__exit__` the + context manager. + + Sentence parsing is very basic for now (a "." in a quoted string will + confuse it). + """ + + COQTOP_PROMPT = re.compile("\r\n[^< ]+ < ") + + def __init__(self, coqtop_bin=None, color=False, args=None) -> str: + """Configure a coqtop instance (but don't start it yet). + + :param coqtop_bin: The path to coqtop; uses $COQBIN by default, falling back to "coqtop" + :param color: When True, tell coqtop to produce ANSI color codes (see + the ansicolors module) + :param args: Additional arugments to coqtop. + """ + self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN'),"coqtop") + self.args = (args or []) + ["-color", "on"] * color + self.coqtop = None + + def __enter__(self): + if self.coqtop: + raise ValueError("This module isn't re-entrant") + self.coqtop = pexpect.spawn(self.coqtop_bin, args=self.args, echo=False, encoding="utf-8") + # Disable delays (http://pexpect.readthedocs.io/en/stable/commonissues.html?highlight=delaybeforesend) + self.coqtop.delaybeforesend = 0 + self.next_prompt() + return self + + def __exit__(self, type, value, traceback): + self.coqtop.kill(9) + + def next_prompt(self): + "Wait for the next coqtop prompt, and return the output preceeding it." + self.coqtop.expect(CoqTop.COQTOP_PROMPT, timeout = 1) + return self.coqtop.before + + def sendone(self, sentence): + """Send a single sentence to coqtop. + + :sentence: One Coq sentence (otherwise, Coqtop will produce multiple + prompts and we'll get confused) + """ + # Suppress newlines, but not spaces: they are significant in notations + sentence = re.sub(r"[\r\n]+", " ", sentence).strip() + # print("Sending {}".format(sentence)) + self.coqtop.sendline(sentence) + output = self.next_prompt() + # print("Got {}".format(repr(output))) + return output + +def sendmany(*sentences): + """A small demo: send each sentence in sentences and print the output""" + with CoqTop() as coqtop: + for sentence in sentences: + print("=====================================") + print(sentence) + print("-------------------------------------") + response = coqtop.sendone(sentence) + print(response) + +def main(): + """Run a simple performance test and demo `sendmany`""" + with CoqTop() as coqtop: + for _ in range(200): + print(repr(coqtop.sendone("Check nat."))) + sendmany("Goal False -> True.", "Proof.", "intros H.", + "Check H.", "Chchc.", "apply I.", "Qed.") + +if __name__ == '__main__': + main() |