syntax highlighting and infoview not working

Stream: lean4

[Jesse Slater]

I am having issues with syntax highlighting and the infoview not updating. It just gets stuck, and does not react to me changing the file. It updates again if I restart vscode, but then quickly goes back to not working. I have been restarting vscode every 5 minutes or so for the past hour. This just started today. Is there anything that could be causing this? What should I do to try to debug the issue?

[Jesse Slater]

Update: I have determined that the problem is just in one theorem. I suspect the issue is that I am using aesop in the theorem and it came up with a monster proof. Then whenever I edit the theorem, it runs again, and slows everything down. Does this sound plausible?

[Jannis Limperg]

Very possible. You can call aesop? to have it print the tactic proof, or set_option trace.aesop.proof in aesop to print the proof term, or set_option trace.aesop.steps in aesop to print the steps Aesop took. (The last one usually produces a lot of output.) If Aesop is slower than you'd expect given your rule set, I'd be happy to investigate.

[Jesse Slater]

Yeah, I replaced it with the tactic proof, and that fixed it. Thanks!