Zulip Chat Archive

Stream: general

Topic: Strange timeout

Heather Macbeth (Jan 09 2022 at 05:41):

I'd be glad of help diagnosing a timeout at the lemma has_sum_repr_symm in #11255. I discussed with @Rob Lewis and he also couldn't see the issue.

I don't really have ideas for speeding it up -- I already rewrote to avoid all simps, for example. I actually get "goals accomplished" in VSCode for this proof, but the timeout shows up just the same.

Rob Lewis (Jan 09 2022 at 05:44):

The proof is complete, but the kernel hates it. I get the same timeout trying to add the declaration with a metaprogram.

Heather Macbeth (Jan 15 2022 at 09:08):

#11255 is now ready for review, I'd like to bump this question about a strange timeout in it!

Last updated: Dec 20 2023 at 11:08 UTC