aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/docker/bionic_coq
AgeCommit message (Collapse)Author
2020-10-12elpi 1.11.4Enrico Tassi
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-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-18Dockerfile: Update ounitGaëtan Gilbert
2020-07-21Add Coqtail to CIwhonore
2020-05-26Fix #12280: do not use xindy to avoid build failures on some machines.Théo Zimmermann
2020-05-19[ci] [docker] Bump ocamlformat and duneEmilio Jesus Gallego Arias
cc: #12350
2020-05-18Bump minimal versions of refman dependencies.Théo Zimmermann
Fixes #11936. Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
2020-05-06[ci] bump elpi to 1.11Enrico Tassi
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-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-03-29[ci] [gitlab] Bump to edge to OCaml 4.10, add test-suite for OCaml 4.11Emilio Jesus Gallego Arias
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[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-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-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
2019-12-13[ci] [docker] Install ocamlformat in docker images.Emilio Jesus Gallego Arias
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] Test latest artifacts of SF instead of the stable versionMaxime Dénès
2019-11-05elpi 1.8Enrico Tassi
2019-09-19[ci] Update supported OCaml version to 4.09.0Emilio Jesus Gallego Arias
2019-09-07update elpi to 1.7Enrico Tassi
2019-08-27[ci] Update to OCaml 4.08.1Emilio Jesus Gallego Arias
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
The changes are large due to `Pervasives` deprecation: - the `Pervasives` module has been deprecated in favor of `Stdlib`, we have opted for introducing a few wrapping functions in `Util` and just unqualified the rest of occurrences. We avoid the shims as in the previous attempt. - a bug regarding partial application have been fixed. - some formatting functions have been deprecated, but previous versions don't include a replacement, thus the warning has been disabled. We may want to clean up things a bit more, in particular w.r.t. modules once we can move to OCaml 4.07 as the minimum required version. Note that there is a clash between 4.08.0 modules `Option` and `Int` and Coq's ones. It is not clear if we should resolve that clash or not, see PR #10469 for more discussion. On the good side, OCaml 4.08.0 does provide a few interesting functionalities, including nice new warnings useful for devs.
2019-07-06[Dockerfile] update menhir versionGaëtan Gilbert
Compcert needs a new menhir.
2019-06-21[docker] [ci] Update Elpi to version 1.4.0Enrico Tassi
2019-06-11update elpi to 1.3.1Enrico Tassi
2019-04-20update elpi to version 1.2Enrico Tassi
2019-03-19[coqide] [ci] Update GTK toolchain to lablgtk3Emilio Jesus Gallego Arias
- Update Docker images to install compatible version of lablgtk3 - We remove unnecesary variables from configure. - We fix path detection of GTK libs in makefile
2019-03-19CoqIDE: Adapt configuration to require lablgtk3 and gtksourceview3.Hugo Herbelin
2019-03-11[ci] [docker] Upgrade odoc to 1.4.0Emilio Jesus Gallego Arias
This is routine as for API doc writers to be able to access the newer features.
2019-02-18[gitlab] [docker] [ci] Remove "edge" compiler switch.Emilio Jesus Gallego Arias
Since a long time the compiler switch is not very useful as it is not used to test any CI. The `edge+flambda` version seems stable enough to carry out the `edge` testing by itself, thus we remove the `egde` switch saving valuable Docker image size and Gitlab runners. We also tweak the `pkg:opam` job as to correctly set the version of the pinned local package.
2019-02-04Dockerfile: update menhir from 20180530 to 20181113Vincent Laporte
2018-12-14[dune] [gitlab] Test OCaml trunk.Emilio Jesus Gallego Arias
We add a job testing the build of Coq with OCaml 4.08 [AKA `trunk`] CoqIDE is not supported in 4.08 due to missing `lablgtk`, also `oUnit` cannot be currently installed, thus we have to add a switch to the test suite to disable `unit-tests`. Many deprecation warnings happened in 4.08 so we use the `release` profile to make them not fatal. Using a 4.08 build profile would be an option too.
2018-12-13[dune] [doc] Support for building the reference manual with Dune.Emilio Jesus Gallego Arias
This is a reduced version of #8503 as to provide a way to build the reference manual with Dune. Dune 1.6 supports (experimentally) directories as targets, thus we introduce a rule that will call `sphinx` to build the manual. This only provides build, however generation of `.install` rules is not done, it will be hopefully addressed in #8503. Note that we set `expire: 1 month` for all the artifacts we build with Dune. IMHO this makes most sense as not to abuse Gitlab's hosting, however of course we could consider a different deployment strategy if wanted.
2018-11-21[camlp5] Remove dependency on camlp5.Emilio Jesus Gallego Arias
2018-11-08Revert "Merge PR #8923: Bump camlp5 minimal version and use its safe API."Pierre-Marie Pédrot
This reverts commit c4880effb91fab55c250a799cbceac9b04681db0, reversing changes made to 65927c22bcad62e1bc9a28a57377d82eba215a2d.
2018-11-07Bump up the minimal camlp5 version to 7.06.Pierre-Marie Pédrot
This is the first release that contains the type-safe grammar API.
2018-11-06[Docker] Update COMPILER_EDGE: 4.07.0 → 4.07.1Vincent Laporte
Also update CAMLP5_VER_EDGE: 7.06 → 7.06.10-g84ce6cc4 This is to avoid an OCaml bug that occurs when compiling the OCaml code extracted from part of a patched version of CompCert. ~~~ File "extraction/Parser.ml", line 12375, characters 19-29: Error: Constraints are not satisfied in this type. Type initstate' should be an instance of initstate' ~~~ This compiler issue only appears with OCaml 4.07.0 (neither with 4.06 nor with 4.07.1); hence this update.
2018-10-23[dune] [opam] Move to OPAM 2.0Emilio Jesus Gallego Arias
We need to update in Docker: - dune to 1.4.0: as it honors `-p` on test stanzas - dune-release to 1.1.0: support for OPAM 2.0 + fixes This makes `dune-release distrib` / `dune-release opam pkg` work. TODO: we need to figure out what is going on with the versioning. Should we do `dune subst` on `pinned`?
2018-10-22[doc] [api] Update `odoc` to new release 1.3.0Emilio Jesus Gallego Arias
This includes many changes, please have a look at the newly generated docs.
2018-10-05[ci] [dune] [opam] Fixes to OPAM and CI target.Emilio Jesus Gallego Arias
The Dune `release` profile is used by OPAM so that should cover the testing. We also update the dependencies: - camlp5: 7.01 had some bugs regarding grammar; we could use 7.02, however this version it is not in OPAM. So I guess that leaves us with 7.03 again. - lablgtk < 2.18.5 does not support OCaml >= 4.05.0.
2018-09-26[ocaml] Update required OCaml version to 4.05.0Emilio Jesus Gallego Arias
Closes #7380. Ubuntu 18.04 and Debian Buster will ship this OCaml version so it makes sense we bump our dependency to 4.05.0 as we can use some newer compiler features.
2018-09-25elpi 1.1.0Enrico Tassi
2018-09-24[ci] [docker] Move to OPAM 2.0Emilio Jesus Gallego Arias
The OPAM 1.2 repository has been frozen, thus we must use OPAM 2.0 if we want to get newer versions of packages / compilers. For now we must perform a manual install of OPAM as no packages for Ubuntu 18.04 exist. Note that this means nothing about the installability of Coq itself, whose OPAM repository should remain in 1.2 format for quite a long period.
2018-09-21[dune] [configure] Allow to set prefix using environment variable.Emilio Jesus Gallego Arias
This is a hack to enable correct OPAM building, the medium-term plan is to avoid having to set a prefix at configure time but instead using a set of rules to locate the Coq library. We use `(env_var ...)` in a dependency rule, which a feature of Dune 1.2
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 18:29:23 +0000