aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-basic-overlay.sh
AgeCommit message (Collapse)Author
2021-04-21Add mczify to CIKazuhiko Sakaguchi
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-03-24iris_string_ident is no longer neededRalf Jung
2021-03-11Add deriving lib to CI.Arthur Azevedo de Amorim
2020-12-30[ci] Switch to testing the maintenance branch for Flocq 3.Théo Zimmermann
This is the version that CompCert will be compatible with for the time being.
2020-12-16Merge PR #13644: Fix overlay system: projects need to be loaded before overlays.coqbot-app[bot]
Reviewed-by: gares
2020-12-16Fix overlay system: projects need to be loaded before overlays.Gaëtan Gilbert
Also fixes is_in_projects
2020-12-15Merge PR #13633: [ci] uniform name of projects w.r.t. opam packagescoqbot-app[bot]
Reviewed-by: ejgallego
2020-12-15[ci] uniform name of projects w.r.t. opam packagesEnrico Tassi
This makes it easier to track projects across Coq's CI and the platform
2020-12-14[ci] fix code to check if the overlay is validEnrico Tassi
2020-12-10[ci] update url of autosubstEnrico Tassi
2020-12-09[ci] function to declare projectsEnrico Tassi
incidentally the "projects" array can be queried to get the list of projects
2020-11-25[ci] job for menhirEnrico Tassi
2020-09-02CI: build Iris examples instead of lambda-RustRalf Jung
2020-07-21Add Coqtail to CIwhonore
2020-06-24Add back fiat-crypto-legacy to the CIJason Gross
This partially reverts commit 35a1cc4f5c708b745a2810a64d220f49eff4beca. (I've not added back the nix things, since I'm not sure what purpose they serve, and I've adjusted the targets slightly.) The CI build should no longer take an enormously long time to start, and fiat-crypto-legacy code is actively being used to track down memory issues in #12487. Additionally, f-c-l revealed a genuine bug in #7825, and so I'd like to keep f-c-l in the CI at least until #7825 is finished. I've been maintaining compatibility of f-c-l with master anyway on the side, in part to continue some performance experiments with it, and expect to continue to do so at least until the end of this calendar year, and it'd be nice for me to get advance warning when a PR is going to break it on master. (It seems reasonable to me to take it off the CI again once I'm no longer maintaining it / collecting data from it, and / or once #7825 is finished.)
2020-06-23[ci] Add coq-community/coq-performance-testsJason Gross
It's tested on the bench, so might as well test it on the CI. Hopefully it's not too memory-heavy. (It should only take a couple of minutes, time-wise.)
2020-06-17[ci] Use a tested branch of PerennialTej Chajed
2020-06-15updated ci for unicoqbeta
2020-06-10Windows: fix menhir and coq-menhirlib build for latest version.Michael Soegtrop
2020-06-08[ci] [overlays] Pin unicoq to a stable version.Emilio Jesus Gallego Arias
Following upstream advice.
2020-05-19[ci] Add mit-plv/engine-benchJason 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-30renaming in Makefile.ci and ci scripts to avoid inconsistenciesOlivier Laurent
2020-04-29Merge PR #12198: CI: change ext-lib url, it is at coq-community nowEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2020-04-29CI: ext-lib is at coq-community nowAntonio Nikishaev
2020-04-27[ci] Add coq-tools to the CIJason 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 bbvJason 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 metacoqMatthieu Sozeau
2020-03-11Update dev/ci/ci-basic-overlay.shEnrico Tassi
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-03-11[CI] test hierarchy builder as part of elpiEnrico Tassi
2020-02-11Remove fiat-crypto-legacy from CIMaxime 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-07restore the default URL for coquelicotYves Bertot
2020-01-28Add reduction-effects to the CIJason Gross
2020-01-17Fix issue #11396 : Rlist hides standard list constructors cons and nilMichael Soegtrop
2020-01-08let CI test bedrock2's 'tested' branch instead of 'master'Samuel Gruetter
2019-12-02[CI] Test latest artifacts of SF instead of the stable versionMaxime Dénès
2019-11-27[ci] Split out the dependencies of fiat-cryptoJason Gross
2019-11-21add tlc to ci; please proof read very carefully and test. thankscharguer
2019-09-20[ci] Add mit-pdos/perennialTej Chajed
2019-08-19Std++, 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-29Fix issue #10593 : Software foundations URL changedMichael Soegtrop
2019-07-16Fix #9351 in master (Add Flocq, CoqInterval, Gappa tool and Gappa)Michael Soegtrop
2019-06-07simple IO CI branch is now `master`Gaëtan Gilbert
2019-05-10Merge PR #9854: Improve field_simplify on fractions with constant denominatorMichael Soegtrop
Reviewed-by: MSoegtropIMC Ack-by: Zimmi48 Reviewed-by: amahboubi Reviewed-by: vbgl
2019-05-09Switched Coquelicot CI URLs from INRIA gforge to INRIA gitlabMichael Soegtrop
2019-05-07Remove ppedrot/ltac2 from CI after integration in main repoGaë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 versionVincent Laporte
2019-03-31CI: add mit-pdos/argosyTej Chajed
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:19:06 +0000