| Commit message (Collapse) | Author | Age |
|
|
|
|
| |
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.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Script modified from
https://unix.stackexchange.com/questions/175146/apt-get-update-exit-status
I stuck the code in "install" rather than "before_install" so that the
lint target didn't need to be changed. I also haven't touched the
targets that add more packages; I'll leave that to someone who knows
more about the "&" and "*" syntax being used in the configuration.
|
|/
|
|
| |
These tests are already done by CircleCI.
|
|
|
|
| |
Closes #6509.
|
|
|
|
|
|
|
|
|
| |
When invoking through Makefile we always rebuild dependencies. To skip
dependencies, invoke ci-wrapper directly. We make Circle CI do this.
In order to properly support invoking ci-wrapper directly we replace
"make" in ci-common by a bash function which adds -j to the make
invocation outside submakes. We also set TIMED in the ci-wrapper.
|
|
|
|
|
|
| |
Travis has moved on to macOS 10.12 but this makes the package
incompatible with earlier versions.
This fix should restore the compatibility with OS X 10.11.
|
|
|
|
|
|
| |
This avoids mixing native and byte compilation as the debug printers
are always byte compiled and the tools have no .byte rule, only the
OCAMLBEST rule.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Due to an API change in laglgtk, we need to update CoqIDE. We use a
makefile hack so it can compile with lablgtk < 2.8.16, another option
would be to require 2.8.16 as a minimal dependency.
We also refactor travis to test more lablgtk versions.
We also need to account for improved attribute handling in 4.06.0, in
particular module aliases will propagate the deprecation status.
Fixes #6140.
|