Zulip Chat Archive
Stream: general
Topic: Timeout in ring_theory.polynomial.basic
Yaël Dillies (Mar 01 2023 at 09:20):
There is a timeout l. 970, if someone wants to investigate
Anne Baanen (Mar 01 2023 at 10:10):
Looks like simpa is spending 17.7s to prove something quite simple, alongside 500ms for executing other tactics...
Anne Baanen (Mar 01 2023 at 10:13):
David Loeffler (Mar 01 2023 at 15:08):
Anne Baanen said:
Looks like
simpais spending 17.7s to prove something quite simple, alongside 500ms for executing other tactics...
Sorry for hijacking the thread here, but how does one find out how long individual tactics take? Is there some kind of profiler mode that can be activated?
Eric Wieser (Mar 01 2023 at 15:10):
set_option profiler true
Anne Baanen (Mar 01 2023 at 15:16):
Works in Lean 3 and in Lean 4 :)
Last updated: Dec 20 2023 at 11:08 UTC