| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
| |
We combine two stages that are both fairly quick (early and lite), and
we move nobigmem from coq to pre-standalone in an attempt to hopefully
decrease the incidence of OOM issues on travis.
|
| | |
|
| | |
|
| |
|
|
| |
Update 8.8.0 to 8.8.2, add v8.9 branch
|
| |
|
|
|
| |
This will hopefully take some burden off later travis stages and make
PR #437 easier to merge.
|
| |
|
|
|
| |
Also change the travis config so that it's easier to insert new stages
without globally renaming everything
|
| |
|
|
| |
It's starting to get pretty slow.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Sometimes we get logs like
[this](https://travis-ci.org/mit-plv/fiat-crypto/jobs/393628098), where
we have
```
Reading package lists...
W: GPG error: http://ppa.launchpad.net/jgross-h/many-coq-versions/ubuntu trusty InRelease: The following signatures couldn't be verified because the public key is not available: NO_PUBKEY E58B19DAA454A7D9
W: The repository 'http://ppa.launchpad.net/jgross-h/many-coq-versions/ubuntu trusty InRelease' is not signed.
W: There is no public key available for the following key IDs:
E58B19DAA454A7D9
W: http://ppa.launchpad.net/couchdb/stable/ubuntu/dists/trusty/Release.gpg: Signature by key 15866BAFD9BCC4F3C1E0DFC7D69548E1C17EAB57 uses weak digest algorithm (SHA1)
```
and then
```
WARNING: The following packages cannot be authenticated!
ocaml-base-nox ocaml-compiler-libs ocaml-interp ocaml-nox
libcamlp4-ocaml-dev camlp4 coq-8.7.2-theories liblablgtk2-ocaml
liblablgtksourceview2-ocaml libcoq-8.7.2-ocaml ocaml-native-compilers
coq-8.7.2 coq-8.7.2ide libfindlib-ocaml libfindlib-ocaml-dev ocaml-findlib
E: There were unauthenticated packages and -y was used without --allow-unauthenticated
```
I'm not sure if this is the right way to fix this...
|
| | |
|
| |
|
|
|
| |
Now we test master, v8.8.dev, v8.7.dev, 8.8.0, and 8.7.2, instead of master,
v8.7.dev, and 8.7.1.
|
| |
|
|
|
|
|
| |
https://github.com/travis-ci/travis-ci/issues/8507
We use a script and travis_retry to work around "failed to fetch" with
launchpad
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Hopefully this will lead to overall faster builds
Also:
- try to allow failures
- Version-specific vo caches
- Make archives stage-specific
This way, if multiple branches are running stages at the same time, they
don't have as much a chance of clobbering each others builds.
|
| | |
|
| | |
|
| |
|
|
| |
https://github.com/travis-ci/travis-ci/issues/8507
|
| |
|
|
| |
This will hopefully work better than kludging around coqdep
|
| |
|
|
| |
building things
|
| | |
|
| | |
|
| |
|
|
| |
This closes #255
|
| | |
|
| |
|
|
|
|
|
|
| |
We now only build selected-test and selected-bench with one version of
Coq (picked 8.7+beta2, because hopefully it'll be faster than 8.6.1).
Previously, some travis builds failed because some travis machines don't
support adc, adcx, mulx, etc.
|
| |
|
|
| |
Also hopefully fix travis
|
| |
|
|
|
|
| |
Travis was too slow to run all of the coq target, so we split off the
no-curves-proofs and the curves-proofs targets, and, while we're at it,
also add 8.7+beta1 tests.
|
| | |
|
| | |
|
| |
|
|
| |
It's not useful, since we pass -compat 8.6
|
| |
|
|
| |
It gives "illegal instruction" on p256
|
| | |
|
| | |
|
| |
|
|
| |
We don't need it
|
| | |
|
| | |
|
| |
|
|
| |
It's more readable now
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
This closes #122
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
jadep
Jason Gross
Andres Erbsen
Jason Gross
Jason Gross