Zulip Chat Archive

Stream: new members

Topic: Timeout tips?


view this post on Zulip Bjørn Kjos-Hanssen (Oct 23 2020 at 02:07):

I have a 445 line file that suffers from (deterministic) timeout problems. Are there some easy ways to avoid that?
Is the use of tactics likely to compound the problem?
Maybe I should be separating some parts into other files and use import?

view this post on Zulip Scott Morrison (Oct 23 2020 at 02:11):

It's typically single declarations that are the problem. Splitting into multiple files won't help.

view this post on Zulip Scott Morrison (Oct 23 2020 at 02:11):

Instead break out smaller lemmas.

view this post on Zulip Scott Morrison (Oct 23 2020 at 02:12):

It is usually, but not always, tactics that cause timeouts. However unification ("heavy rfl") can be arbitrarily slow! Often this can be fixed by making definitions (more) irreducible.

view this post on Zulip Bjørn Kjos-Hanssen (Oct 23 2020 at 02:24):

Thanks @Scott Morrison

view this post on Zulip Kevin Buzzard (Oct 23 2020 at 06:38):

Feel free to post working code if you want people to make more precise comments. Note that it has to run though (all imports, definitions etc must be there).


Last updated: May 15 2021 at 02:11 UTC