aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-basic-overlay.sh
AgeCommit message (Collapse)Author
2019-03-28Use only lowercase for unimath in CI scriptsGaëtan Gilbert
Fix #9845
2019-03-05[CI] Add stdlib2Vincent Laporte
2019-02-04the default branch of Mtac2 changed to masterbeta
2019-01-11Merge pull request #8778 from SkySkimmer/merge-plugin-tutoYves Bertot
Move plugin tutorial to Coq repo
2019-01-08[ci] Update fiat-crypto legacyJason 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-08Integrate plugin tutorial after code importGaëtan Gilbert
2019-01-07Merge PR #9309: [ci] Add Verdi Raft with dependencies to CIEmilio Jesus Gallego Arias
2019-01-05[ci] Add Verdi Raft with dependencies to CIKarl Palmskog
2019-01-04Remove formal-topology from CIMaxime Dénès
This was suggested by the author. See https://github.com/bmsherman/topology/issues/23
2018-12-09fix copy-paste error in CI_ARCHIVEURLChristian Doczkal
2018-12-09add relation-algebra to CI test suiteChristian Doczkal
2018-12-05[ci] Add four color theorem proof to CIEmilio Jesus Gallego Arias
2018-12-04CI: track dev branch of coq-simple-ioYishuai Li
2018-11-21Remove pidetop from CIMaxime 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-13Merge PR #8976: CoqHammer CIGaëtan Gilbert
2018-11-12CoqHammer CILukasz Czajka
2018-11-10[ci] Add paramcoq to CI.Emilio Jesus Gallego Arias
2018-10-26Revert "[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.
2018-10-05CI: fix Iris and stdpp ref selectionGaëtan Gilbert
This was broken due to a typo when introducing the archive download method. We also remove default [master] values from basic-overlay which hid this issue.
2018-10-03Fix issue #8321 "Add more useful addons to the Windows Installer"Michael Soegtrop
Implemented by merging addon changes in V8.8.2 (keeping everything on master)
2018-10-01[ci] Add plugin-tutorial to CI.Emilio Jesus Gallego Arias
This closes #7618.
2018-08-31Download tarball instead of cloning external projects (when $CI is set).Théo Zimmermann
This allows to use fixed commits and not just branches or tags. We keep using git clone when $FORCE_GIT is set (for projects on gforge.inria.fr and projects pulling dependencies through git submodules). fiat-parsers also calls git submodule, but inside its own Makefile.
2018-08-31[ci] Fix QuickChick by adding new simple-io dependency.Théo Zimmermann
2018-06-27Add mit-plv/bedrock2-ci to CIAndres Erbsen
2018-06-25Reuse CI info to know which version of plugins to build on Windows.Théo Zimmermann
2018-06-21Update dpdgraph branch nameGaëtan Gilbert
See https://github.com/Karmaki/coq-dpdgraph/issues/50 for context
2018-06-02QuickChick CILeonidas Lampropoulos
2018-05-16[ci] Don't build lite versions of CI developments.Emilio Jesus Gallego Arias
In the original Travis CI setup, the per-job time limit was an issue. However, Gitlab has much improved this problem due to a) Coq not being built for each contrib, b) user-configurable time limit. We thus disable the expensive builds from Travis: `fiat-crypto`, `formal-topology`, `geocoq`, `iris-lambda-rust`, `math-comp`, `unimath`, `vst` and instruct Gitlab to build [`geocoq`, `math-comp`, `unimath`, `vst`] in full. We also update the `math-comp` script as the `odd-order` theorem lives in a separate repository and it is a key CI case.
2018-05-09[ci] Add mit-plv/cross-cryptoJason Gross
I followed the code for fiat-crypto / fiat-parsers. I hope I didn't miss anything.
2018-05-02[ci]: add pidetop (fix #7336)Enrico Tassi
2018-04-25updating CI for Mtac2Beta Ziliani
2018-04-20CI: add fcsl-pcmAnton Trunov
2018-04-13Update the CI branch for Equations.Théo Zimmermann
2018-02-19ci: add elpiEnrico Tassi
2018-02-05Points to Flocq official repository.Théo Zimmermann
Following comment at https://github.com/coq/coq/pull/6596#issuecomment-358246528.
2018-01-16Source basic overlay before user overlays.Gaëtan Gilbert
2017-12-07[ci] CoLoR has moved to githubEmilio Jesus Gallego Arias
Closes #6194 .
2017-11-20Add Equations to CIMatthieu Sozeau
2017-11-13Merge PR #6071: [ci] Add Ltac2Maxime Dénès
2017-11-04[ci] Add Ltac2Jason Gross
2017-10-30[ci] Switch VST back to upstream.Théo Zimmermann
This finally closes #5994.
2017-10-27[ci] Switch back to upstream version of Math-Classes and Corn.Théo Zimmermann
2017-10-25Merge PR #6003: Point HoTT back at master, which now supports Coq masterMaxime Dénès
2017-10-23Point HoTT back at master, which now supports Coq masterJason Gross
2017-10-20Switch testing branch back to CompCert upstream.Théo Zimmermann
This follows the merge of AbsInt/CompCert#191.
2017-10-19CI: build lambdaRust (which depends on Iris) rather than just IrisRalf Jung
2017-10-04[ci] Remove temporary bignums overlay.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 07:32:30 +0000