Zulip Chat Archive

Stream: general

Topic: travis failing, works locally?


view this post on Zulip Scott Morrison (May 13 2019 at 03:57):

My PR on the rewrite_all tactic (a precursor to rewrite_search) keeps failing on travis, although it compiles fine locally. I've restarted the build several times on travis. Not sure what to do?

view this post on Zulip Scott Morrison (May 13 2019 at 03:57):

https://travis-ci.org/leanprover-community/mathlib/builds/529976394?utm_source=github_status&utm_medium=notification

view this post on Zulip Mario Carneiro (May 13 2019 at 04:49):

it looks like it's a pure timeout issue. It would be nice if we could see what files it's getting stuck on

view this post on Zulip Kevin Buzzard (May 13 2019 at 06:08):

Funny -- we have a lemma in the perfectoid project which works on travis and times out locally

view this post on Zulip Simon Hudon (May 13 2019 at 12:00):

@Kevin Buzzard Does it time out when you call Lean from the command line?

view this post on Zulip Kevin Buzzard (May 13 2019 at 12:01):

if and only if I put -T100000

view this post on Zulip Kevin Buzzard (May 13 2019 at 12:01):

My comment is not mysterious -- I'm just observing that travis calls Lean with no -T option, but VS Code puts -T100000 by default

view this post on Zulip Simon Hudon (May 13 2019 at 12:01):

@Scott Morrison I restarted it to see if it's a fluke

view this post on Zulip Johan Commelin (May 13 2019 at 12:01):

if and only if I put -T100000

Aah, you should try -T100001

view this post on Zulip Kevin Buzzard (May 13 2019 at 12:01):

I think I'll stick to Mario's solution in the other thread ;-)

view this post on Zulip Johan Commelin (May 13 2019 at 12:02):

But it's an "if and only if"!

view this post on Zulip Kevin Buzzard (May 13 2019 at 12:02):

ouch! you're right :-) Maybe my proof of one direction needs formalising.

view this post on Zulip Kevin Buzzard (May 13 2019 at 12:02):

Never trust a mathematician

view this post on Zulip Simon Hudon (May 13 2019 at 12:28):

@Scott Morrison I commented on this PR. You have multiple definitions with the same name.


Last updated: May 14 2021 at 06:16 UTC