Zulip Chat Archive

Stream: general

Topic: timeout in `cech_nerve`

Yury G. Kudryashov (Nov 27 2021 at 20:33):

I get "deterministic" timeout in algebraic_topology.cech_nerve in some branches, near line 66. I tried to squeeze simp but failed (squeeze_simp timeouts with 10x time limit, the output of simp? doesn't work).

Yaël Dillies (Nov 27 2021 at 20:34):

See https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2310312.20timeouts.20in.20cech_nerve

Adam Topaz (Nov 27 2021 at 20:37):

Seems like the Cech nerve is the most popular construction in mathlib now! :tada:

Last updated: May 02 2025 at 03:31 UTC