## Stream: general

### Topic: travis failing, works locally?

#### 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?

#### 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

#### 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

#### Simon Hudon (May 13 2019 at 12:00):

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

#### Kevin Buzzard (May 13 2019 at 12:01):

if and only if I put -T100000

#### 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

#### Simon Hudon (May 13 2019 at 12:01):

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

#### Johan Commelin (May 13 2019 at 12:01):

if and only if I put -T100000

Aah, you should try -T100001

#### Kevin Buzzard (May 13 2019 at 12:01):

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

#### Johan Commelin (May 13 2019 at 12:02):

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

#### Kevin Buzzard (May 13 2019 at 12:02):

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

#### Kevin Buzzard (May 13 2019 at 12:02):

Never trust a mathematician

#### 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