travis caching

Stream: general

[Mario Carneiro]

@Gabriel Ebner Could you help me try to set up build caching on travis? The from-scratch build times are nearing the time limit for public jobs. I tried following https://docs.travis-ci.com/user/caching/ but I can't find the Build branch updates option.

[Gabriel Ebner]

I think this option is now called "build pushed branches".

[Gabriel Ebner]

I'm not sure the caching feature will fix the timeouts though. The cache is only saved when a build is completed. The next time somebody changes tactic/interactive.lean everything will need to be rebuilt, the build won't finish, and the cache remains out of date (forever, since all future builds fail as well).

[Simon Hudon]

If you want to separate a preparatory step, you can use build stages.

[Gabriel Ebner]

I don't see any good way to break up the build into stages though. The main lean --make invocation takes almost an hour (is that right? it's much faster locally?), and we need to cache its output.

[Simon Hudon]

can we build a few directories in the first stage and then the rest?

[Gabriel Ebner]

That's one option. 2) We could break up mathlib into multiple repositories, add binary releases, and then use the binary releases for travis in the dependent repositories. This is also a bit of work, and the development workflow is probably worse. 3) Probably the least effort: somebody sets up a machine with Jenkins somewhere (@Mario Carneiro?). Then mathlib can build for hours (probably less, a full mathlib build only takes a bit over 9 minutes here).

[Simon Hudon]

I do not believe 3) is the least effort. The people I know who have their own Jenkins setup say that it's much more trouble than using Travis.

[Simon Hudon]

You could probably do a mix of 1) and 2) and create different subsets of mathlib that will build in separate stages on Travis

[Gabriel Ebner]

Jenkins has a bit of a learning curve since you can't copy a random .travis.yml. But executing three lines of shell script is pretty easy, you just need to insert it as a build step. Fighting with travis build stages and caching may be more work. We've had a pretty good experience with jenkins in our group.

[Gabriel Ebner]

I just wanted to bring it up as an option, it took me about a minute to set up mathlib in jenkins (12 minutes build time): http://clogic92.dmg.tuwien.ac.at/job/mathlib/2/console (GH integration and zulip notification is not much more work.) The main problem is of course hosting, so if we can easily fix travis then this is probably the way to go.

[Simon Hudon]

Nice! Do you need to dedicate your own computer or can you put it only on something like AWS?

[Gabriel Ebner]

You can of course use AWS, but that probably gets pricy. It is probably easier and cheaper to host it at a university.

[Simon Hudon]

That's probably easier than maintaining the machines yourself too

[Johan Commelin]

Maybe CoCalc wants to help, and has the experience? I have no clue if they would be open to something like that?

[Johan Commelin]

Maybe we should just ask William... @Kevin Buzzard what do you think?

[Johan Commelin]

You know him best.

[Kevin Buzzard]

I know him but I have no understanding of this thread

[Johan Commelin]

We are talking about a self-hosted Travis replacement. Where we can have compile times >1hr.

[Johan Commelin]

But self-hosting implies that you have to maintain stuff

[Johan Commelin]

@Mario Carneiro @Gabriel Ebner @Simon Hudon I don't know if you guys are familiar with CoCalc. It is a cloud environment for scientific computing. And William is a mathematician who is interested in Lean. So that helps.

[Johan Commelin]

William is interested in Lean in the sense that he wants to make it available in CoCalc, once he has figured out how to make a good user interface for it.

[Simon Hudon]

Cool! Does he not like the online version?

[Johan Commelin]

If you guys want to consider the Jenkins approach, and would like me to ask William, just tell me.

[Johan Commelin]

The online version is way to slow when you want to do serious stuff. And it is not collaborative.

[Johan Commelin]

With CoCalc you would have fast servers running Lean, and just a UI in the browser.

[Simon Hudon]

You want it to be like Google Docs or just have some git support?

[Johan Commelin]

So far he has collaborative editors for LaTeX (with live preview) and Python (+ all its scientific extensions), Jupyter etc...

[Johan Commelin]

No, Google Docs like

[Johan Commelin]

But a VScode-like UI

[Johan Commelin]

So, they definitely have the computing power for the Jenkins instance. The question is if they want to support it. (They don't have that much staff...)

[Simon Hudon]

VSCode is available online for some languages: https://stackblitz.com/ maybe that would help

[Johan Commelin]

Yes, I gave him that link.

[Simon Hudon]

Cool

[Johan Commelin]

But now you need to add in collaboration, and the Lean extension.

[Scott Morrison]

I don't think we should be asking William Stein to help us with things like travis.

[Mario Carneiro]

@Gabriel Ebner I'm okay with self-hosting Jenkins, provided that it doesn't need 100% uptime. That is, the server does not need to be running when someone pushes a commit, it just builds when it's available

[Mario Carneiro]

I don't know that much about Jenkins though

[Mario Carneiro]

Not sure about available CMU resources

[Gabriel Ebner]

I don't think running Jenkins on your laptop is a good idea. It should have a public IP so that other people can look at the build logs in case of failure. (But you don't need six nines availability either.)

[Mario Carneiro]

Simon suggested that we use a staged build https://docs.travis-ci.com/user/build-stages/ , since the different jobs have independent timeouts. The idea would be to run lean --make for 45 minutes or so in the first job, and then always succeed and update the cache. Then stage 2 would be a regular lean build using the artifacts from the first run. @Gabriel Ebner Could you see if this works with the caching? Travis documentation suggests using S3 for common files so I'm not sure if the cache sharing trick will work.

[Simon Hudon]

What do you mean by the cache sharing trick?

[Simon Hudon]

Rather: why do you think that sharing cache between phases might not work?

[Mario Carneiro]

They run in separate VMs

[Simon Hudon]

Ok but when I used it, my later stages inherited the cache from the early stages. I don't see why that wouldn't happen for mathlib

[Scott Morrison]

I just investigated setting up a copy of Jenkins (it's easy!), but couldn't get too far. When I asked it to scan the leanprover organization on github, it quickly errored: it asks for things through the API that only people with commit access can use:

ERROR: [Mon Jun 04 20:46:32 AEST 2018] Could not fetch sources from navigator org.jenkinsci.plugins.github_branch_source.GitHubSCMNavigator@48f109dc
java.io.FileNotFoundException: https://api.github.com/repos/leanprover/lean/collaborators/Kha/permission
    at com.squareup.okhttp.internal.huc.HttpURLConnectionImpl.getInputStream(HttpURLConnectionImpl.java:243)
    at com.squareup.okhttp.internal.huc.DelegatingHttpsURLConnection.getInputStream(DelegatingHttpsURLConnection.java:210)
    at com.squareup.okhttp.internal.huc.HttpsURLConnectionImpl.getInputStream(HttpsURLConnectionImpl.java:25)
    at org.kohsuke.github.Requester.parse(Requester.java:612)
    at org.kohsuke.github.Requester.parse(Requester.java:594)
    at org.kohsuke.github.Requester._to(Requester.java:272)
Caused: org.kohsuke.github.GHFileNotFoundException: {"message":"Must have push access to view collaborator permission.","documentation_url":"https://developer.github.com/v3/repos/collaborators/#review-a-users-permission-level"}
    at org.kohsuke.github.Requester.handleApiError(Requester.java:686)
    at org.kohsuke.github.Requester._to(Requester.java:293)
    at org.kohsuke.github.Requester.to(Requester.java:234)
    at org.kohsuke.github.GHRepository.getPermission(GHRepository.java:502)
    at org.jenkinsci.plugins.github_branch_source.GitHubSCMSource$1.fetch(GitHubSCMSource.java:874)
    at org.jenkinsci.plugins.github_branch_source.GitHubSCMSourceRequest.getPermissions(GitHubSCMSourceRequest.java:474)
    at

[Johan Commelin]

Can you get it to work with one of your own lean repos?

[Scott Morrison]

I got Jenkins to read the .travis.yml file from one of my own repos, and it starts off happily enough, but then says:

leanpkg test
OSX 'readlink' command does not support option '-f', please install 'greadlink'. If you use 'brew', you can install 'greadlink' using 'brew install coreutils'

[Scott Morrison]

coreutils is already installed, and leanpkg test works just fine on the command line. :-(

[Sebastian Ullrich]

Different PATHs, probably?

[Johan Commelin]

Hmmm, I don't know how to help you with that one. (I don't really have any Jenkins experience myself.) Are you on a Mac? Or is Jenkins just very Mac-oriented?

[Scott Morrison]

I think I'm going to pause my Jenkins experiments for now. (I have a big fat machine with plenty of RAM and cores, with a fixed IP address, but I would have to negotiate some holes in firewalls with my ... uncooperative ... IT staff.)

[Johan Commelin]

Aah, yes, I forgot that William isn't the only one with big fat machines. So do you (-;

[Gabriel Ebner]

I think the easiest way to setup jenkins with github nowadays is to use the blue ocean interface with Jenkinsfile (docs here and here). All you need to do is install elan and add this file to the repo. Then everything seems to work out of the box, including status information on PRs (look here). (This is a linux machine btw, and we use it for another project so I can't easily repurpose it for mathlib.)
You definitely want a public IP with an open http port so people can look at the build log. On the permission side, I think anybody in the lean github organization can authorize it. The best way to automatically trigger jenkins is via webhooks, then it starts building a few seconds after a PR gets created or a commit is pushed. Unfortunately I can't create webhooks on any of the lean projects. In the worst case, jenkins can poll github in regular intervals.

[Scott Morrison]

So while I have a machine I can run Jenkins on, it seems there’s no way I can convince local IT people to let that Jenkins interface be publicly accessible. I could set it up to poll github in order to initiate builds, but I’d need some mechanism to output the build logs to a web server. If anyone knows of an out-of-the-box solution to this, I’m happy to pursue it, but perhaps there are better avenues.

[Johan Commelin]

Can't you have it push the build logs by ssh to some web server?

[Scott Morrison]

Yes, that's what I had in mind. I guess I was asking if someone knows of an easy-to-configure Jenkins plugin that does this. I'd be happy to contribute hardware and a little setup time, but I don't want to feel responsible for managing an intricate web of scripts. :-)

[Reid Barton]

from .travis.yml:

  - rm `git status | grep "\.lean" | sed "s/\.lean/.olean/"` ||  true
  - rm `git status | grep "\.lean"` || true

Is there a reason we couldn't replace this with

  - git clean -d -f

This should remove all untracked files, which I think is what the rm lines are trying to accomplish, while leaving ignored files, e.g. built .olean files.

[Reid Barton]

The rm lines failed for #641, because the cache contained an entire directory left over from a rename, and in that situation git status only reports the directory as a whole as untracked.

[Kevin Buzzard]

641 divides $2^{2^5}+1$, the 5th Fermat number, disproving a conjecture of Fermat.

[Reid Barton]

Oh wait this won't actually work, because the old .olean files will still be left behind and lean will use them (argh)

[Sebastian Ullrich]

git clean first, then remove all .olean files without corresponding .lean file?

[Reid Barton]

@Simon Hudon and I arrived at the same conclusion

[Sebastian Ullrich]

Definitely an improvement over the old code :)

[Reid Barton]

By the way, GHC seems to ignore object files without matching source files. I think that's a better behavior than Lean's

[Reid Barton]

GHC is also pretty smart about not recompiling downstream modules if a dependency was modified in a way that can't affect clients. It might be worth borrowing those techniques at some point, though I don't know how effective they would be in the Lean world