| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
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
|
|
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.
|
|
I think the usage looks cleaner this way.
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
#9488)
Ack-by: gares
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: cpitclaudel
|
|
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>
|
|
It was used in the standard library and the test-suite but undocumented so far.
|
|
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: maximedenes
|
|
|
|
|
