| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-05-19 | [ci] Add mit-plv/engine-bench | Jason Gross | |
| This is a new development where I'm aggregating a specific set of benchmarks. It's intended to be relatively lightweight, taking only a handful of minutes. It's probably one of the few developments currently testing Ltac2. | |||
| 2020-05-14 | [ci] [sf] Fix SF build. | Emilio Jesus Gallego Arias | |
| We move from the previous complex CI download setup to a much more straightforward public mirror repository. Thanks to Yishuai Li and Benjamin Pierce for the very quick response. Closes #12290 | |||
| 2020-04-30 | renaming in Makefile.ci and ci scripts to avoid inconsistencies | Olivier Laurent | |
| 2020-04-29 | Merge PR #12198: CI: change ext-lib url, it is at coq-community now | Emilio Jesus Gallego Arias | |
| Reviewed-by: Zimmi48 Reviewed-by: ejgallego | |||
| 2020-04-29 | CI: ext-lib is at coq-community now | Antonio Nikishaev | |
| 2020-04-27 | [ci] Add coq-tools to the CI | Jason Gross | |
| After #12023 broke the bug minimizer, I'd like to add [coq-tools](https://github.com/JasonGross/coq-tools/) to the CI. It's relatively light-weight (under 5 minutes, I believe), and I'd like to know when it's going to break on master before it's broken, rather than after. It tests a relatively under-tested part of Coq, mostly (the display output of error message, by and large), and I'm happy to take responsibility for fixing it when some PR is going to break it (mainly I just want a sort-of early warning system, and I want PRs to not accidentally break it by changing things that they don't realize they're changing). | |||
| 2020-03-26 | [ci] Add bbv | Jason Gross | |
| I believe a recent commit to master broke it, and now that it's no longer tested as part of fiat-crypto-legacy, I think it's time to add it. | |||
| 2020-03-23 | [ci] add metacoq | Matthieu Sozeau | |
| 2020-03-11 | Update dev/ci/ci-basic-overlay.sh | Enrico Tassi | |
| Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | |||
| 2020-03-11 | [CI] test hierarchy builder as part of elpi | Enrico Tassi | |
| 2020-02-11 | Remove fiat-crypto-legacy from CI | Maxime Dénès | |
| 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. | |||
| 2020-02-07 | restore the default URL for coquelicot | Yves Bertot | |
| 2020-01-28 | Add reduction-effects to the CI | Jason Gross | |
| 2020-01-17 | Fix issue #11396 : Rlist hides standard list constructors cons and nil | Michael Soegtrop | |
| 2020-01-08 | let CI test bedrock2's 'tested' branch instead of 'master' | Samuel Gruetter | |
| 2019-12-02 | [CI] Test latest artifacts of SF instead of the stable version | Maxime Dénès | |
| 2019-11-27 | [ci] Split out the dependencies of fiat-crypto | Jason Gross | |
| 2019-11-21 | add tlc to ci; please proof read very carefully and test. thanks | charguer | |
| 2019-09-20 | [ci] Add mit-pdos/perennial | Tej Chajed | |
| 2019-08-19 | Std++, Iris, and Lambda-Rust have moved. | Théo Zimmermann | |
| We update the URLs to the new ones, even if the previous continue to work. | |||
| 2019-07-29 | Fix issue #10593 : Software foundations URL changed | Michael Soegtrop | |
| 2019-07-16 | Fix #9351 in master (Add Flocq, CoqInterval, Gappa tool and Gappa) | Michael Soegtrop | |
| 2019-06-07 | simple IO CI branch is now `master` | Gaëtan Gilbert | |
| 2019-05-10 | Merge PR #9854: Improve field_simplify on fractions with constant denominator | Michael Soegtrop | |
| Reviewed-by: MSoegtropIMC Ack-by: Zimmi48 Reviewed-by: amahboubi Reviewed-by: vbgl | |||
| 2019-05-09 | Switched Coquelicot CI URLs from INRIA gforge to INRIA gitlab | Michael Soegtrop | |
| 2019-05-07 | Remove ppedrot/ltac2 from CI after integration in main repo | Gaëtan Gilbert | |
| 2019-04-24 | [coq_makefile] Enforce warn_error for plugins. | Emilio Jesus Gallego Arias | |
| The amount of dangerous warnings in plugins is out of hand, including some very serious ones. As Coq developers are maintaining plugins these days it makes sense to require the contributions to follow the same coding discipline as in the main tree, thus we require the set of warnings fatal warnings to be the same in Coq and in plugins. We don't mark deprecation as fatal as to allow time for migration. Fixes #6974 | |||
| 2019-04-01 | [CI] Coquelicot: use “master” development version | Vincent Laporte | |
| 2019-03-31 | CI: add mit-pdos/argosy | Tej Chajed | |
| 2019-03-28 | Use only lowercase for unimath in CI scripts | Gaëtan Gilbert | |
| Fix #9845 | |||
| 2019-03-05 | [CI] Add stdlib2 | Vincent Laporte | |
| 2019-02-04 | the default branch of Mtac2 changed to master | beta | |
| 2019-01-11 | Merge pull request #8778 from SkySkimmer/merge-plugin-tuto | Yves Bertot | |
| Move plugin tutorial to Coq repo | |||
| 2019-01-08 | [ci] Update fiat-crypto legacy | Jason Gross | |
| 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.) | |||
| 2019-01-08 | Integrate plugin tutorial after code import | Gaëtan Gilbert | |
| 2019-01-07 | Merge PR #9309: [ci] Add Verdi Raft with dependencies to CI | Emilio Jesus Gallego Arias | |
| 2019-01-05 | [ci] Add Verdi Raft with dependencies to CI | Karl Palmskog | |
| 2019-01-04 | Remove formal-topology from CI | Maxime Dénès | |
| This was suggested by the author. See https://github.com/bmsherman/topology/issues/23 | |||
| 2018-12-09 | fix copy-paste error in CI_ARCHIVEURL | Christian Doczkal | |
| 2018-12-09 | add relation-algebra to CI test suite | Christian Doczkal | |
| 2018-12-05 | [ci] Add four color theorem proof to CI | Emilio Jesus Gallego Arias | |
| 2018-12-04 | CI: track dev branch of coq-simple-io | Yishuai Li | |
| 2018-11-21 | Remove pidetop from CI | Maxime Dénès | |
| pidetop relies on some rather low level API from STM, which we'd like to change. It does not seem maintained much anymore, and still hasn't moved to github. | |||
| 2018-11-17 | [ci] Uniformize casing of makefile targets and ci variables. | Emilio Jesus Gallego Arias | |
| This is convenient as to have better automation. | |||
| 2018-11-13 | Merge PR #8976: CoqHammer CI | Gaëtan Gilbert | |
| 2018-11-12 | CoqHammer CI | Lukasz Czajka | |
| 2018-11-10 | [ci] Add paramcoq to CI. | Emilio Jesus Gallego Arias | |
| 2018-10-26 | Revert "[ci] Pin CI_REF to plugin_tutorial to use not yet merged commit." | Gaëtan Gilbert | |
| This reverts commit df69c44af03f2587b3f1706a805d0e2728c1f1dc. Should be merged before any PR with plugin tutorial overlays, or we can just merge the vendor PR instead. | |||
| 2018-10-18 | [ci] Pin CI_REF to plugin_tutorial to use not yet merged commit. | Théo Zimmermann | |
| This fixes the CI until this commit is merged into master. | |||
| 2018-10-08 | [ci] Add aac-tactics. | Théo Zimmermann | |
| And fix a typo that was previously there. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |