Add Coq to Travis CI

[liyishuai]

Meta-issue

Our current template builds everything in Docker, which is less flexible than what Travis can do with other languages. It'll be nice if we could have language: coq and run scripts conveniently.
Travis allows community-supported languages, and our community seems the right people to do that.
Similar issue in OCaml world: ocaml/ocaml-ci-scripts#53

[erikmd]

Hi @liyishuai

As we discussed just now in coq-community/templates#1, the necessary boilerplate involved in the Travis-CI+Docker-Coq templates is not that verbose…

However, I think this use case (reducing the verbosity of the CI script by making Travis CI support Docker-based testing "natively" like GitLab CI or Circle CI) is directly related to these upstream issues:

• [QUESTION] Is there way to use a custom docker image? travis-ci/travis-ci#4741 [closed question]
• Use custom docker image for builds travis-ci/travis-ci#7726 [open issue]

Thus, I'm a bit split on the timeliness to engage in the process described in the page you mention (https://docs.travis-ci.com/user/languages/community-supported-languages) as this process requires some additional work and maintenance… which would not be worth it if travis-ci/travis-ci#7726 happens to be implemented at some point :)

[Zimmi48]

Note that while Travis support would need to be maintained, and so represents additional work, it also becomes more straightforward for any Coq user to test their projects. Existing Travis users will find the information on how to test their Coq projects more quickly. It has another advantage which is to add Coq to the list on this page https://docs.travis-ci.com/user/languages, which is one of many small ways to give more notoriety to Coq. (And for once, we would be the first proof assistant to appear in this list.)

[Zimmi48]

One main requirement is to have three volunteers. I can be one of them if needed. I haven't looked yet at how much work this would represent though.

[llelf]

@Zimmi48 I looked at how Perl 6 (one of the “community-supported” languages) works, and the minimal (i. e. no any fancy stuff like matrices of builds etc, and they just build the compiler each time from the source) version is as simple as travis-ci/travis-build@7becb33.

[Zimmi48]

Thanks for looking into it. Building Coq every time from source is definitely not an option. If we decide to provide a native Travis support, it needs to be good enough, because there is nothing worse than to frustrate users. If providing good support is deemed too costly, it's better not to do anything.

[llelf]

Then there should be a place to store binaries for (at least one) Ubuntu version travis supports. Namely,

Ubuntu Bionic 18.04
Ubuntu Xenial 16.04 default
Ubuntu Trusty 14.04
Ubuntu Precise 12.04

The apt install Coq version in those a no-go, as it’s extremely old.

macOS version can be just downloaded from github releases.

[liyishuai]

I can volunteer if needed. If done I'd use it on QuickChick, which would save a lot of effort compared to current process.

[liyishuai]

The apt install Coq version in those a no-go, as it’s extremely old.

macOS version can be just downloaded from github releases.

We should probably install Coq via OPAM even if there are binaries available, for convenient dependency management.

[Zimmi48]

As long as it can be cached somewhere that will avoid rebuilding every time.

[liyishuai]

As long as it can be cached somewhere that will avoid rebuilding every time.

Did you mean caching Coq or dependencies?
Our environment should provide Coq installed, with version specified as parameter (should we specify OCaml version as well?) I don't think we should cache dependencies by default, since Travis fetches caches in a weird way that might retrieve from other branches.

[Zimmi48]

I mean Coq. I'm not sure what you mean by "dependencies".

[llelf]

We should probably install Coq via OPAM even if there are binaries available, for convenient dependency management.

What do you mean exactly?

The problem with the caches is that only successful builds are cached.
apt install-ing pre-built binaries (or even curl | tar -xf) actually would be better user experience.

[liyishuai]

Correct me if I'm wrong: I thought the configuration stage (where we install Coq) is done before the user's build, creating some image to start with, so there's no need to "cache" Coq.
My experience was caching the whole OPAM directory. When there's no cache available on some non-default branch, Travis fetches one from the default branch, which contains unwanted packages that mess up everything (including wrong version of Coq that has to be uninstalled).

[Zimmi48]

After reading this thread discussing the fate of Nix community support in Travis, and given that we now have pretty good GitHub Actions support (with very short and straightforward configuration files), I propose to decide that we won't add Coq community support to Travis and to close this issue.