aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci
Commit message (Collapse)AuthorAge
* Merge PR#778: Revert "[travis] temporary UniMath overlay"Gravatar Maxime Dénès2017-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
| | |
* | | [travis] overlay for fiat-crypto (a Require Import FunInd)Gravatar Pierre Letouzey2017-06-14
| | |
* | | [travis] overlays for CompCert and VST (an extra Require Export FunInd)Gravatar Pierre Letouzey2017-06-14
| | |
* | | [travis] fix Software Foundation (one added Require Extraction)Gravatar Pierre Letouzey2017-06-14
| | |
* | | [travis] fix CoLoR by inserting some Require Import FunIndGravatar Pierre Letouzey2017-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] overlay for cornGravatar Pierre Letouzey2017-06-13
| | |
* | | [travis] extra test ci-bignums (+factorize other scripts)Gravatar Pierre Letouzey2017-06-13
| | |
* | | [travis] overlay + extra deps for math-classes (and formal-topology)Gravatar Pierre Letouzey2017-06-13
| | |
* | | [travis] adapt CoLoR compilation to depend on the bignum packageGravatar 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
| | |
* | | add overlaysGravatar Matej Košík2017-06-12
| | |
| | * Point ci-hott at a newer version of HoTTGravatar Jason Gross2017-06-11
| |/ |/|
| * Mirror dpdgraph's travis test more accuratelyGravatar Jason Gross2017-06-08
| |
| * Remove coq-dpdgraph overlayGravatar Jason Gross2017-06-08
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\ \
* | | Remove overlay.Gravatar Maxime Dénès2017-06-08
| | |
* | | add overlaysGravatar Matej Košík2017-06-07
| | |
* | | Overlay.Gravatar Maxime Dénès2017-06-06
| | |
* | | Remove some overlays.Gravatar Maxime Dénès2017-06-06
| | |
* | | Overlays.Gravatar Maxime Dénès2017-06-06
| | |
* | | Merge PR#723: [travis] [fiat] Test also fiat-core.Gravatar Maxime Dénès2017-06-06
|\ \ \
| | | * Add an overlay for coq-dpdgraph for 8.7Gravatar Jason Gross2017-06-02
| | | |
| | | * Add coq-dpdgraph CIGravatar Jason Gross2017-06-02
| | | |
| * | | [travis] [fiat] Test also fiat-core.Gravatar Emilio Jesus Gallego Arias2017-06-02
| | |/ | |/| | | | | | | I didn't rename the test file to `fiat` as IMHO it is not worth the noise.
* / | Adding overlay for math-comp.Gravatar Hugo Herbelin2017-05-31
|/ /
* | Merge PR#687: Gitlab CIGravatar Maxime Dénès2017-05-29
|\ \
| * | Gitlab CIGravatar Gaëtan Gilbert2017-05-28
| | |
* | | [coqlib] Move `Coqlib` to `library/`.Gravatar Emilio Jesus Gallego Arias2017-05-27
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | [travis] temporary UniMath overlayGravatar Maxime Dénès2017-05-27
| | | | | | | | We are waiting for an upstream merge of a fix related to coq_makefile2.
* | Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\ \
* \ \ Merge PR#406: coq makefile2Gravatar Maxime Dénès2017-05-25
|\ \ \
* | | | [location] [travis] Add overlays for located_switchGravatar Emilio Jesus Gallego Arias2017-05-25
| | | |
* | | | Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \ \ \
| | | * | [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| | |/ / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | * Add parsers-examples target to fiat-parsers ciGravatar Jason Gross2017-05-23
| | | | | | | | | | | | This tests a bit more of fiat-parsers, adding an extra ~3 minutes to the build.
| | * | overlay for UniMathGravatar Enrico Tassi2017-05-23
| |/ /
| * | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-05-17
| |\|
| | * 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.
| * | Merge PR#568: Remove tactic compatibility layerGravatar Maxime Dénès2017-04-27
| |\ \
| * \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-04-27
| |\ \ \ | | | |/ | | |/|
* | / | [travis] mathcomp and fiat overlay for #402Gravatar Emilio Jesus Gallego Arias2017-04-25
|/ / /