aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
AgeCommit message (Collapse)Author
2020-06-05Merge PR #12397: Fix #12280: do not use xindy to avoid build failures on ↵Emilio Jesus Gallego Arias
some machines. Reviewed-by: SkySkimmer Reviewed-by: cpitclaudel
2020-05-31[ci] Split fiat-crypto into non-OCaml and OCamlJason Gross
Note that this should reduce the overall build time of fiat-crypto related targets by about 10--20 minutes, as I've removed the heaviest jobs (about 25--30 minutes in serial) from the OCaml target. I'd like to keep the OCaml target around just to make sure that Coq doesn't introduce a change to extraction that breaks compilation of extracted OCaml code. See https://github.com/ocaml/ocaml/issues/7826 for the issue tracking performance of compiling the extracted OCaml code (and perhaps there should be another issue opened on the OCaml bug tracker about flambda on the fiat-crypto extracted files?) Alternative to #12405 Closes #12405 Fixes #12400
2020-05-26Fix #12280: do not use xindy to avoid build failures on some machines.Théo Zimmermann
2020-05-21Merge PR #12364: [ci] [docker] Bump ocamlformat and duneGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: vbgl
2020-05-20Merge PR #12359: [ci] Add mit-plv/engine-benchGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-20Merge PR #12342: Direct URL for triggering a pipeline with SKIP_DOCKER=false.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: jfehrle
2020-05-19[ci] Add mit-plv/engine-benchJason Gross
This is a new development where I'm aggregating a specific set of benchmarks. It's intended to be relatively lightweight, taking only a handful of minutes. It's probably one of the few developments currently testing Ltac2.
2020-05-19[ci] [docker] Bump ocamlformat and duneEmilio Jesus Gallego Arias
cc: #12350
2020-05-19Merge PR #12224: Support :gdef:`text<term>` syntax (adding "<term>")Clément Pit-Claudel
Reviewed-by: Zimmi48 Reviewed-by: cpitclaudel
2020-05-18Bump minimal versions of refman dependencies.Théo Zimmermann
Fixes #11936. Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
2020-05-18[ci] Old overlay cleanup.Emilio Jesus Gallego Arias
2020-05-18Direct URL for triggering a pipeline with SKIP_DOCKER=false.Théo Zimmermann
2020-05-16[ci] [azure] Rework windows Azure pipelineEmilio Jesus Gallego Arias
- use a different mirror for main cygwin archive - (always) publish build log as artifact - fix call to dune makefiles - we do just build Coq for now, as: + dune is rebuilding Coq to run the test-suite, this needs move investigation. + the test suite seems to take long and it times-out on Win.
2020-05-16Merge PR #8855: More search optionsEmilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: kyoDralliam
2020-05-16Merge PR #11566: [misc] Better preserve backtraces in several modulesPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-05-15Add overlays for coqhammer and coq-dpdgraph.Hugo Herbelin
2020-05-15Merge PR #11948: Hexadecimal numeralsHugo Herbelin
Reviewed-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin
2020-05-15Merge PR #12032: [win] Elpi, Coq-Elpi and HBMichael Soegtrop
Reviewed-by: MSoegtropIMC
2020-05-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
Re-raising inside exception handlers must be done with care in order to preserve backtraces; even if newer OCaml versions do a better job in automatically spilling `%reraise` in places that matter, there is no guarantee for that to happen. I've done a best-effort pass of places that were re-raising incorrectly, hopefully I got the logic right. There is the special case of `Nametab.error_global_not_found` which is raised many times in response to a `Not_found` error; IMHO this error should be converted to something more specific, however the scope of that change would be huge as to do easily...
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
Reviewed-by: Matafou Ack-by: SkySkimmer Reviewed-by: gares
2020-05-14[ci] [sf] Fix SF build.Emilio Jesus Gallego Arias
We move from the previous complex CI download setup to a much more straightforward public mirror repository. Thanks to Yishuai Li and Benjamin Pierce for the very quick response. Closes #12290
2020-05-13Overlay elpiHugo Herbelin
2020-05-10Add overlays.Pierre-Marie Pédrot
2020-05-09Add overlaysPierre Roux
2020-05-07[win] CI build addons Coq-Elpi Hierarchy-BuilderEnrico Tassi
2020-05-07[ci] overlay for coq-elpiEnrico Tassi
2020-05-06[ci] bump elpi to 1.11Enrico Tassi
2020-05-05Merge PR #12227: Spring cleaning of the tactic compatibility layerEnrico Tassi
Reviewed-by: gares
2020-05-04update documentation for overlay buildingOlivier Laurent
2020-05-03Add overlays.Pierre-Marie Pédrot
2020-05-01Merge PR #12217: Fix #12215: ci scripts naming inconsistenciesEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-30renaming in Makefile.ci and ci scripts to avoid inconsistenciesOlivier Laurent
2020-04-30Merge PR #12107: Remove mod_constraints field of module bodyPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-29Merge PR #12198: CI: change ext-lib url, it is at coq-community nowEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2020-04-29Merge PR #12174: [ci] Add coq-tools to the CIThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-29correct script name create_overlays.shOlivier Laurent
2020-04-29CI: ext-lib is at coq-community nowAntonio Nikishaev
2020-04-27[ci] Add coq-tools to the CIJason Gross
After #12023 broke the bug minimizer, I'd like to add [coq-tools](https://github.com/JasonGross/coq-tools/) to the CI. It's relatively light-weight (under 5 minutes, I believe), and I'd like to know when it's going to break on master before it's broken, rather than after. It tests a relatively under-tested part of Coq, mostly (the display output of error message, by and large), and I'm happy to take responsibility for fixing it when some PR is going to break it (mainly I just want a sort-of early warning system, and I want PRs to not accidentally break it by changing things that they don't realize they're changing).
2020-04-21Overlay for fiat-crypto, Mtac2, MetaCoq and UniMath.Hugo Herbelin
2020-04-21Adding a Declare ML Module in empty file Ltac.v.Hugo Herbelin
Indeed, it would be intuitive that `Require Import Ltac` is an equivalent for Ltac of `Require Import Ltac2.Ltac2`. Also declaring the classic proof mode.
2020-04-21Merge PR #11896: Use lists instead of arrays in evar instances.Maxime Dénès
Ack-by: SkySkimmer Reviewed-by: maximedenes
2020-04-21Fix VST after PrincetonUniversity/VST#402Gaëtan Gilbert
Specifically https://github.com/PrincetonUniversity/VST/commit/86d7ac6eaf9c580d5705c4257814f64560d24257
2020-04-20Remove mod_constraints field of module bodyGaëtan Gilbert
2020-04-14Merge PR #11820: Partial importsMaxime Dénès
Reviewed-by: Zimmi48 Reviewed-by: jfehrle Reviewed-by: maximedenes Ack-by: ppedrot
2020-04-13[ocamlformat] Update to 0.14.0Emilio Jesus Gallego Arias
No diff to sources (luckily), see release notes at https://discuss.ocaml.org/t/ann-ocamlformat-0-14-0/5435 for more information.
2020-04-13Overlay for partial importsGaëtan Gilbert
2020-04-11[ci] [build] Bump Dune to 2.5.0Emilio Jesus Gallego Arias
It is unfortunate that we cannot install coqide and Dune 2.5.0 in < 4.07.0
2020-04-06Add overlays.Pierre-Marie Pédrot
2020-04-03Fix Flocq CI script.Théo Zimmermann
autogen.sh was removed in https://gitlab.inria.fr/flocq/flocq/-/commit/d679d3770aea2ff8608c77096158653837798124
2020-04-03Fix CoRN CI script.Théo Zimmermann
Auto-generated files like the Makefile have recently been removed from the sources (cf. coq-community/corn#88). Calling ./configure.sh is now required.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:29:33 +0000