| Age | Commit message (Collapse) | Author |
|---|
|
|
|
They should not be necessary today as they date from the shareable
pre-artifact epoch, an incur in an slowdown.
|
|
|
|
|
|
|
|
In this way interval does not have to wait too much
|
|
|
|
|
|
|
|
|
|
This partially reverts commit 35a1cc4f5c708b745a2810a64d220f49eff4beca.
(I've not added back the nix things, since I'm not sure what purpose
they serve, and I've adjusted the targets slightly.)
The CI build should no longer take an enormously long time to start, and
fiat-crypto-legacy code is actively being used to track down memory
issues in #12487. Additionally, f-c-l revealed a genuine bug in #7825,
and so I'd like to keep f-c-l in the CI at least until #7825 is
finished.
I've been maintaining compatibility of f-c-l with master anyway on the
side, in part to continue some performance experiments with it, and
expect to continue to do so at least until the end of this calendar
year, and it'd be nice for me to get advance warning when a PR is going
to break it on master. (It seems reasonable to me to take it off the CI
again once I'm no longer maintaining it / collecting data from it, and /
or once #7825 is finished.)
|
|
It's tested on the bench, so might as well test it on the CI. Hopefully
it's not too memory-heavy. (It should only take a couple of minutes,
time-wise.)
|
|
Note that this should reduce the overall build time of fiat-crypto
related targets by about 10--20 minutes, as I've removed the heaviest
jobs (about 25--30 minutes in serial) from the OCaml target.
I'd like to keep the OCaml target around just to make sure that Coq
doesn't introduce a change to extraction that breaks compilation of
extracted OCaml code. See https://github.com/ocaml/ocaml/issues/7826
for the issue tracking performance of compiling the extracted OCaml
code (and perhaps there should be another issue opened on the OCaml bug
tracker about flambda on the fiat-crypto extracted files?)
Alternative to #12405
Closes #12405
Fixes #12400
|
|
This is a new development where I'm aggregating a specific set of
benchmarks. It's intended to be relatively lightweight, taking only a
handful of minutes. It's probably one of the few developments currently
testing Ltac2.
|
|
|
|
After #12023 broke the bug minimizer, I'd like to add
[coq-tools](https://github.com/JasonGross/coq-tools/) to the CI. It's
relatively light-weight (under 5 minutes, I believe), and I'd like to
know when it's going to break on master before it's broken, rather than
after. It tests a relatively under-tested part of Coq, mostly (the
display output of error message, by and large), and I'm happy to take
responsibility for fixing it when some PR is going to break it (mainly I
just want a sort-of early warning system, and I want PRs to not
accidentally break it by changing things that they don't realize they're
changing).
|
|
Specifically https://github.com/PrincetonUniversity/VST/commit/86d7ac6eaf9c580d5705c4257814f64560d24257
|
|
I believe a recent commit to master broke it, and now that it's no
longer tested as part of fiat-crypto-legacy, I think it's time to add
it.
|
|
|
|
Add headers to a few files which were missing them.
|
|
No reason to have them in the same .sh
|
|
Motivations:
- We should have only maintained developments in our CI
- `make ci-fiat-crypto-legacy` takes about 15 mins before the first call
to `coqc`, making it unusable to work on overlays
- The coding style of this development is so fragile that adapting to
any change of behavior requires diffing gigabytes of Ltac traces.
@mattam82 and I have been blocked for 6 months this way, when working on
unifall.
I understand this development was meant to stress-test some components
like printing, but I think the trade-off is bad. We should rather come
up with specialized test suites for these components.
|
|
Fiat-Crypto does not guarantee compatibility with the tip of bedrock2,
only with the pinned version, and bedrock2 is still relatively unstable.
So we make the CI not have Fiat-Crypto depend on bedrock2, and instead
use the pinned submodule, by using `EXTERNAL_REWRITER=1
EXTERNAL_COQPRIME=1` rather than `EXTERNAL_DEPENDENCIES=1`.
|
|
|
|
|
|
|
|
|
|
TLC and CPDT are not actually tested. No point in keeping them as if they were.
|
|
|
|
|
|
The amount of dangerous warnings in plugins is out of hand, including
some very serious ones.
As Coq developers are maintaining plugins these days it makes sense to
require the contributions to follow the same coding discipline as in
the main tree, thus we require the set of warnings fatal warnings to
be the same in Coq and in plugins.
We don't mark deprecation as fatal as to allow time for migration.
Fixes #6974
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
This was suggested by the author. See
https://github.com/bmsherman/topology/issues/23
|
|
|
|
|
|
pidetop relies on some rather low level API from STM, which we'd like to
change. It does not seem maintained much anymore, and still hasn't moved
to github.
|
|
This is convenient as to have better automation.
|
|
|
|
|
|
|
|
And fix a typo that was previously there.
|
|
This was kept as a fallback for some time, not worth keeping it
anymore as our GitLab setup seems mature and reliable enough.
|
|
This closes #7618.
|
|
|
|
There is the new pipeline, and the old pipeline. Most of what they
share in common is the (very large) library of lemmas about `Z`.
As per the discussion in
https://github.com/coq/coq/pull/8064#issuecomment-413474176 through
https://github.com/coq/coq/pull/8064#issuecomment-413793143
|
