aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
AgeCommit message (Collapse)Author
2020-06-23[ci] Add coq-community/coq-performance-testsJason Gross
It's tested on the bench, so might as well test it on the CI. Hopefully it's not too memory-heavy. (It should only take a couple of minutes, time-wise.)
2020-06-22Merge PR #12546: [ci] Use a tested branch of PerennialEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-19Add overlays.Pierre-Marie Pédrot
2020-06-17[ci] Use a tested branch of PerennialTej Chajed
2020-06-15Merge PR #12509: updated ci for unicoqThéo Zimmermann
Reviewed-by: Zimmi48
2020-06-15updated ci for unicoqbeta
2020-06-15Merge PR #12494: [dev/ci/nix] Support for building the Gappa plugin.Vincent Laporte
Reviewed-by: vbgl
2020-06-10[dev/ci/nix] Support for building the Gappa plugin.Théo Zimmermann
2020-06-10Windows: fix menhir and coq-menhirlib build for latest version.Michael Soegtrop
2020-06-08[ci] [overlays] Pin unicoq to a stable version.Emilio Jesus Gallego Arias
Following upstream advice.
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 20:26:59 +0000