| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
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
|
|
|
|
After #9590
Instead of this we could override before_script, either duplicating the debug
prints or just not doing debug prints for the trunk jobs.
|
|
|
|
This ensures that the log will contain the commit hash that we tested.
This reuses the method from the Windows build script (we have a number
of common functions, it would be interesting to start a bash shared
library file).
|
|
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.
|
|
Reviewed-by: SkySkimmer
|
|
When the bot auto-merged the linter saw no commits to lint, eg
https://gitlab.com/coq/coq/-/jobs/162893603
I'm pushing from a non-current master so we will see if this works.
|
|
Ack-by: ppedrot
|
|
and primititive projections
Reviewed-by: maximedenes
|
|
Fixes #9323.
|
|
Since a long time the compiler switch is not very useful as it is not
used to test any CI.
The `edge+flambda` version seems stable enough to carry out the `edge`
testing by itself, thus we remove the `egde` switch saving valuable
Docker image size and Gitlab runners.
We also tweak the `pkg:opam` job as to correctly set the version of
the pinned local package.
|
