Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | Remove ci-fiat-parsers from allowed_failures | 2017-06-15 | ||
|/ | | | | It shouldn't be failing. | |||
* | Move Fiat to allowed failures. | 2017-06-15 | ||
| | | | | For now, Fiat still relies on 8.4 compatibility. | |||
* | Remove bedrock from test suite. | 2017-06-15 | ||
| | | | | | | Bedrock relies on the 8.4 compat flag that we are removing, and we heard from MIT that they did not plan to port bedrock to more recent versions of Coq. | |||
* | Merge PR#749: Normalize deprecation notices of ./configure | 2017-06-14 | ||
|\ | ||||
* | | [travis] extra test ci-bignums (+factorize other scripts) | 2017-06-13 | ||
| | | ||||
| * | Normalize deprecation notices of ./configure | 2017-06-11 | ||
| | | | | | | | | Always output a warning on stderr when a deprecated option is used. | |||
* | | Make coq-dpdgraph allow-fail | 2017-06-02 | ||
| | | ||||
* | | Add coq-dpdgraph CI | 2017-06-02 | ||
|/ | ||||
* | [travis] Add OSX test-suite checking. | 2017-06-01 | ||
| | | | | | | This is a first step towards getting Travis build our OSX package, but is also useful immediately (c.f. the recent breakage of the coq_makefile test-suite under OSX). | |||
* | travis: coq_makefile needs the tipa package | 2017-05-23 | ||
| | ||||
* | Travis: do not cache opam logs (+prettier spacing) | 2017-05-19 | ||
| | ||||
* | Merge branch 'v8.6' | 2017-05-17 | ||
|\ | ||||
* | | Travis: add -warn-error targets (standard and 4.04.1 ocaml) | 2017-05-17 | ||
| | | ||||
* | | Travis: deduplicate package list for coqide+documentation targets | 2017-05-17 | ||
| | | ||||
* | | Travis: do not run the tests if building Coq fails | 2017-05-17 | ||
| | | ||||
* | | [travis] Update OCaml to 4.04.1 | 2017-05-13 | ||
| | | ||||
* | | [travis] Move VST to required suite. | 2017-05-13 | ||
| | | ||||
| * | Put .travis.yml in alphabetical order | 2017-05-09 | ||
| | | ||||
| * | Add bmsherman/topology to the ci | 2017-05-01 | ||
| | | | | | | | | | | This development of @bmsherman tests universe polymorphism and setoid rewriting in type, and should build with v8.6 and trunk. | |||
* | | Merge branch 'v8.6' | 2017-04-27 | ||
|\| | ||||
* | | [travis] Pin camlp5 to the minimal version 6.14 for 4.02.3 | 2017-04-24 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | We now test: - 4.02.3 + 6.14 [and 32bits of those] - 4.04.0 + 6.17 this looks like what the official support set should be for 8.7, given that both Ubuntu and Debian will ship the first, then switch to the latter. We also pin xmlm to version 1.2.0 to workaround bug https://github.com/ocaml/opam-repository/issues/8815 | |||
| * | Add bedrock targets src and facade | 2017-04-20 | ||
| | | ||||
* | | [travis] Add webhook to Gitter. | 2017-04-06 | ||
| | | ||||
| * | [travis] Backport from trunk: VST | 2017-03-24 | ||
| | | ||||
* | | [travis] Add VST | 2017-03-24 | ||
| | | ||||
| * | [travis] [8.6.only] Backport latest changes from trunk. | 2017-03-22 | ||
| | | ||||
* | | [ci] Document that sudo: false is slower | 2017-03-10 | ||
| | | ||||
| * | [travis] Move GeoCoq to allow fail. | 2017-03-10 | ||
| | | | | | | | | We need to agree a bit more with upstream. | |||
* | | [travis] Move GeoCoq to allow fail. | 2017-03-09 | ||
| | | | | | | | | We need to agree a bit more with upstream. | |||
| * | [travis] Backport trunk's travis support. | 2017-03-02 | ||
| | ||||
* | [travis] [External CI] fiat-parsers | 2017-02-24 | ||
| | ||||
* | [travis] [External CI] CompCert official 8.6 support + UniMath | 2017-02-15 | ||
| | ||||
* | [travis] [External CI] GeoCoq | 2017-02-07 | ||
| | ||||
* | [travis] Enable 32bit test-suite + validate. | 2017-02-07 | ||
| | ||||
* | [travis] [External CI] C-Corn color coquelicot cpdt fiat-crypto floqc ↵ | 2017-02-07 | ||
| | | | | | | iris-coq math-classes sf - [TLC] [metacoq] not ready for 8.6 yet | |||
* | [travis] [External CI] Script renaming. | 2017-02-07 | ||
| | ||||
* | [travis] Improvements to main script | 2017-02-07 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | | - Add README.ci Suggestions and comments welcome. - Use the system compiler to get some boot speedup. - Build log folding. - Set NJOBS=2 (very moderate speedup) - Set language to a defined value. OPAM itself recommends C, so we follow suit. - Remove spurious `.opam`test No harm in testing we are in the right opam setting even if the cache did exist. Anyways, it seems that the previous was spurious, as it was testing if ~/coq/.opam did exists. I think the correct command would have been: ```shell [ -e ${HOME}/.opam ] || opam init ... ``` See the log at https://travis-ci.org/coq/coq/builds/198948812 for an example. | |||
* | [travis] [External CI] compcert HoTT math-comp | 2017-02-07 | ||
| | | | | | | - Improve the setup to support external contribs. We use a more minimalistic Coq build, gaining a few extra minutes. - [math-comp] workaround `make -j` bug to enable parallel building. | |||
* | [travis] Run tests using a parallel matrix. | 2017-02-06 | ||
| | | | | We also optimize `travis_wait` use. | |||
* | [travis] : more apt deps + parallel jobs + non-container based | 2017-02-04 | ||
| | ||||
* | [travis] CoqIde + doc + last available LST | 2017-02-04 | ||
| | ||||
* | Travis CI configuration. Runs validate & test-suite. | 2017-02-03 | ||