search

coq-community / manifesto

Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.
Other
68 stars 6 forks source link

Add Coq to Travis CI #70

Closed liyishuai closed 4 years ago

liyishuai commented 5 years ago

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 commented 5 years ago

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:

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 https://github.com/travis-ci/travis-ci/issues/7726 happens to be implemented at some point :)

Zimmi48 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

@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 https://github.com/travis-ci/travis-build/commit/7becb333a0b53a15ebe60a8edc563b9c68c77f75.

Zimmi48 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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

liyishuai commented 5 years ago

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 commented 5 years ago

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

llelf commented 5 years ago

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 commented 5 years ago

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 commented 4 years ago

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.