| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
|
|
|
|
I followed the code for fiat-crypto / fiat-parsers. I hope I didn't
miss anything.
|
|
So we avoid problems like the one in #7438.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
When invoking through Makefile we always rebuild dependencies. To skip
dependencies, invoke ci-wrapper directly. We make Circle CI do this.
In order to properly support invoking ci-wrapper directly we replace
"make" in ci-common by a bash function which adds -j to the make
invocation outside submakes. We also set TIMED in the ci-wrapper.
|
|
|
|
|
