aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/coqrst
AgeCommit message (Collapse)Author
2020-01-03[tools] Remove support for python2Emilio Jesus Gallego Arias
Closes #10491 We re-add the header in doc/tools/coqrst/notations/fontsupport.py which was removed by accident in 1a9c769ed363ee2f2784e7252af72e6c1e2fbcc6 The fontsupport script itself has been kept for reference, however it is not involved by any build target as of today.
2019-12-28Prevent apostrophes and backticks from being stylized in latexJim Fehrle
2019-12-28Convert productionlists to prodnsJim Fehrle
2019-12-19Support additional escape sequences in notationsJim Fehrle
2019-12-14Make prodn look more like productionlistJim Fehrle
2019-07-01Update doc for % escapes in Sphinx doc, improve error messagesJim Fehrle
2019-06-17Adapt change-header script to handle shebangs in addition to Emacs comments.Théo Zimmermann
Remove other types of lines before copyright headers.
2019-06-17Update py-style headers to new year.Théo Zimmermann
2019-06-17Update c-style headers to new year.Théo Zimmermann
2019-06-14Add a comment documenting what fontsupport.py is.Théo Zimmermann
2019-05-21Fixing typos - Part 1JPR
2019-05-16[refman] Introduce syntax for alternatives in notationsClément Pit-Claudel
Closes GH-8482.
2019-05-12[refman] Raise an error when a notation doesn't parseClément Pit-Claudel
2019-04-21Remove duplicate copy of _warn_if_duplicate_name.Jim Fehrle
2019-02-28[sphinx] Add warn option to coqtop directive.Théo Zimmermann
By default Coq warnings are made fatal when building the manual. If you want to show a command resulting in a warning, use the warn option. Preexisting warnings are either fixed or marked as expected.
2019-02-20Merge PR #9560: [coqlib] Remove `-boot` option for setting the coqlibEnrico Tassi
Reviewed-by: SkySkimmer Ack-by: ejgallego Reviewed-by: gares
2019-02-19[sphinx] Refactor handling of options for coqtop directive.Théo Zimmermann
Make it mandatory to give exactly one display option.
2019-02-18[sphinx] Add abort and restart options to directive coqtop.Théo Zimmermann
2019-02-18coqdomain.py fix typo in commentGaëtan Gilbert
2019-02-18Sphinx: nicer error reportingGaëtan Gilbert
Example: add this to the first block in canonical-structures.rst: ~~~ Check nat. Check nat nat. ~~~ Output: ~~~ reading sources... [ 2%] addendum/canonical-structures Extension error: /home/gaetan/dev/coq/coq/doc/sphinx/addendum/canonical-structures.rst:43: Error while sending the following to coqtop: Check nat nat. coqtop output: Toplevel input, characters 6-13: > Check nat nat. > ^^^^^^^ Error: Illegal application (Non-functional construction): The expression "nat" of type "Set" cannot be applied to the term "nat" : "Set" Full error text: End Of File (EOF). Exception style platform. <pexpect.pty_spawn.spawn object at 0x7fc8c8b1bc18> command: /home/gaetan/dev/coq/coq/bin/coqtop args: [b'/home/gaetan/dev/coq/coq/bin/coqtop', b'-boot', b'-color', b'on'] buffer (last 100 chars): '' before (last 100 chars): 'xpression "nat" of type "\x1b[33;1mSet\x1b[0m"\r\ncannot be applied to the term\r\n "nat" : "\x1b[33;1mSet\x1b[0m"\r\n' after: <class 'pexpect.exceptions.EOF'> match: None match_index: None exitstatus: None flag_eof: True pid: 11150 child_fd: 5 closed: False timeout: 30 delimiter: <class 'pexpect.exceptions.EOF'> logfile: None logfile_read: None logfile_send: None maxread: 2000 ignorecase: False searchwindowsize: None delaybeforesend: 0 delayafterclose: 0.1 delayafterterminate: 0.1 searcher: searcher_re: 0: re.compile('\r\n[^< ]+ < ') make[1]: *** [Makefile.doc:65: refman-html] Error 2 ~~~ Co-authored-by: Clément Pit-Claudel <clement.pitclaudel@live.com>
2019-02-18Sphinx: fail when a command failsGaëtan Gilbert
This uses a new coqtop-only option "Coqtop Exit On Error", not sure where to put the doc for it. It being an option means we can locally turn it off (.. coqtop:: fail).
2019-02-18Sphinx: remove [coqtop:: undo]Gaëtan Gilbert
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2019-02-18Add diff rule for README.rst to dune refman-html aliasGaëtan Gilbert
We change regen_readme such that when given an argument it outputs there instead of overwriting the readme. Prompted by me noticing I forgot to regen in #9553.
2019-02-14[coqlib] Remove `-boot` option for setting the coqlibEmilio Jesus Gallego Arias
Instead, if the coqlib is special, we set it explicitly in the command line, as Dune does. This is a continuation of #9523. In Sphinx, we stop using -boot, and pass `-coqlib` through the environment instead. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2019-02-12Fix doc for coqtop:: undoGaëtan Gilbert
2019-01-09[Manual] Remove link to non-existing CSS fileVincent Laporte
2018-12-14Merge PR #9073: [sphinx] No more undocumented objects.Clément Pit-Claudel
2018-12-14Do not raise object without body warning for prodn objects.Théo Zimmermann
2018-12-13[dune] [doc] Support for building the reference manual with Dune.Emilio Jesus Gallego Arias
This is a reduced version of #8503 as to provide a way to build the reference manual with Dune. Dune 1.6 supports (experimentally) directories as targets, thus we introduce a rule that will call `sphinx` to build the manual. This only provides build, however generation of `.install` rules is not done, it will be hopefully addressed in #8503. Note that we set `expire: 1 month` for all the artifacts we build with Dune. IMHO this makes most sense as not to abuse Gitlab's hosting, however of course we could consider a different deployment strategy if wanted.
2018-10-01Merge PR #8301: Documentation for proof diffsThéo Zimmermann
2018-09-25[doc] Fix GH-8529: wrap macro definitions in math delimiters for MathJaxClément Pit-Claudel
2018-09-23Update flag, option and table descriptions in coqdomain.py, update ↵Jim Fehrle
README.rst to match. Bump env_version.
2018-09-23Documentation for proof diffsJim Fehrle
2018-09-20Define flags (binary-valued settings) and tables (settings that are sets)Jim Fehrle
as separate NotationObject types, include in index.
2018-09-20[doc] Rewrite and document the prodn directiveClément Pit-Claudel
It was broken and undocumented. We dropped the git logs, too, so it wasn't clear who wrote it and why it was introduced in the first place.
2018-09-20[doc] Work around https://github.com/sphinx-doc/sphinx/issues/4979Clément Pit-Claudel
2018-09-20[doc] Ensure that merging coqtop blocks preserves anchorsClément Pit-Claudel
2018-09-20[doc] Work around https://github.com/sphinx-doc/sphinx/issues/4980Clément Pit-Claudel
2018-09-20[doc] Fix a typo in the developer guideClément Pit-Claudel
2018-09-20[doc] Add env_version to metadata of coqrst pluginClément Pit-Claudel
This is required by Sphinx 8.0. See https://github.com/sphinx-doc/sphinx/issues/4460.
2018-09-20[doc] Create a separate index file for the LaTeX buildClément Pit-Claudel
See https://github.com/sphinx-doc/sphinx/issues/4977 for context.
2018-09-20[doc] Move the LaTeX preamble to a separate .tex fileClément Pit-Claudel
2018-09-20[doc] Fix a typo in coqdomain.pyClément Pit-Claudel
2018-08-31Merge PR #8170: Don't index names starting with `_` in docsThéo Zimmermann
2018-08-22Fix #8251: remove "the the" occurrencesGaëtan Gilbert
2018-07-30[sphinx] Use arguments of '.. example::' directive as a titleClément Pit-Claudel
Most existing uses of .. example did not use the first line as a title, so this commit also adds appropriate blank lines.
2018-07-26[sphinx] Do name cleanup in handle_signatureClément Pit-Claudel
2018-07-25[sphinx] Add a way of skipping names in the indexes.Théo Zimmermann
2018-06-21Merge PR #7815: On cygwin, pass the filename in a format that coqdoc ↵Maxime Dénès
understands.
2018-06-20On cygwin, pass the filename in a format that coqdoc understands.Jim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-12 19:25:46 +0000