| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-27 | [travis] temporary UniMath overlay | Maxime Dénès | |
| We are waiting for an upstream merge of a fix related to coq_makefile2. | |||
| 2017-05-25 | Merge PR#481: [option] Remove support for non-synchronous options. | Maxime Dénès | |
| 2017-05-25 | Merge PR#406: coq makefile2 | Maxime Dénès | |
| 2017-05-25 | [location] [travis] Add overlays for located_switch | Emilio Jesus Gallego Arias | |
| 2017-05-24 | Merge branch 'trunk' into located_switch | Emilio Jesus Gallego Arias | |
| 2017-05-24 | [option] Remove support for non-synchronous options. | Emilio Jesus Gallego Arias | |
| Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers. | |||
| 2017-05-23 | Add parsers-examples target to fiat-parsers ci | Jason Gross | |
| This tests a bit more of fiat-parsers, adding an extra ~3 minutes to the build. | |||
| 2017-05-23 | overlay for UniMath | Enrico Tassi | |
| 2017-05-17 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-05-10 | Switch bedrock to mit-plv base | Jason Gross | |
| 2017-05-01 | Add bmsherman/topology to the ci | Jason Gross | |
| This development of @bmsherman tests universe polymorphism and setoid rewriting in type, and should build with v8.6 and trunk. | |||
| 2017-04-27 | Merge PR#568: Remove tactic compatibility layer | Maxime Dénès | |
| 2017-04-27 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-04-25 | [travis] mathcomp and fiat overlay for #402 | Emilio Jesus Gallego Arias | |
| 2017-04-24 | Adding a dedicated travis overlay for fiat-parsers. | Pierre-Marie Pédrot | |
| 2017-04-20 | Add bedrock targets src and facade | Jason Gross | |
| 2017-04-15 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-04-14 | [travis] Use the lite target for fiat-crypto. | Maxime Dénès | |
| 2017-04-07 | [travis] Overlay for PR#461: Camlp4 removal. | Emilio Jesus Gallego Arias | |
| 2017-03-24 | [travis] Backport from trunk: VST | Emilio Jesus Gallego Arias | |
| 2017-03-24 | [travis] Add VST | Emilio Jesus Gallego Arias | |
| 2017-03-22 | [travis] Fix iris-coq build. | Emilio Jesus Gallego Arias | |
| We need to do a bit of hacking, but it should be fine for the short term. c.f. https://gitlab.mpi-sws.org/FP/iris-coq/issues/83 | |||
| 2017-03-22 | [travis] [8.6.only] Backport latest changes from trunk. | Emilio Jesus Gallego Arias | |
| 2017-03-21 | trivial: fix comment | Matej Kosik | |
| 2017-03-13 | [travis] Basic support for overlays. | Emilio Jesus Gallego Arias | |
| We now allow the user to overlay contribution repositories and branches by adding their own rules to `ci-basic-overlay.sh`. This just provides very basic support. | |||
| 2017-03-10 | [travis] Make the git_checkout function more reliable. | Théo Zimmermann | |
| This commit also documents the behavior of said function; and fix the location of the ssreflect clone to an absolute path (this is now necessary). | |||
| 2017-03-10 | [travis] Adding a template file and using it for all targets. | Théo Zimmermann | |
| 2017-03-10 | [travis] Change headband for wider compatibility. | Théo Zimmermann | |
| 2017-03-10 | Improve build of travis target on local machine. | Théo Zimmermann | |
| - Move the git clones to a specific subfolder to avoid pollution. - Do not fail when git clone already exist (but make sure it is up-to-date). | |||
| 2017-03-10 | [travis] Move GeoCoq to allow fail. | Emilio Jesus Gallego Arias | |
| We need to agree a bit more with upstream. | |||
| 2017-03-09 | [travis] Move GeoCoq to allow fail. | Emilio Jesus Gallego Arias | |
| We need to agree a bit more with upstream. | |||
| 2017-03-02 | [travis] Backport trunk's travis support. | Emilio Jesus Gallego Arias | |
| 2017-02-24 | [travis] [External CI] fiat-parsers | Emilio Jesus Gallego Arias | |
| 2017-02-21 | [travis] track an 8.7 specific branch of HoTT. | Maxime Dénès | |
| This is required since we merged PR#309: Ltac as a plugin. | |||
| 2017-02-15 | [travis] [External CI] CompCert official 8.6 support + UniMath | Emilio Jesus Gallego Arias | |
| 2017-02-15 | [travis] [External CI] Factor out math-comp installs. | Emilio Jesus Gallego Arias | |
| We make math-comp overlays easier, we also start structuring the scripts a bit more. | |||
| 2017-02-07 | Merge PR#425: [travis] [External CI] [geocoq] don't build slow file | Maxime Dénès | |
| 2017-02-07 | [travis] [External CI] [geocoq] don't build slow file | Emilio Jesus Gallego Arias | |
| Unfortunately `Ch16_coordinates_with_functions.v` takes alone ~15 minutes which is too much for Travis. Pity, because it was a nice use case. | |||
| 2017-02-07 | [travis] [External CI] iris-coq: fix dependencies | Emilio Jesus Gallego Arias | |
| 2017-02-07 | [travis] [External CI] GeoCoq | Emilio Jesus Gallego Arias | |
| 2017-02-07 | [travis] Move ci files from `tools` to `dev`. | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |