aboutsummaryrefslogtreecommitdiffhomepage
path: root/.travis.yml
Commit message (Collapse)AuthorAge
* [ci] Remove warning jobs in favor of default `-warn-error yes`Gravatar Emilio Jesus Gallego Arias2018-07-12
| | | | | As discussed in #6930, we remove the warnings jobs and instead do require the developers to submit a clean build.
* [ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0Gravatar Emilio Jesus Gallego Arias2018-07-11
| | | | | | - 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.
* Merge PR #8036: [travis] Remove even more jobs.Gravatar Emilio Jesus Gallego Arias2018-07-10
|\
| * [travis] Remove even more jobs.Gravatar Théo Zimmermann2018-07-10
| | | | | | | | | | Users who want to test external projects should be encouraged to activate GitLab CI as is documented in dev/ci/README.md.
* | [travis] Try to workaround the repeated APT failures by using Jason Gross's ↵Gravatar Théo Zimmermann2018-07-10
|/ | | | suggestion.
* Remove some Travis jobs to make the build faster.Gravatar Théo Zimmermann2018-07-05
|
* Remove Elpi from Travis.Gravatar Théo Zimmermann2018-06-16
| | | | Rather than trying to keep the version of dependencies in sync with GitLab CI.
* Remove cross-crypto from Travis. It is still tested in GitLab CI.Gravatar Théo Zimmermann2018-06-07
| | | | This fixes #7734.
* Allow make clean to work on a fresh cloneGravatar Jason Gross2018-05-25
| | | | | | | | | | | 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
* [ci] Add Dune to the base system.Gravatar Emilio Jesus Gallego Arias2018-05-21
| | | | | | | 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.
* Merge PR #6808: Add unit tests to test-suiteGravatar Gaëtan Gilbert2018-05-17
|\
* \ Merge PR #7514: [ci] Don't build lite versions of CI developments.Gravatar Gaëtan Gilbert2018-05-16
|\ \
| | * add unit tests to test suiteGravatar Paul Steckler2018-05-16
| |/ |/|
| * [ci] Don't build lite versions of CI developments.Gravatar Emilio Jesus Gallego Arias2018-05-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | [travis] Remove some more jobs from PR testing now that they are on Gitlab.Gravatar Emilio Jesus Gallego Arias2018-05-16
|/ | | | This is a "test" PR, but could be merged if we like it.
* Remove tutorials.Gravatar Théo Zimmermann2018-05-10
|
* Merge PR #7473: [ci] Add mit-plv/cross-cryptoGravatar Emilio Jesus Gallego Arias2018-05-10
|\
| * [ci] Add mit-plv/cross-cryptoGravatar Jason Gross2018-05-09
| | | | | | | | | | I followed the code for fiat-crypto / fiat-parsers. I hope I didn't miss anything.
* | [travis] Add explicit opam switch command to guarantee we're using the ↵Gravatar Théo Zimmermann2018-05-09
| | | | | | | | requested compiler.
* | [travis] Fix version of camlp5 for OCaml 4.06.1.Gravatar Théo Zimmermann2018-05-09
|/
* [gitlab] [circleci] Use a Custom Docker Image as base CI setup.Gravatar Emilio Jesus Gallego Arias2018-05-05
| | | | | | | | | | | | | | | | | | | | 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
* Merge PR #7402: [ci]: add pidetop (fix #7336)Gravatar Emilio Jesus Gallego Arias2018-05-03
|\
| * [ci]: add pidetop (fix #7336)Gravatar Enrico Tassi2018-05-02
| |
* | [ci] [travis] Install num by default in all switches.Gravatar Emilio Jesus Gallego Arias2018-04-30
|/ | | | | This makes sense and simplifies the script a bit. In preparation for a more uniform, Docker-based base image.
* [doc] Remove unused dependencies.Gravatar Emilio Jesus Gallego Arias2018-04-28
| | | | AFAICS `imagemagick` `hacha` and `transfig` are not used anymore.
* [CI] elpi 1.0 has an official opam packageGravatar Enrico Tassi2018-04-27
|
* updating CI for Mtac2Gravatar Beta Ziliani2018-04-25
|
* CI: add fcsl-pcmGravatar Anton Trunov2018-04-20
|
* Travis: cleanup environment variables a bit.Gravatar Gaëtan Gilbert2018-04-16
| | | | | | - BUILD_TARGET not used - Put elpi's FINDLIB_VER="" at the end of the environment for nicer display in the travis UI.
* [ci] Tentative fix for #7206: MacOS test-suite job failing.Gravatar Théo Zimmermann2018-04-09
|
* Emergency fix for OSX packaging job on Travis.Gravatar Maxime Dénès2018-03-16
| | | | | | | | 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.
* Integration of a sphinx-based documentation generator.Gravatar Maxime Dénès2018-03-09
| | | | | | | | 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.
* Merge PR #6817: [configure]: support for profilesGravatar Maxime Dénès2018-03-08
|\
* | Fix failing packaging job.Gravatar Théo Zimmermann2018-03-05
| | | | | | | | | | | | | | | | 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.
| * configure: -warn-error: now takes a bool so that you can also turn it offGravatar Enrico Tassi2018-03-05
|/
* travis: elpi needs findlib >= 1.5Gravatar Enrico Tassi2018-02-28
|
* tavis: make the . in pkg.version part of $VERSIONGravatar Enrico Tassi2018-02-28
|
* ci: add elpiGravatar Enrico Tassi2018-02-19
|
* Merge PR #6636: Stop running duplicate Travis jobs on pull requests.Gravatar Maxime Dénès2018-01-30
|\
* | Add a comment referencing travis issue numbersGravatar Jason Gross2018-01-25
| |
* | Delay installing packagesGravatar Jason Gross2018-01-23
| | | | | | | | | | sudo apt-get install will fail on gcc-multilib if apt-get update cannot fetch launchpad, so instead we delay installing these packages.
* | Use travis_retry on apt-get updateGravatar Jason Gross2018-01-23
| | | | | | | | | | | | | | | | | | | | 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.
| * Stop running duplicate Travis jobs on pull requests.Gravatar Théo Zimmermann2018-01-23
|/ | | | These tests are already done by CircleCI.
* Update the lower-bound of the lablgtk dependency.Gravatar Théo Zimmermann2018-01-04
| | | | Closes #6509.
* Fix CI with parallel make (messed up dependencies)Gravatar Gaëtan Gilbert2017-12-21
| | | | | | | | | 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.
* Compatibility of the Coq macOS package with OS X 10.11.Gravatar Théo Zimmermann2017-12-15
| | | | | | 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.
* CI: use -byte-only in [warnings] jobs.Gravatar Gaëtan Gilbert2017-11-28
| | | | | | 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.
* Travis: do not build stdlib in [warnings] jobs.Gravatar Gaëtan Gilbert2017-11-28
|
* Add Equations to CIGravatar Matthieu Sozeau2017-11-20
|
* [ci] [coq] Complete 4.06.0 support.Gravatar Emilio Jesus Gallego Arias2017-11-13
| | | | | | | | | | | | | 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.