Zulip Chat Archive

Stream: general

Topic: Timeout in `gromov_hausdorff_realized`

Yury G. Kudryashov (Jul 13 2021 at 08:29):

I get a timeout in gromov_hausdorff_realized (line 258) in some of my PRs but I can't reproduce it locally. Any ideas?

Oliver Nash (Jul 13 2021 at 08:31):

Did you see https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238279.20timeouts.20in.20gromov_hausdorff_realized.2Elean/near/245789291 ?

Yury G. Kudryashov (Jul 13 2021 at 08:32):

Thanks!

Last updated: Aug 03 2023 at 10:10 UTC