Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | [travis] Move GeoCoq to allow fail. | Emilio Jesus Gallego Arias | 2017-03-10 | |
| | | | | | | | | We need to agree a bit more with upstream. | |||
* | | [travis] Move GeoCoq to allow fail. | Emilio Jesus Gallego Arias | 2017-03-09 | |
| | | | | | | | | We need to agree a bit more with upstream. | |||
| * | [travis] Backport trunk's travis support. | Emilio Jesus Gallego Arias | 2017-03-02 | |
| | ||||
* | [travis] [External CI] fiat-parsers | Emilio Jesus Gallego Arias | 2017-02-24 | |
| | ||||
* | [travis] [External CI] CompCert official 8.6 support + UniMath | Emilio Jesus Gallego Arias | 2017-02-15 | |
| | ||||
* | [travis] [External CI] GeoCoq | Emilio Jesus Gallego Arias | 2017-02-07 | |
| | ||||
* | [travis] Enable 32bit test-suite + validate. | Emilio Jesus Gallego Arias | 2017-02-07 | |
| | ||||
* | [travis] [External CI] C-Corn color coquelicot cpdt fiat-crypto floqc ↵ | Emilio Jesus Gallego Arias | 2017-02-07 | |
| | | | | | | iris-coq math-classes sf - [TLC] [metacoq] not ready for 8.6 yet | |||
* | [travis] [External CI] Script renaming. | Emilio Jesus Gallego Arias | 2017-02-07 | |
| | ||||
* | [travis] Improvements to main script | Emilio Jesus Gallego Arias | 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 | Emilio Jesus Gallego Arias | 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. | Emilio Jesus Gallego Arias | 2017-02-06 | |
| | | | | We also optimize `travis_wait` use. | |||
* | [travis] : more apt deps + parallel jobs + non-container based | Pierre-Yves Strub | 2017-02-04 | |
| | ||||
* | [travis] CoqIde + doc + last available LST | Pierre-Yves Strub | 2017-02-04 | |
| | ||||
* | Travis CI configuration. Runs validate & test-suite. | Pierre-Yves Strub | 2017-02-03 | |