| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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>
|
|
|
|
|
|
|
|
|
|
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.
|
|
Lintian found some spelling errors in the Debian packaging for coq. Fix
them most places they appear in the current source. (Don't change
documentation anchor names, as that would invalidate external
deeplinks.)
This also fixes a bug in coqdoc: prior to this commit, coqdoc would
highlight `instanciate` but not `instantiate`.
|
|
|
|
|
|
README.rst to match.
Bump env_version.
|
|
|
|
as separate NotationObject types, include in index.
|
|
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.
|
|
|
|
|
|
|
|
|
|
This is required by Sphinx 8.0. See
https://github.com/sphinx-doc/sphinx/issues/4460.
|
|
See https://github.com/sphinx-doc/sphinx/issues/4977 for context.
|
|
|
|
|
|
|
|
|
|
Most existing uses of .. example did not use the first line as a title, so this
commit also adds appropriate blank lines.
|
|
|
|
|
|
understands.
|
|
|
|
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.
|
|
|
|
As discussed in GH-7556.
|
|
|
|
|
|
|
|
Co-Authored-By: @Zimmi48
|
|
|
|
Co-Authored-By: @Zimmi48
|
