Zulip Chat Archive

Stream: general

Topic: debug deterministic timeout


Bernd Losert (Jul 18 2022 at 19:54):

So I running into a deterministic timeout when I use a lemma in a proof. When I comment it out, everything works again. Is there a way to debug what is going on?

Adam Topaz (Jul 18 2022 at 20:00):

Is this on a branch?

Bernd Losert (Jul 18 2022 at 20:02):

Not in mathlib, but it's a github project set up with gitpod.

Bernd Losert (Jul 18 2022 at 20:03):

https://github.com/berndlosert/convergence/blob/master/src/convergence_space/algebra.lean#L245 <-- Here's the problem.

Adam Topaz (Jul 18 2022 at 20:08):

It will be hard to diagnose this because it's not on a mathlib branch, unfortunately.

Bernd Losert (Jul 18 2022 at 20:14):

That's OK. I'll try do finish the proof without the lemma. Maybe that will help.

Junyan Xu (Jul 19 2022 at 00:04):

So I running into a deterministic timeout when I use a lemma in a proof.

@Bernd Losert You should use a permalink like this; the line number may change with each commit. Is filter.inv_smul_of_smul the lemma in question?
image.png

Since this lemma is in another file in your project instead of in mathlib, it's indeed hard to diagnose unless you extract a #mwe with all imports in mathlib. If you want to diagnose yourself, one of the things to look into unification problems in the instance arguments of the lemma; for example, instead of exact ..., use convert ... using 1 (or a higher number), and check whether the instances match up in the widget.


Last updated: Dec 20 2023 at 11:08 UTC