lean travis problems

Stream: general

[Kevin Buzzard]

https://travis-ci.org/leanprover/lean/jobs/359716662#L1465

[Kenny Lau]

lol

[Kevin Buzzard]

travis is a real headache at the minute, but it affects end users because if mathlib works with lean HEAD but travis doesn't like lean HEAD then the nightly doesn't appear, and then end users who use the nightlies (like me) on more than one machine (like me) find themselves in situations where the nightly on one machine is too old for some reason, but the canonical upgrade process ("upgrade to current lean nightly and mathlib head") doesn't work.

[Kevin Buzzard]

Is travis trying to be too clever? I would imagine that Leo / Sebastian don't usually commit versions of Lean which don't compile for them.

[Gabriel Ebner]

The failure is in the external smt2_interface package.

[Gabriel Ebner]

And it shouldn't affect nightlies (they are uploaded in another configuration)

[Kevin Buzzard]

Oh that's good :-)

[Kevin Buzzard]

Since the recent incident where I upgraded Lean using my usual process and found mathlib not compiling, I've tried to become more aware of what actually happens here. So travis can give a red X at https://github.com/leanprover/lean/commits/master after a new commit but the nightly might change anyway?

[Kevin Buzzard]

Note that 8 out of the last 10 commits have been given red X's. Usually I would not care, but recent events have made me more cautious.

[Kenny Lau]

or just use git

[Gabriel Ebner]

Note that 8 out of the last 10 commits have been given red X's.

That's a diplomatic way to say "none of the last 20 builds have been successful". :smile:

[Kevin Buzzard]

I know I can use git Kenny, I am more concerned with people like Chris, who really don't want to have to download a bunch of stuff onto their (possibly low-spec) machine so they can spend hours compiling Lean.

[Gabriel Ebner]

There's already a PR for smt2_interface, I'll merge it and then travis should be green again.

[Kevin Buzzard]

I hope I'm not nagging. I just saw the effects of travis failure recently and was hoping not to have to go through it again. When Lean 3.4 appears there will be an alternative solution -- "get to 3.4 and then don't upgrade again".

[Kenny Lau]

stop that "don't upgrade again" crap

[Kevin Buzzard]

Kenny I need a solution which works for people who don't want to be bothered by upgrades. Imagine if all the software on your computer needed upgrading constantly and you had to build it from source.

[Kenny Lau]

not all softwares are beta

[Kevin Buzzard]

In practice I get people coming to Xena on Thursdays and they have managed to put their Lean in an unusable state and I just want to fix it with "download the nightly, use leanpkg upgrade/build, that's the end". This happened with Luca recently. He had edited a file in mathlib and then reverted his edits, but ended up with an olean file which did not match his lean file and this produced strange errors. We downloaded the nightly and fixed it really quickly. But with Chris more recently this approach did not work. Luca can't compile Lean from source without a huge amount of hassle.

[Gabriel Ebner]

@Kevin Buzzard The latest nightly is from Tuesday, did you expect a newer one?

[Gabriel Ebner]

@Sebastian Ullrich What is the recommended way to get nightlies in travis scripts these days (i.e. for mathib, etc.)?

[Kevin Buzzard]

@Gabriel Ebner I was just expressing concern about the recent red X's. I have not cared about them in the past, but then they bit me, so now I am more wary.

[Kevin Buzzard]

Basically I reported a lean assertion violation in the lean issues tracker, and then thought "hmm maybe I should upgrade to the latest nightly to check it's still there" and then I thought "but wait, there's a red X so there's a chance that upgrading will break mathlib, which is far more of a problem to me than anything else"

[Gabriel Ebner]

To be fair, mathlib is broken with the current nightly. (The unit_eq lemma is gone.)

[Kevin Buzzard]

My algorithm for dealing with the fact that this is beta software is "upgrade to latest nightly iff it won't cause a problem with mathlib".

[Kevin Buzzard]

My current test for this is "are there any signs of red X's in the list of commits? If not, was the last mathlib commit some time after the last Lean commit? If so, upgrade!"

[Kevin Buzzard]

I would be happy to be told about better tests. Ideally I want to be able to do the tests without bothering anyone else, but I would rather fail in the sense that I didn't upgrade when upgrading was possible, because failing by upgrading and then finding mathlib doesn't compile hurts me more (it's harder to roll back).

[Gabriel Ebner]

Why is it hard to roll back? You can just download the previous nightly. If you haven't seen it yet: https://github.com/leanprover/lean-nightly/releases

[Kevin Buzzard]

It's hard to roll back because leanpkg upgrade upgrades mathlib to HEAD

[Kevin Buzzard]

so I have to manually intervene and figure out which version of mathlib I had before and then switch to this commit.

[Kevin Buzzard]

and in the past I have not made a note of which commit I was switching from.

[Kevin Buzzard]

More generally, when students have done something dumb like editing mathlib files and they were using a nightly from 2 months ago, if the current nightly does not work then I have to decide which version of mathlib to checkout with which version of the nightly.

[Kevin Buzzard]

These are problems I actually see in practice.

[Kevin Buzzard]

I am well aware that this is software which is not quite "end-user ready" yet, but somehow I am just trying to give examples of the problems I see and am hoping that we are actually almost in a position to be able to solve them. I had not seen the nightly releases link -- thanks. I had heard talk about it but I hadn't really understood that it had happened.

[Kevin Buzzard]

If leanpkg could download the "approved mathlib commit" for each of the nightlies then this would be perfect. But maybe this is asking too much. I should however be able to download the nightly onto a student's machine, look at the commit #, and then guess an appropriate mathlib commit.

[Kevin Buzzard]

This is important because it means I don't need to compile Lean on a student's machine.

[Sebastian Ullrich]

@Gabriel Ebner

@Sebastian Ullrich What is the recommended way to get nightlies in travis scripts these days (i.e. for mathib, etc.)?

I was planning to figure out a script that also correctly takes lean_version into account, but at that point we're halfway to a proper leanget application that would also be useful to end users...

[Sebastian Ullrich]

@Gabriel Ebner I guess this works :)

curl -s https://api.github.com/repos/leanprover/lean-nightly/releases | jq -r '.[0].assets | map(select(.name | contains("linux"))) | .[0].browser_download_url'

[Kevin Buzzard]

I wonder if it works on a fresh OS X install?

[Kenny Lau]

why does the latest build fail?

[Kenny Lau]

@Mario Carneiro