| Age | Commit message (Collapse) | Author |
|---|
|
Fixes #12582
The previous code said that `Nat.v.log` (and therefore `Nat.vo`) should
be rebuilt anytime `Nat.v.log` is older than `plik.v.vo`, and also says
that `plik.v.log` (and therefore `plik.vo`) should be rebuilt anytime
`plik.v.log` is older than `Nat.vo`. This is circular, and results in
`make` considering all of the `modules/` tests out-of-date on any fresh
run.
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: herbelin
|
|
This is needed for the case the sources are set to read-only mode, for
example when using Dune >= 2.5 [needed for the global cache support]
Fixes #12264
Co-authored-by: Ignat Insarov <kindaro@gmail.com>
|
|
|
|
This reverts commits 71ea3ca8b4d3a6fa6b005e48ff7586176b06259e and
0976a670cf853c9bc61b3eee6dceae4a429e066f.
|
|
Since `ocaml_pwd.ml` was added this unquoted glob would be expanded by
the shell before being passed to `find`.
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
|
|
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: gares
|
|
Add headers to a few files which were missing them.
|
|
This was accidentaly disabled by #6264 when no_native_compiler was
renamed to native_compiler.
Moreover, the (then unactivated test) was broken by commit 48ae6ce
(part of #9088).
|
|
See "https://github.com/coq/coq/pull/10008#discussion_r382899607".
|
|
Compile buffer, and with building from a path containing spaces.
Updated CHANGES.md
Now using Filename.quote instead of enclosing in single quotes.
Fixed rebasing problems.
|
|
(and not just…
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
The regexp parsing the time needed an update to support the case
"Finished failing translation". Also, not all cases of failures were
reported.
|
|
|
|
c.f. https://dev.azure.com/coq/coq/_build/results?buildId=6485&view=logs&jobId=2d2b3007-3c5c-5840-9bb0-2b1ea49925f3&j=2d2b3007-3c5c-5840-9bb0-2b1ea49925f3&t=77aad734-2057-5694-9ae2-ee1f5f26eae8
|
|
Apparently `expr 1 \+ 1` is fine on Linux but not cygwin/Windows, where
it fails with "syntax error". Similarly for `-` and `/`.
|
|
This reverts commit ec505a2fa67b0776b624be54417e06c6512f1734.
A better fix is coming
|
|
Apparently the bogomips produced by cygwin are extra-bogo.
|
|
if the .vos file is empty, rename -quick to -vio, dump empty .vos when producing .vio, dump empty .vos and .vok files when producing .vo from .vio.
|
|
In particular, display how long they took in bogomips-adjusted
centiseconds.
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Ack-by: proux01
Ack-by: silene
Ack-by: vbgl
|
|
A .vos file stores the result of compiling statements (defs, lemmas)
but not proofs.
A .vok file is an empty file that denotes successful compilation of
the full contents of a .v file.
Unlike a .vio file, a .vos file does not store suspended proofs,
so it is more lightweight. It cannot be completed into a .vo file.
|
|
Add utility ldexp and frexp functions to prevent dealing with the shift of
ldshiftexp and frshiftexp everywhere.
Also move primitive integer tests to place all primitive tests in the
same directory.
|
|
i.e. you can do
~~~
make -f Makefile.dune world
make -C test-suite success
~~~
to make just the success tests, then modify Coq sources and retest
just the ones you want
|
|
with coqtop
Reviewed-by: gares
Ack-by: jfehrle
|
|
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
|
|
|
|
Since Ltac2 cannot be put under the stdlib logical root (some file names
would clash), we move it to the `user-contrib` directory, to avoid adding
another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego.
Thanks to @Zimmi48 for the thorough documentation review and the
numerous suggestions.
|
|
This causes the makefile to break due to dependencies when it fails,
and it's not worth adding a whole mess of code to catch the failure
for these files.
|
|
|
|
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.
|
|
- default targets don't depend on ocamlopt when it's unavailable
- coqc.byte is built by byte target and coqc by coqbinaries target
- unit tests use best ocaml
- poly-capture-global-univs tests ml compilation with ocamlc
- don't try to install .cmx and native-compute .o files
cf https://github.com/coq/coq/issues/9464
|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
Reviewed-by: gares
|
|
We make `coqc` a truly standalone binary, whereas `coqtop` is
restricted to interactive use.
Thus, `coqtop -compile` will emit a warning and call `coqc`.
We have also refactored `Coqargs` into a common `Coqargs` module and a
compilation-specific module `Coqcargs`.
This solves problems related to `coqc` having its own argument
parsing, and reduces the number of strange argument combinations a
lot.
|
|
This PR deprecates the use of `coqtop` as a compiler.
There is no point on having two binaries with the same purpose; after
the experiment in #8690, IMHO we have a lot to gain in terms of code
organization by splitting the compiler and the interactive binary.
We adapt the documentation and adapt the test-suite.
Note that we don't make `coqc` a true binary yet, but here we take
care only of the user-facing part.
The conversion of the binary will take place in #8690 and will bring
code simplification, including a unified handling of arguments.
|
|
This makes the display consistent wrt `TEST`:
```
TEST failure/Case7.v
CHECK Case7
```
vs
```
TEST failure/Case7.v
CHECK failure/Case7.v
```
|
|
After #8655
|
