| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
|
|
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
The `-boot` option was used to:
- suppress loading of the rc_file
- allow to save modules with prefix `Coq`
There is no good reason disable saving of modules with `Coq` prefix by
default, thus we remove this option.
Fixes: #9575
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
|
|
|
|
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
Reviewed-by: ejgallego
|
|
|
|
In passing add -coqlib to coqchk's usage message.
|
|
shell buffer
Reviewed-by: ejgallego
|
|
Reviewed-by: vbgl
|
|
+ remove checker/.depend forgotten file
|
|
Reviewed-by: SkySkimmer
|
|
Absolute paths follow different separator rules so "c:\foo/bar" may
not work on `mingw`.
We try to improve this situation using OCaml's `Filename.dir_sep/concat`
|
|
We may want to keep the make-based and Dune job, however the
make-based setup is tested by the INRIA workers so it may not be
needed.
In order for some test to run well, we always run in Dune with an
absolute path. The easiest way to get a portable absolute path is to
use OCaml itself so we introduce a small executable to do that.
While we are at it, we do some cleanup of the test-suite `dune` file,
in particular we remove useless comments, set `--no-buffer` so results
can be seen in real time, and recognize the `NJOBS` variable as we
have moved to a Dune version that supports env vars.
|
|
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
|
|
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: Zimmi48
Reviewed-by: cpitclaudel
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
Ack-by: herbelin
Reviewed-by: mattam82
|
|
effectively computed at lexing time)
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
|
|
Parameters had to be removed in cases_pattern_of_glob_constr.
|
|
This is because it can raise Not_found in depth and we need to catch
it at the right time.
|
|
Make it mandatory to give exactly one display option.
|
|
|
|
The conclusion of W-Ind,
"\WF{E;~\ind{p}{Γ_I}{Γ_C}}{Γ}", is changed to
"\WF{E;~\ind{p}{Γ_I}{Γ_C}}{}" because
local contexts should be empty when
inductive definition is defined globally.
This is consistent with W-Global-Assum and W-Global-Def.
The side condition "c_i ∉ Γ ∪ E" which I changed previous commit is
changed again to "c_i ∉ E" because I guess that it tries to
avoid name conflicts to the local contexts in the conclusion.
However, the condition is useless after the local contexts is empty.
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
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>
|
|
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
Reviewed-by: herbelin
Ack-by: jashug
|
|
Reviewed-by: ejgallego
|
|
tarball.
Reviewed-by: SkySkimmer
Reviewed-by: ejgallego
|
|
Ack-by: Zimmi48
Reviewed-by: jfehrle
Ack-by: ppedrot
|
|
Reviewed-by: ejgallego
|
