| Age | Commit message (Collapse) | Author |
|---|
|
This is the first release that contains the type-safe grammar API.
|
|
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.
|
|
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`?
|
|
This includes many changes, please have a look at the newly generated
docs.
|
|
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.
|
|
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.
|
|
|
|
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.
|
|
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
|
|
The minimum required versions of the Sphinx-related (and ANTLR)
Python packages for Coq 8.10 were chosen as the lower bound
between what is currently in Debian Buster and in NixOS 18.09
Jellyfish (in practice the lower bound was always met by NixOS
18.09 Jellyfish).
These minimum required versions were documented.
In the docker image used by GitLab CI, we install these
Python packages through pip as this allows us to pin them
to these specific versions.
In Travis, we let them unspecified to always test the
latest versions.
Finally, we also add the new dependencies of the Sphinx
PDF manual.
|
|
- odoc: used to generate the ML API documentation by Dune's `@doc`
target.
- dune-release: Automatic OPAM package generation and release.
Both packages require OCaml >= 4.02 thus installing on edge switches
only.
|
|
We'd like to use `(lang 1.1)` features. Elpi needs update as recent
`ppx_tools_versioned` changes broke it.
|
|
- We update the OCaml version used in the base CI image.
- Windows / OSX image building is also updated to use newer OCaml.
- We also update Dune to 1.0.0.
|
|
This should help towards ensuring that the system only has the
packages we specify in the Dockerfile.
We were missing:
- `git`: used in the CI system itself!
- `rsync`: used in the test-suite
- `python3-setuptools`, `python3-wheel`: necessary to use pip3
properly to install the missing python package.
- `autoconf`, `automake`: a few CI contribs depend on them.
|
|
|
|
Packages such as `menhir` or `elpi` are fragile w.r.t. updates, so
allowing a non-deterministic install in the Dockefile seems risky. We
have found trouble with Menhir in the past. We thus specify a concrete
version for all `CI_OPAM` packages.
cc: https://github.com/AbsInt/CompCert/issues/234
We also add remove `hevea` from `apt` dependencies as it hasn't been
needed since #7466 and add `texlive-science` which is needed to build
the `source-doc` target due to the `textgreek` package being used.
|
|
|
|
We also introduce a bit more systematic job naming: `base/edge`.
In order to make the flambda switch selectable we update the Docker
image so all the dependencies are installed in that one.
Note the extra quote rule for the flambda parameters, but unless we
can assign arrays to Gitlab variables there is not a good way to do
this I'm afraid.
With this patch we are getting close to being able to remove most
builds from Travis.
|
|
This should help #6808.
|
|
We provide a custom `Dockerfile` for Coq's CI system, based on
`ubuntu:bionic`. The image includes the required set of packages and
OPAM switches.
This greatly simplifies the Gitlab and Circle scripts, at the cost of
having to push a Docker build for them to depend on.
Travis is not included in this PR as it requires significant more
refactoring due to lack of native Docker support.
This is work in progress but ready, a build hook is used so the image
is properly tagged in the Docker autobuilder.
We need to improve the autobuilder setup but this last point requires
some design on how to trigger it.
Fixes #7383
|
