| Age | Commit message (Collapse) | Author |
|---|
|
The azure OSX job replaces the first travis job, and the second always
fails and so is useless.
|
|
This changes the semantics a bit since we don't have
TRAVIS_COMMIT_RANGE anymore, instead we do per-commit linting for the
commits since the last merge commit.
|
|
|
|
This was kept as a fallback for some time, not worth keeping it
anymore as our GitLab setup seems mature and reliable enough.
|
|
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 LaTeX doc is already tested in GitLab CI and finding the right dependencies
in this older version of Ubuntu is a hurdle.
|
|
We'd like to use `(lang 1.1)` features. Elpi needs update as recent
`ppx_tools_versioned` changes broke it.
|
|
OCaml 4.07.0 should have fixed the (memory eating bug)[https://caml.inria.fr/mantis/view.php?id=7630]
|
|
As discussed in #6930, we remove the warnings jobs and instead do
require the developers to submit a clean build.
|
|
- 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.
|
|
|
|
Users who want to test external projects should be encouraged to activate
GitLab CI as is documented in dev/ci/README.md.
|
|
suggestion.
|
|
|
|
Rather than trying to keep the version of dependencies in sync with GitLab CI.
|
|
This fixes #7734.
|
|
The file `config/Makefile` doesn't exist unless we run `./configure`.
We shouldn't have to run `./configure` to run `make clean`. We now no
longer error in any case if `config/Makefile` doesn't exist; this is
simpler than only not erroring if the target is `clean`.
We also now test this property when building on CI.
This fixes #7542
|
|
It is needed by Elpi and pidetop, and it is anyways needed for most
OCaml packages, including some Coq tools in the future.
The future base Docker image will include it by default.
|
|
|
|
|
|
|
|
In the original Travis CI setup, the per-job time limit was an
issue. However, Gitlab has much improved this problem due to
a) Coq not being built for each contrib,
b) user-configurable time limit.
We thus disable the expensive builds from Travis:
`fiat-crypto`, `formal-topology`, `geocoq`, `iris-lambda-rust`,
`math-comp`, `unimath`, `vst`
and instruct Gitlab to build [`geocoq`, `math-comp`, `unimath`, `vst`]
in full.
We also update the `math-comp` script as the `odd-order` theorem lives
in a separate repository and it is a key CI case.
|
|
This is a "test" PR, but could be merged if we like it.
|
|
|
|
|
|
I followed the code for fiat-crypto / fiat-parsers. I hope I didn't
miss anything.
|
|
requested compiler.
|
|
|
|
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
|
|
|
|
|
|
This makes sense and simplifies the script a bit. In preparation for a
more uniform, Docker-based base image.
|
|
AFAICS `imagemagick` `hacha` and `transfig` are not used anymore.
|
|
|
|
|
|
|
|
- BUILD_TARGET not used
- Put elpi's FINDLIB_VER="" at the end of the environment for nicer
display in the travis UI.
|
|
|
|
Updates to homebrew packages can currently make this packaging job fail
at any stage of the release cycle. Also, we are leaving dangerously
because we depend on python2 and python3 at the same time, which is not
supported by homebrew. To make this more reliable, we should switch to a
Nix-based build infrastructure at least for macOS.
|
|
The original contribution is from Clément Pit-Claudel. I updated
his code and integrated it with the Coq build system. Many improvements
by Paul Steckler (MIT).
This commit adds the infrastructure but no content.
|
|
|
|
gtksourceview depends transitively on py2cairo which was updated in
Homebrew to depend explicitly on python2 (see Homebrew/homebrew-core#24714):
this makes the python3 install step impossible.
We also remove the libxml2 install step which was failing in a non-fatal way.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
sudo apt-get install will fail on gcc-multilib if apt-get update cannot
fetch launchpad, so instead we delay installing these packages.
|
