| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
The computation of which files to build is now mostly cached rather than
computed, eliminting basically all of the wait-time from `make` to the
first invocation of `coqc`.
Note that we no longer need to invoke
`./etc/ci/remove_autogenerated.sh`, but it does not hurt, and it speeds
up `coqdep` somewhat significantly.
Fixes #9298
|
|
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 allows to use fixed commits and not just branches or tags.
We keep using git clone when $FORCE_GIT is set (for projects on
gforge.inria.fr and projects pulling dependencies through git submodules).
fiat-parsers also calls git submodule, but inside its own Makefile.
|
|
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
|
