aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
AgeCommit message (Collapse)Author
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>
2020-02-04Non maximal implicits: add overlays for several librariesSimonBoulier
2020-02-02[ci] [fiat-crypto] Use the pinned bedrock2Jason Gross
Fiat-Crypto does not guarantee compatibility with the tip of bedrock2, only with the pinned version, and bedrock2 is still relatively unstable. So we make the CI not have Fiat-Crypto depend on bedrock2, and instead use the pinned submodule, by using `EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1` rather than `EXTERNAL_DEPENDENCIES=1`.
2020-02-02Move kind_of_type from the kernel to ssr.Pierre-Marie Pédrot
It was virtually unused except in ssr, and there is no reason to clutter the kernel with irrelevant code. Fixes #9390: What is the purpose of the function "kind_of_type"?
2020-02-01No spaces with em-dashes.Théo Zimmermann
Co-Authored-By: Jason Gross <jasongross9@gmail.com>
2020-01-31[ci] [fiat-crypto-legacy] Use new, faster targetsJason Gross
The computation of which files to build is now mostly cached rather than computed, eliminting basically all of the wait-time from `make` to the first invocation of `coqc`. Note that we no longer need to invoke `./etc/ci/remove_autogenerated.sh`, but it does not hurt, and it speeds up `coqdep` somewhat significantly. Fixes #9298
2020-01-31Clarify expectations for overlays in contributing guide and CI doc.Théo Zimmermann
Contributors are *not* required to prepare all the patches by themselves. They can request help from project authors, who should be ready to take part in this. Also, finish replacing "development" by the more appropriate word "project".
2020-01-28Add reduction-effects to the CIJason Gross
2020-01-21[ci] Pin SF until they solve their CI issues.Emilio Jesus Gallego Arias
Latest build on SF is erroring due to: ``` "messages" : [ { "type" : "error", "message" : "This job has been blocked because no credits are available on your plan. Please upgrade to continue building.", "reason" : "execution-authorization-failed" } ], ``` we temporary pin to the last successful job that produced artifacts.
2020-01-19Merge PR #11368: Turn trailing implicit warning into an errorHugo Herbelin
Ack-by: Zimmi48 Reviewed-by: herbelin Ack-by: maximedenes
2020-01-17Fix issue #11396 : Rlist hides standard list constructors cons and nilMichael Soegtrop
2020-01-15[Nix/CI] Add verdi-raftVincent Laporte
2020-01-15[Nix/CI] Update fiat_cryptoVincent Laporte
2020-01-08let CI test bedrock2's 'tested' branch instead of 'master'Samuel Gruetter
2020-01-07Trailing implicit error: overlaysSimonBoulier
2019-12-26Remove uses of Global in Evd API.Pierre-Marie Pédrot
Namely, Evd.evar_env and Evd.evar_filtered_env now take an additional environment instead of querying the imperative global one. We percolate this change as higher up as possible.
2019-12-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot
We restrict to those that are actually related to typeclasses, and perform the following renamings: Classops --> Coercionops Class --> ComCoercion
2019-12-18Merge PR #9786: Fix Equation's ci scriptPierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-12-16Overlay for #11027Gaëtan Gilbert
2019-12-13[ci] [docker] Install ocamlformat in docker images.Emilio Jesus Gallego Arias
2019-12-13Fix Equation's ci scriptMatthieu Sozeau
2019-12-06Adding overlay for Quickchick PR#145.Hugo Herbelin
2019-12-06Merge PR #11174: [dune] Update to dune language version 2.0Théo Zimmermann
Reviewed-by: Zimmi48
2019-12-04Overlay for ELPIHugo Herbelin
2019-12-04[dune] Update to dune language version 2.0Emilio Jesus Gallego Arias
This is the minimal set of changes requires for Coq to build under 2.0 mode. We may likely take advantage of some more new features. Note that Dune 2.0 requires OCaml >= 4.06.0, OPAM allows to use Dune in older versions as it will install a secondary compiler.
2019-12-02[ci] [sf] Add authentication to artifact download.Emilio Jesus Gallego Arias
It seems we need to pass the token to the actual artifact download.
2019-12-02[CI] Test latest artifacts of SF instead of the stable versionMaxime Dénès
2019-11-27[ci] Split out the dependencies of fiat-cryptoJason Gross
2019-11-27[ci] Build slightly more in the fiat-crypto targetJason Gross
This adds a couple extra files, but not many.
2019-11-21add tlc to ci; please proof read very carefully and test. thankscharguer
2019-11-12Expand documentation about generating a Docker image.Pierre-Marie Pédrot
2019-11-05overlayEnrico Tassi
2019-11-05elpi 1.8Enrico Tassi
2019-11-01Add overlaysPierre Roux
2019-10-29[declare] Use helper function for `fix_exn` instead of relying on internals.Emilio Jesus Gallego Arias
2019-10-25[funind] Remove duplicate save function.Emilio Jesus Gallego Arias
AFAICT the reasoning for introducing this function doesn't hold anymore. This is needed for future refactorings that should make some types private.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-22 15:21:03 +0000