| Age | Commit message (Collapse) | Author |
|---|
|
Remove unneeded source and output files
Move all commands under command NT
Add a lot of edits for commands and tactics
|
|
|
|
(translate '_' to '-' consistently)
|
|
Ack-by: SkySkimmer
Reviewed-by: jfehrle
Reviewed-by: ppedrot
|
|
|
|
|
|
following changes to attribute parsing.
|
|
|
|
Add headers to a few files which were missing them.
|
|
|
|
|
|
|
|
|
|
Show effect of edits to edited nt in PRINT
Add cmdv:: info to prodnCommands
Supporting code globally replaces a given "substring" in productions
with another. (Substring over doc_symbols, not over characters.)
|
|
those in the rsts.
|
|
|
|
Reviewed-by: Zimmi48
|
|
|
|
Ex: "(tactic)" instead of "(tacn)"
|
|
Otherwise you need a few feedback loops to install all dependencies.
|
|
I lacked this package, and got:
``` $ make -j2 COQ_USE_DUNE=1 refman-html
[...]
env doc/sphinx_build (exit 2)
(cd _build/default/doc && /usr/bin/env COQLIB=.. sphinx-build -j4 -W -b html -d sphinx_build/doctrees sphinx sphinx_build/html)
Running Sphinx v2.1.2
Extension error:
Could not import extension sphinxcontrib.bibtex (exception: No module named 'sphinxcontrib.bibtex')
make: *** [refman-html] Error 1
```
|
|
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.
|
|
|
|
|
|
|
|
|
|
Update doc_grammar tool
The grammar in the doc is generated semi-automatically with doc_grammar:
- the grammar is automatically extracted from the mlg files
- developer-prepared editing scripts *.mlg_edit modify the extracted
grammar for clarity, simplicity and ordering of productions
- chunks of the resulting grammar are automatically inserted into the
rsts using instructions embedded in the rsts
Running doc_grammar is currently a manual step.
The grammar updates in the rst files have been manually reviewed.
|
|
for integers and natural nums
|
|
and inserting it into the .rst files
|
|
|
|
Remove other types of lines before copyright headers.
|
|
|
|
|
|
|
|
|
|
Closes GH-8482.
|
|
|
|
|
|
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.
|
|
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
|
|
Make it mandatory to give exactly one display option.
|
|
|
|
|
|
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.
> ^^^^^^^
[37;41;1mError:[0m Illegal application (Non-functional construction):
The expression "nat" of type "[33;1mSet[0m"
cannot be applied to the term
"nat" : "[33;1mSet[0m"
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>
|
|
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).
|
|
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
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.
|
|
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>
|
|
|
|
|
