aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci/ci-basic-overlay.sh
Commit message (Collapse)AuthorAge
* Add mit-plv/bedrock2-ci to CIGravatar Andres Erbsen2018-06-27
|
* Reuse CI info to know which version of plugins to build on Windows.Gravatar Théo Zimmermann2018-06-25
|
* Update dpdgraph branch nameGravatar Gaëtan Gilbert2018-06-21
| | | | See https://github.com/Karmaki/coq-dpdgraph/issues/50 for context
* QuickChick CIGravatar Leonidas Lampropoulos2018-06-02
|
* [ci] Don't build lite versions of CI developments.Gravatar Emilio Jesus Gallego Arias2018-05-16
| | | | | | | | | | | | | | | | | | | 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.
* [ci] Add mit-plv/cross-cryptoGravatar Jason Gross2018-05-09
| | | | | I followed the code for fiat-crypto / fiat-parsers. I hope I didn't miss anything.
* [ci]: add pidetop (fix #7336)Gravatar Enrico Tassi2018-05-02
|
* updating CI for Mtac2Gravatar Beta Ziliani2018-04-25
|
* CI: add fcsl-pcmGravatar Anton Trunov2018-04-20
|
* Update the CI branch for Equations.Gravatar Théo Zimmermann2018-04-13
|
* ci: add elpiGravatar Enrico Tassi2018-02-19
|
* Points to Flocq official repository.Gravatar Théo Zimmermann2018-02-05
| | | | Following comment at https://github.com/coq/coq/pull/6596#issuecomment-358246528.
* Source basic overlay before user overlays.Gravatar Gaëtan Gilbert2018-01-16
|
* [ci] CoLoR has moved to githubGravatar Emilio Jesus Gallego Arias2017-12-07
| | | | Closes #6194 .
* Add Equations to CIGravatar Matthieu Sozeau2017-11-20
|
* Merge PR #6071: [ci] Add Ltac2Gravatar Maxime Dénès2017-11-13
|\
| * [ci] Add Ltac2Gravatar Jason Gross2017-11-04
| |
* | [ci] Switch VST back to upstream.Gravatar Théo Zimmermann2017-10-30
|/ | | | This finally closes #5994.
* [ci] Switch back to upstream version of Math-Classes and Corn.Gravatar Théo Zimmermann2017-10-27
|
* Merge PR #6003: Point HoTT back at master, which now supports Coq masterGravatar Maxime Dénès2017-10-25
|\
| * Point HoTT back at master, which now supports Coq masterGravatar Jason Gross2017-10-23
| |
* | Switch testing branch back to CompCert upstream.Gravatar Théo Zimmermann2017-10-20
| | | | | | | | This follows the merge of AbsInt/CompCert#191.
* | CI: build lambdaRust (which depends on Iris) rather than just IrisGravatar Ralf Jung2017-10-19
|/
* [ci] Remove temporary bignums overlay.Gravatar Théo Zimmermann2017-10-04
|
* Merge PR #914: Making the detyper lazyGravatar Maxime Dénès2017-09-07
|\
* | Fix Software Foundations build.Gravatar Maxime Dénès2017-09-05
| | | | | | | | The Software Foundations archive has been replaced by three volumes.
| * Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
|/ | | | | | | | | | | | | | | | | | | 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.
* Merge PR #782: Update API for fiatGravatar Maxime Dénès2017-07-28
|\
* | [ci] VST is now built with IGNORECOQVERSION=true.Gravatar Théo Zimmermann2017-07-18
| |
* | Revert fiat-crypto overlayGravatar Jason Gross2017-07-04
| | | | | | | | | | Not a useful overlay. Fiat-crypto has since been updated to pass -compat 8.6.
* | Merge PR#778: Revert "[travis] temporary UniMath overlay"Gravatar Maxime Dénès2017-06-15
|\ \
| | * Update fiat-parsers overlayGravatar Jason Gross2017-06-15
| |/ |/|
* | Remove bedrock from test suite.Gravatar Maxime Dénès2017-06-15
| | | | | | | | | | | | 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.
* | Merge PR#771: [travis overlay] Partially Revert 013c0232953f1f58Gravatar Maxime Dénès2017-06-14
|\ \
* | | Temporary overlays because fewer plugins are loaded at startup.Gravatar Maxime Dénès2017-06-14
| | |
* | | Temporary overlays for bignums.Gravatar Maxime Dénès2017-06-14
| | |
| | * Revert "[travis] temporary UniMath overlay"Gravatar Théo Zimmermann2017-06-13
| | | | | | | | | | | | | | | | | | This reverts commit 7ca4e36af8a12236a618bd3a8d045439df40dd43. Not necessary anymore since UniMath/UniMath#715 has been merged.
* | | [travis] extra test ci-bignums (+factorize other scripts)Gravatar Pierre Letouzey2017-06-13
| |/ |/|
* | Merge PR#764: Point ci-hott at a newer version of HoTTGravatar Maxime Dénès2017-06-13
|\ \
* \ \ Merge PR#715: Add coq-dpdgraph ciGravatar Maxime Dénès2017-06-12
|\ \ \
| | | * [travis overlay] Partially Revert 013c0232953f1f58Gravatar Jason Gross2017-06-12
| |_|/ |/| | | | | I've pushed commits which add `-bypass-API` to bedrock in the proper way, so these overlays are no longer needed
* | | Temporary overlay, waiting for upstream PR merges.Gravatar Maxime Dénès2017-06-12
| | |
| | * Point ci-hott at a newer version of HoTTGravatar Jason Gross2017-06-11
| |/ |/|
| * Remove coq-dpdgraph overlayGravatar Jason Gross2017-06-08
| |
| * Add an overlay for coq-dpdgraph for 8.7Gravatar Jason Gross2017-06-02
| |
| * Add coq-dpdgraph CIGravatar Jason Gross2017-06-02
|/
* [travis] temporary UniMath overlayGravatar Maxime Dénès2017-05-27
| | | | We are waiting for an upstream merge of a fix related to coq_makefile2.
* Switch bedrock to mit-plv baseGravatar Jason Gross2017-05-10
|
* Add bmsherman/topology to the ciGravatar Jason Gross2017-05-01
| | | | | This development of @bmsherman tests universe polymorphism and setoid rewriting in type, and should build with v8.6 and trunk.
* Add bedrock targets src and facadeGravatar Jason Gross2017-04-20
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 04:40:43 +0000