vscode extension feature request

Stream: lean4

[Shreyas Srinivas]

Currently the extension seems to periodically call the elaborator and kernel and show results on the infoview. Thus we get a live update on the infoview for whatever we type in. This is awesome in many ways.

At the same time it might be nice to have an option that only runs lean on a file when the file is saved. Sometimes, when I am typing in some annoyingly long statement with sets/finsets etc, the extension gets stuck on some issue (such as typeclass inferences) even before I am done typing in everything. Sometimes it is just an incomplete import statement that I would have finished typing in a second. As I have pointed out in a thread or two before, some of these lean threads don't stop running until the extension is started, and my machine heats up. Currently the default value for Lean4: Elaboration Delay settings is 200 ms, so the extension starts 5 times before I am done typing a long import. Changing this setting to a higher value is a quick fix, but not ideal.

[Wojciech Nawrocki]

Note that the elaboration delay counter resets on every keypress, so if you type something in with less than 200ms (or whatever you set it to) between every keypress, elaboration should only run once. But maybe you already knew that! In any case update-on-save sounds like a useful feature, perhaps especially when the infoview is paused; could you make a feature request on the vscode-lean4 repo?

[Shreyas Srinivas]

Okay. Will do

[Shreyas Srinivas]

I think I have been told about the way elaboration timer resets (or read it somewhere) but, at least on macOS, there are spurious processes that continue to run in the background even after the relevant code is removed.

[Shreyas Srinivas]

But that's a different problem altogether

[Wojciech Nawrocki]

Shreyas Srinivas said:

I think I have been told about the way elaboration timer resets (or read it somewhere) but, at least on macOS, there are spurious processes that continue to run in the background even after the relevant code is removed.

Ah, yes, if you change imports, this will launch a process running lake print-paths. This process may continue to run for a while even when it is no longer needed because the file changed again. There are potentially some improvements to be made to the server and/or Lake to clean this up better.

[Shreyas Srinivas]

an update-on-save feature might at least give users control over when these processes are triggered

[Shreyas Srinivas]

It is not only with imports. This issue arises when writing statements that involve membership or subset relationship in finsets, fintypes (and possibly other places). No clue why.

[Sebastian Ullrich]

These are not quite the same issue. One is runaway processes, the other runaway elaboration threads

[Sebastian Ullrich]

(and we should solve both of them, but the runaway processes will probably be solved first)

[Shreyas Srinivas]

Okay. But on the whole, especially on weaker machines, an optional "update on save" feature would be nice to have. When chosen, both elaborator re-run and and infoview updates happen when the file is saved. Of course, when autosave is turned on, this automatically translates to the present behaviour.

[Shreyas Srinivas]

Github issue : https://github.com/leanprover/vscode-lean4/issues/305