| Age | Commit message (Collapse) | Author |
|---|
|
(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
|
|
|
|
|
|
We add a job testing the build of Coq with OCaml 4.08 [AKA `trunk`]
CoqIDE is not supported in 4.08 due to missing `lablgtk`, also `oUnit`
cannot be currently installed, thus we have to add a switch to the
test suite to disable `unit-tests`.
Many deprecation warnings happened in 4.08 so we use the `release`
profile to make them not fatal. Using a 4.08 build profile would be an
option too.
|
|
|
|
|
|
|
|
It seems we forgot to export when moving the script to a separate file.
|
|
Hopefully this goes away when OCAMLPATH is properly handled by the
build system.
|
|
This fixes an obvious bug introduced in #8602.
|
|
tests.
|
|
|
|
|
|
|
|
This is slightly more robust and allows to run the test suite with
Dune which may place OCaml objects differently.
|
|
|
|
- Simplex based linear prover
Unset Simplex to get Fourier elimination
For lia and nia, do not enumerate but generate cutting planes.
- Better non-linear support
Factorisation of the non-linear pre-processing
Careful handling of equation x=e, x is only eliminated if x is used linearly
- More opaque interfaces
(Linear solvers Simplex and Mfourier are independent)
- Set Dump Arith "file" so that lia,nia calls generate Coq goals
in filexxx.v. Used to collect benchmarks and regressions.
- Rationalise the test-suite
example.v only tests psatz Z
example_nia.v only tests lia, nia
In both files, the tests are in essence the same.
In particular, if a test is solved by psatz but not by nia,
we finish the goal by an explicit Abort.
There are additional tests in example_nia.v which require specific
integer reasoning out of scope of psatz.
|
|
|
|
Also test that the compat updating script hasn't become outdated on the
CI.
|
