| Age | Commit message (Collapse) | Author |
|---|
|
The timing diff script dies badly on non-utf8 input (https://github.com/coq/coq/issues/9767).
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: jashug
|
|
Ack-by: gares
Ack-by: herbelin
Ack-by: mattam82
Ack-by: ppedrot
|
|
This is routine as for API doc writers to be able to access the newer
features.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
It used to simply remember the normal form of the type of the constructor.
This is somewhat problematic as this is ambiguous in presence of
let-bindings. Rather, we store this data in a fully expanded way, relying
on rel_contexts.
Probably fixes a crapload of bugs with inductive types containing
let-bindings, but it seems that not many were reported in the bugtracker.
|
|
|
|
Supersedes #8718.
|
|
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.
|
|
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).
|
|
Reviewed-by: SkySkimmer
|
|
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.
|
|
In order to do so we place the polymorphic status and name in the
read-only part of the monad.
Note the added comments, as well as the fact that almost no part of
tactics depends on `proofs` nor `interp`, thus they should be placed
just after pretyping.
Gaëtan Gilbert noted that ideally, abstract should not depend on the
polymorphic status, should we be able to defer closing of the
constant, however this will require significant effort.
Also, we may deprecate nameless abstract, thus rending both of the
changes this PR need unnecessary.
|
|
Reviewed-by: maximedenes
|
|
passed
https://gitlab.com/coq/coq/-/jobs/158737429
|
|
COQMF_ARGS is a bedrock2-specific name to pass extra arguments to coq_makefile,
and we use VERBOSE=1 for better debuggability
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Reviewed-by: ejgallego
|
|
|
|
|
|
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: vbgl
|
|
|
|
Coq and the Coq libraries can now be excluded
(by setting the NOCOQ environment variable).
|
|
|
|
|
|
|
|
suite again
|
|
The azure OSX job replaces the first travis job, and the second always
fails and so is useless.
|
|
Reviewed-by: maximedenes
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: Zimmi48
|
|
We're recently reorganized fiat-crypto. This should fix the OOM CI
issues.
Fixes #9338
|
|
Move plugin tutorial to Coq repo
|
|
Once https://github.com/mit-plv/fiat-crypto/pull/477 is merged, the
master branch will no longer contain the files nor the targets for
fiat-crypto legacy. (We should perhaps consider moving fiat-crypto
legacy to coq-community as a source of vm and printing tests.)
|
|
|
|
|
|
|
|
This was suggested by the author. See
https://github.com/bmsherman/topology/issues/23
|
