aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-basic-overlay.sh
AgeCommit message (Collapse)Author
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
2017-09-07Merge PR #914: Making the detyper lazyMaxime Dénès
2017-09-05Fix Software Foundations build.Maxime Dénès
The Software Foundations archive has been replaced by three volumes.
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager.
2017-07-28Merge PR #782: Update API for fiatMaxime Dénès
2017-07-18[ci] VST is now built with IGNORECOQVERSION=true.Théo Zimmermann
2017-07-04Revert fiat-crypto overlayJason Gross
Not a useful overlay. Fiat-crypto has since been updated to pass -compat 8.6.
2017-06-15Merge PR#778: Revert "[travis] temporary UniMath overlay"Maxime Dénès
2017-06-15Update fiat-parsers overlayJason Gross
2017-06-15Remove bedrock from test suite.Maxime Dénès
Bedrock relies on the 8.4 compat flag that we are removing, and we heard from MIT that they did not plan to port bedrock to more recent versions of Coq.
2017-06-14Merge PR#771: [travis overlay] Partially Revert 013c0232953f1f58Maxime Dénès
2017-06-14Temporary overlays because fewer plugins are loaded at startup.Maxime Dénès
2017-06-14Temporary overlays for bignums.Maxime Dénès
2017-06-13Revert "[travis] temporary UniMath overlay"Théo Zimmermann
This reverts commit 7ca4e36af8a12236a618bd3a8d045439df40dd43. Not necessary anymore since UniMath/UniMath#715 has been merged.
2017-06-13[travis] extra test ci-bignums (+factorize other scripts)Pierre Letouzey
2017-06-13Merge PR#764: Point ci-hott at a newer version of HoTTMaxime Dénès
2017-06-12Merge PR#715: Add coq-dpdgraph ciMaxime Dénès
2017-06-12[travis overlay] Partially Revert 013c0232953f1f58Jason Gross
I've pushed commits which add `-bypass-API` to bedrock in the proper way, so these overlays are no longer needed
2017-06-12Temporary overlay, waiting for upstream PR merges.Maxime Dénès
2017-06-11Point ci-hott at a newer version of HoTTJason Gross
2017-06-08Remove coq-dpdgraph overlayJason Gross
2017-06-02Add an overlay for coq-dpdgraph for 8.7Jason Gross
2017-06-02Add coq-dpdgraph CIJason Gross
2017-05-27[travis] temporary UniMath overlayMaxime Dénès
We are waiting for an upstream merge of a fix related to coq_makefile2.
2017-05-10Switch bedrock to mit-plv baseJason Gross
2017-05-01Add bmsherman/topology to the ciJason Gross
This development of @bmsherman tests universe polymorphism and setoid rewriting in type, and should build with v8.6 and trunk.
2017-04-20Add bedrock targets src and facadeJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 06:38:25 +0000