Zulip Chat Archive

Stream: new members

Topic: Timeout tips?


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?

Scott Morrison (Oct 23 2020 at 02:11):

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

Scott Morrison (Oct 23 2020 at 02:11):

Instead break out smaller lemmas.

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.

Bjørn Kjos-Hanssen (Oct 23 2020 at 02:24):

Thanks @Scott Morrison

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: Dec 20 2023 at 11:08 UTC