coq/doc/tools/coqrst/repl, branch master

Show "Error:"/"Warning:" with white type (on red/orange background)

2021-02-15T06:11:15+00:00

Add -q flag to coqrst python invocation of coqtop

2020-12-16T16:55:17+00:00

This will help with reproducibility for people who have something in their coqrc file.

Co-authored-by: Théo Zimmermann

Match only a single line as the coqtop prompt

2020-06-06T21:18:20+00:00

(the previous expression was including some expected output)

Update headers in the whole code base.

2020-03-18T11:15:43+00:00

Add headers to a few files which were missing them.

Update py-style headers to new year.

2019-06-17T16:08:32+00:00

Fixing typos - Part 1

2019-05-21T21:07:55+00:00

[sphinx] Add warn option to coqtop directive.

2019-02-28T13:26:41+00:00

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.

Merge PR #9560: [coqlib] Remove `-boot` option for setting the coqlib

2019-02-20T12:24:34+00:00

Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares

Sphinx: nicer error reporting

2019-02-18T20:24:11+00:00

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.
    
    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: 
    match: None
    match_index: None
    exitstatus: None
    flag_eof: True
    pid: 11150
    child_fd: 5
    closed: False
    timeout: 30
    delimiter: 
    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

[coqlib] Remove `-boot` option for setting the coqlib

2019-02-14T15:30:28+00:00

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