aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
AgeCommit message (Collapse)Author
2020-10-16Overlay for elpi.Hugo Herbelin
2020-10-12Merge PR #13175: [ci] elpi 1.11.4coqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: MSoegtropIMC
2020-10-12Merge PR #12449: Minimize Prop <= i to i := Setcoqbot-app[bot]
Reviewed-by: mattam82 Ack-by: Janno Ack-by: gares
2020-10-12Automatically merge overlays with most recent upstream versionGaëtan Gilbert
This avoids the need to rebase the overlay when nothing has changed.
2020-10-12Lowercase variables in git_downloadGaëtan Gilbert
2020-10-12elpi 1.11.4Enrico Tassi
2020-10-09Merge PR #13088: [stm] move par: to comTacticcoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: ppedrot Reviewed-by: ejgallego
2020-10-09overlay for mtac2Enrico Tassi
2020-10-09overlay for minim-prop-tosetGaëtan Gilbert
2020-10-08Add overlays for Coq-Equations, aac-tactics.Hugo Herbelin
2020-10-08update for Iris build system changesRalf Jung
2020-10-06Define a new type instance_flag instead of using [unit option]Gaëtan Gilbert
2020-09-28CI script wrapper now requires PythonMaxime Dénès
2020-09-23Merge PR #12977: Statically ensure that only polymophic hint terms come with ↵coqbot-app[bot]
a context. Reviewed-by: mattam82
2020-09-22Add overlay for Equations.Hugo Herbelin
2020-09-21Make print-pretty-timed robust against non-output-sync logsJason Gross
Also pass `--output-sync` on the CI, as suggested in https://github.com/coq/coq/pull/12653#issuecomment-696226093, to protect against this failure mode. Fixes #13062
2020-09-17[build] Don't link `num` anymore in CoqEmilio Jesus Gallego Arias
After #8743 we don't depend on `num` anymore in the codebase; thus we drop the dependency. This could create problems for plugins relying on this implicit linking.
2020-09-15[zarith] [micromega] Bump to 1.10 and remove some hacksEmilio Jesus Gallego Arias
In particular, behavior of `Z.gcd` and `Z.lcm` has been fixed in 1.10, see https://github.com/ocaml/Zarith/issues/58
2020-09-14[ci] [docker] Up testing to OCaml 4.11.1Emilio Jesus Gallego Arias
- `odoc` must be bumped to support 4.11
2020-09-13Add overlays.Pierre-Marie Pédrot
2020-09-11[ci] [mathcomp] run the test suiteEnrico Tassi
2020-09-10Add simple-io to dev/ci/nix.Théo Zimmermann
2020-09-04Merge PR #12969: CI: build Iris examples instead of lambda-Rustcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-09-03Add Equations overlayMaxime Dénès
2020-09-02fix grepping for the Iris commitRalf Jung
2020-09-02CI: build Iris examples instead of lambda-RustRalf Jung
2020-08-31Update update_global_env usageGaëtan Gilbert
- take just a ugraph instead of the whole env - rename to update_sigma_univs - push global env lookup a bit further up - fix vernacinterp call to update all surrounding proofs, not just the top one - flip argument order for nicer partial applications
2020-08-31Merge PR #12875: Further extensions of About wrt Arguments and renamingcoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: herbelin
2020-08-28Adding overlay for coq-elpi.Hugo Herbelin
2020-08-27[numeral] [plugins] Switch from `Big_int` to ZArith.Emilio Jesus Gallego Arias
We replace Coq's use of `Big_int` and `num` by the ZArith OCaml library which is a more modern version. We switch the core files and easy plugins only for now, more complex numerical plugins will be done in their own commit. We thus keep the num library linked for now until all plugins are ported. Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2020-08-25Merge PR #12801: Put cyclic numbers in sort Set instead of TypeAnton Trunov
Ack-by: Zimmi48 Reviewed-by: anton-trunov
2020-08-25Merge PR #12798: Change OUnit package name to ounit2.coqbot-app[bot]
Reviewed-by: ejgallego
2020-08-24Fix Coqtail test directory.whonore
Tests moved in https://github.com/whonore/Coqtail/pull/134.
2020-08-24Put cyclic numbers in sort Set instead of TypeVincent Semeria
Added user overlay for bignums
2020-08-24Merge PR #12565: Dnets now consider axioms as being opaque for pattern ↵coqbot
recognition. Reviewed-by: mattam82
2020-08-20Merge PR #12756: Do not refresh the names of implicit arguments.Maxime Dénès
Reviewed-by: herbelin Reviewed-by: maximedenes
2020-08-20Adding overlays.Pierre-Marie Pédrot
2020-08-19Do not refresh the names of implicit arguments.Jasper Hugunin
Try just going with the user-given names, and not worrying about what happens with repeated names or anonymous implicits. (Support for anonymous implicits is due to herbelin in #11098.) This PR should not change behaviour in the absence of repeated names. Since repeated names are already a poorly handled corner case, I would recommend changing binder names to avoid overlap in the case of a change in behavior. Since anonymous implicits and implicits with repeated names can already happen, I think this is unlikely to cause too many new problems, though it might exacerbate existing ones. However, I already had to fix one newly possible anomaly, so I can't be too confident. The most common change in external developments was that an argument no longer gets `0` appended to it, causing the `Arguments` command to complain about renaming. To fix this and keep the old name, one can simply use the `rename` flag as suggested, or switch to the new, un-suffixed name. Closes #6785 Closes #12001 Another step towards checking the standard library with `-mangle-names`.
2020-08-19Add overlay.Pierre-Marie Pédrot
2020-08-18Dockerfile: Update ounitGaëtan Gilbert
2020-08-12Add overlays.Pierre-Marie Pédrot
2020-07-24CI metacoq: make .merlinGaëtan Gilbert
For convenience
2020-07-21Add Coqtail to CIwhonore
2020-07-17Merge PR #12701: CI: Use bundled compcert for VSTEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-17CI: pass -silent to coqchk in compcert jobGaëtan Gilbert
Otherwise gitlab stops logging somewhere in the middle. Also pass -o because we can.
2020-07-17CI: Use bundled compcert for VSTGaëtan Gilbert
2020-07-15Merge PR #12671: Minor improvement to CI logsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-10Minor improvement to CI logsGaëtan Gilbert
- don't `set -x` while loading overlays, non-verbose untaring - ls _build_ci to help figure out artifact download issues
2020-07-09Overlay for removing struc_tupleGaëtan Gilbert
2020-07-08[ci] Overlay for metacoq and rewriterEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:00:04 +0000