| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
This allows for nicer formatting without having to deal with Make's
semantic whitespace.
|
|
|
|
This fixes the fix 1522b989 to #7192.
The remaining Not_found after 1522b989 should have rung a bell that
something was still strange.
|
|
|
|
GitLab setup is quite stable these days thanks to the work of many
people and `coqbot`. We decided to keep CircleCI support for a while
as a safeguard in case something happened in the migration to GitLab,
but these days we are just wasting resources to them and to us. As I'm
afraid CircleCI won't scale for us, the time to remove it has arrived.
Still, CircleCI had some awesome functionality that GitLab's CI
doesn't offer yet, see the links at:
https://github.com/coq/coq/issues/6919#issuecomment-395885573
- https://gitlab.com/gitlab-org/gitlab-ce/issues/29347
- https://gitlab.com/gitlab-org/gitlab-ce/issues/35222
- https://gitlab.com/gitlab-org/gitlab-ce/issues/41947
- https://gitlab.com/gitlab-org/gitlab-ce/issues/47063
|
|
When launched through PATH argv.(0) is just the command name.
eg "coqtop -compile foo.v" -> argv.(0) = "coqtop"
Using executable_name also follows symlinks but this isn't tested to
avoid messing with windows. Running Coq through a symlink is not as
important as PATH anyways.
|
|
|
|
The file `config/Makefile` doesn't exist unless we run `./configure`.
We shouldn't have to run `./configure` to run `make clean`. We now no
longer error in any case if `config/Makefile` doesn't exist; this is
simpler than only not erroring if the target is `clean`.
We also now test this property when building on CI.
This fixes #7542
|
|
|
|
|
|
|
|
NB: I made .aux be cleaned only with distclean imitating the main Makefile.
|
|
ie you might see
make
TEST bugs/closed/1337.v
TEST bugs/closed/3263.v
TEST bugs/closed/7777.v
FAILED bugs/closed/3263.v.log
TEST bugs/opened/1.v
...
report: 3263 failed (should be closed)
|
|
|
|
|
|
PRINT_LOGS can be used for interactive calls, eg
make report PRINT_LOGS=1
|
|
|
|
|
|
This allows us to enforce that it works without breaking the build
when it doesn't.
|
|
|
|
|
|
The file links.v is using utf-8 characters so this is needed at least
to test this file. For the other files, it is not completely without
effect since it makes that symbols like => and forall are respectively
displayed ⇒ and ∀.
Maybe tests with iso-8859-1 or test without a charset option should be
kept.
|
|
This file can be used to get in an environment ready to compile Coq
(with `nix-shell`) or to compile and install Coq (with `nix-build`).
|
|
|
|
This is a temporary workaround, until we fix the underlying issue which
makes coqtop hang on those tests.
|
|
Commit 8f12597 introduced new output tests but these were broken on Windows.
We fix them by using --strip-trailing-cr option of diff, like in other
output tests in the test-suite.
|
|
wrongly tagged as keywords
|
|
|
|
|
|
|
|
|
|
One file was already ready for testing. We add another one.
Note that we have to remove the machine-dependent lines in the output
tex files.
|
|
It drops anything after a `/`, so we change all `/`s into `.`.
There must be a better way to do this that doesn't involve so much bash
hackery, right?
|
|
|
|
|
|
|
|
|
|
There was an extra trailing space in #680.
Now things display as, e.g.,
```
TEST bugs/opened/3754.v
TEST bugs/opened/4803.v (-compat 8.4)
```
instead of
```
TEST bugs/opened/3754.v ( )
TEST bugs/opened/4803.v (-compat 8.4 )
```
|
