debug deterministic timeout

Stream: general

[Bernd Losert]

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]

Is this on a branch?

[Bernd Losert]

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

[Bernd Losert]

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

[Adam Topaz]

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

[Bernd Losert]

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

[Junyan Xu]

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.