aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
AgeCommit message (Collapse)Author
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-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.
2020-04-01Merge PR #11971: [ci] Run bignums' testsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-03-31Merge PR #11818: [proof] Further consolidation of the regular declaration pathGaëtan Gilbert
Ack-by: Matafou Reviewed-by: SkySkimmer
2020-03-31[ci] Run bignums' testsPierre Roux
2020-03-30[ci] [overlays] Adapt to declare API changes.Emilio Jesus Gallego Arias
- problem with metacoq overlay ; it expects to send a non-ground constant to the kernel, now it fails at prepare. Record Sigma (A : Type) (B : A -> Type) : Type := { fst : A ; snd : B fst }. Arguments fst {A B}. Arguments snd {A B}. Quote Recursively Definition foo := (fst, snd). There is a hack on the overlay, we need to discuss it a bit more.
2020-03-29[ci] [gitlab] Bump to edge to OCaml 4.10, add test-suite for OCaml 4.11Emilio Jesus Gallego Arias
2020-03-26[ci] Add bbvJason Gross
I believe a recent commit to master broke it, and now that it's no longer tested as part of fiat-crypto-legacy, I think it's time to add it.
2020-03-24Merge PR #11703: Making of NumTok an API for numeralPierre-Marie Pédrot
Reviewed-by: SkySkimmer Reviewed-by: ppedrot Reviewed-by: proux01
2020-03-23[ci] add metacoqMatthieu Sozeau
2020-03-22Overlay for QuickChickHugo Herbelin
2020-03-22Merge PR #11731: [proof] Miscellaneous refactoringsGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2020-03-19[ocamformat] Update to 0.13.0Emilio Jesus Gallego Arias
We include the `version=0.13.0` field that should help users not to use the wrong version. `disable=true` still seems a noop with `dune`. There are some minor changes in the way comments are formatted; I'm unsure if this is due to the `wrap-comments` option; as always; tweaks to the config are most welcome.
2020-03-19[obligations] Step towards more structured handling of remaining obligations.Emilio Jesus Gallego Arias
There is a lot of check overhead in the code, we will try to provide a more convenient API for manipulation of remaining obligations.
2020-03-19[ci] Overlays for declare interface refactoring.Emilio Jesus Gallego Arias
2020-03-19[refman] Remove workaround for sphinx-doc/sphinx#4983Clément Pit-Claudel
2020-03-18[ci] [docker] Update to 4.09.1Emilio Jesus Gallego Arias
That release includes non trivial changes related C compilers, in particular due to `-fno-common` support.
2020-03-18Adding overlays.Pierre-Marie Pédrot
2020-03-16[ci] Cleanup old overlays.Emilio Jesus Gallego Arias
2020-03-16[ci] [docker] Update components in Docker imageEmilio Jesus Gallego Arias
We bump ounit, odoc, and lablgtk3 ; so far this is routine maintenance.
2020-03-13Merge PR #11804: [CI] test hierarchy builder as part of elpiGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-12[ci] [doc] Point to actual docker instructions.Emilio Jesus Gallego Arias
2020-03-11Update dev/ci/ci-basic-overlay.shEnrico Tassi
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-03-11[CI] test hierarchy builder as part of elpiEnrico Tassi
2020-03-10Merge PR #11764: Simplify mutual template polymorphismGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-09Do not erase OCAMLPATH in CI targets with Dune-built CoqMaxime Dénès
2020-03-09Add CI overlays.Pierre-Marie Pédrot
2020-03-04Add overlay for equations.Hugo Herbelin
2020-03-01[ci] [docker] overlay for elpi 1.10Enrico Tassi
2020-03-01[ci] [docker] bump elpi to 1.10.2Enrico Tassi
2020-03-01[ci] bump dune to 2.0.1 due to upstream problemsEnrico Tassi
2020-02-24[ci] Fix Coquelicot buildEmilio Jesus Gallego Arias
New versions did remove the autogen.sh script in favor of plain `autoreconf` Note that the Coquelicot build documentation seems incorrect.
2020-02-20Merge PR #10832: Addressing #6082 and #7766: warning when overriding ↵Emilio Jesus Gallego Arias
notation format + new notion of format associated to a given interpretation Ack-by: maximedenes
2020-02-19Merge PR #11499: Clarify expectations for overlay creationEmilio Jesus Gallego Arias
Ack-by: JasonGross Ack-by: SkySkimmer Reviewed-by: ejgallego
2020-02-19Overlays for Equations, QuickChick and Iris.Hugo Herbelin
2020-02-18Merge PR #10204: Remove `unsafe_type_of` from `Coercion`Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: mattam82
2020-02-14Overlay for Inductive.type_of_inductive doesn't take an envGaëtan Gilbert
2020-02-13Merge PR #11417: Move kind_of_type from the kernel to EConstr.Enrico Tassi
Reviewed-by: SkySkimmer Reviewed-by: gares
2020-02-13Merge PR #11521: Remove Goptions.opt_name fieldPierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-02-12Split unicoq out of ci-mtac2.sh (keeping 1 CI job)Gaëtan Gilbert
No reason to have them in the same .sh
2020-02-12overlay for removal of optnameGaëtan Gilbert
2020-02-11Add paramcoq overlayMaxime Dénès
2020-02-11Remove fiat-crypto-legacy from CIMaxime Dénès
Motivations: - We should have only maintained developments in our CI - `make ci-fiat-crypto-legacy` takes about 15 mins before the first call to `coqc`, making it unusable to work on overlays - The coding style of this development is so fragile that adapting to any change of behavior requires diffing gigabytes of Ltac traces. @mattam82 and I have been blocked for 6 months this way, when working on unifall. I understand this development was meant to stress-test some components like printing, but I think the trade-off is bad. We should rather come up with specialized test suites for these components.
2020-02-11Merge PR #11235: Add syntax for non maximal implicit argumentsHugo Herbelin
Reviewed-by: herbelin Reviewed-by: jfehrle Ack-by: maximedenes
2020-02-07restore the default URL for coquelicotYves Bertot
2020-02-04Apply suggestions from HugoSimonBoulier
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 12:31:13 +0000