travis failing, works locally?

Stream: general

[Scott Morrison]

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?

[Scott Morrison]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Simon Hudon]

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

[Kevin Buzzard]

if and only if I put -T100000

[Kevin Buzzard]

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

[Simon Hudon]

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

[Johan Commelin]

if and only if I put -T100000

Aah, you should try -T100001

[Kevin Buzzard]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Never trust a mathematician

[Simon Hudon]

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