aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
AgeCommit message (Collapse)Author
2017-06-15Merge PR#778: Revert "[travis] temporary UniMath overlay"Maxime Dénès
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-14[travis] overlay for fiat-crypto (a Require Import FunInd)Pierre Letouzey
2017-06-14[travis] overlays for CompCert and VST (an extra Require Export FunInd)Pierre Letouzey
2017-06-14[travis] fix Software Foundation (one added Require Extraction)Pierre Letouzey
2017-06-14[travis] fix CoLoR by inserting some Require Import FunIndPierre Letouzey
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] overlay for cornPierre Letouzey
2017-06-13[travis] extra test ci-bignums (+factorize other scripts)Pierre Letouzey
2017-06-13[travis] overlay + extra deps for math-classes (and formal-topology)Pierre Letouzey
2017-06-13[travis] adapt CoLoR compilation to depend on the bignum packagePierre 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-12add overlaysMatej Košík
2017-06-11Point ci-hott at a newer version of HoTTJason Gross
2017-06-08Mirror dpdgraph's travis test more accuratelyJason Gross
2017-06-08Remove coq-dpdgraph overlayJason Gross
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-08Remove overlay.Maxime Dénès
2017-06-07add overlaysMatej Košík
2017-06-06Overlay.Maxime Dénès
2017-06-06Remove some overlays.Maxime Dénès
2017-06-06Overlays.Maxime Dénès
2017-06-06Merge PR#723: [travis] [fiat] Test also fiat-core.Maxime Dénès
2017-06-02Add an overlay for coq-dpdgraph for 8.7Jason Gross
2017-06-02Add coq-dpdgraph CIJason Gross
2017-06-02[travis] [fiat] Test also fiat-core.Emilio Jesus Gallego Arias
I didn't rename the test file to `fiat` as IMHO it is not worth the noise.
2017-05-31Adding overlay for math-comp.Hugo Herbelin
2017-05-29Merge PR#687: Gitlab CIMaxime Dénès
2017-05-28Gitlab CIGaëtan Gilbert
2017-05-27[coqlib] Move `Coqlib` to `library/`.Emilio Jesus Gallego Arias
We move Coqlib to library in preparation for the late binding of Gallina-level references. Placing `Coqlib` in `library/` is convenient as some components such as pretyping need to depend on it. By moving we lose the ability to locate references by syntactic abbreviations, but IMHO it makes to require ML code to refer to a true constant instead of an abbreviation/notation. Unfortunately this change means that we break the `Coqlib` API (providing a compatibility function is not possible), however we do so for a good reason. The main changes are: - move `Coqlib` to `library/`. - remove reference -> term from `Coqlib`. In particular, clients will have different needs with regards to universes/evar_maps, so we force them to call the (not very safe) `Universes.constr_of_global` explicitly so the users are marked. - move late binding of impossible case from `Termops` to `pretying/Evarconv`. Remove hook. - `Coqlib.find_reference` doesn't support syntactic abbreviations anymore. - remove duplication of `Coqlib` code in `Program`. - remove duplication of `Coqlib` code in `Ltac.Rewrite`. - A special note about bug 5066 and commit 6e87877 . This case illustrates the danger of duplication in the code base; the solution chosen there was to transform the not-found anomaly into an error message, however the general policy was far from clear. The long term solution is indeed make `find_reference` emit `Not_found` and let the client handle the error maybe non-fatally. (so they can test for constants.
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-25Merge PR#481: [option] Remove support for non-synchronous options.Maxime Dénès
2017-05-25Merge PR#406: coq makefile2Maxime Dénès
2017-05-25[location] [travis] Add overlays for located_switchEmilio Jesus Gallego Arias
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-24[option] Remove support for non-synchronous options.Emilio Jesus Gallego Arias
Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers.
2017-05-23Add parsers-examples target to fiat-parsers ciJason Gross
This tests a bit more of fiat-parsers, adding an extra ~3 minutes to the build.
2017-05-23overlay for UniMathEnrico Tassi
2017-05-17Merge branch 'v8.6'Pierre-Marie Pédrot
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-27Merge PR#568: Remove tactic compatibility layerMaxime Dénès
2017-04-27Merge branch 'v8.6'Pierre-Marie Pédrot
2017-04-25[travis] mathcomp and fiat overlay for #402Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 02:12:43 +0000