VS Code extension, pause typechecking

Stream: lean4

[Kyle Miller]

Sometimes I don't want continuous typechecking, and my ideal interface would be to have some keybinding to trigger typechecking for the current file (maybe up to the current cursor position, or up to the next command after the current cursor position). Especially on a laptop, this can save battery life and help the editor UI be more responsive. Continuous typechecking can also seem to cause the server to use a whole lot of memory, especially when you're editing a large function with many match cases.

I've looked through the settings and Lean 4 commands, but I haven't seen anything that would at least let you pause typechecking. Is there anything like this? I'd rather not have to stop and start the server if possible.

[Kyle Miller]

I often use Gitpod as well for editing Lean 4, and I've noticed that continuous typechecking can make it almost impossible to do expansions due to how much stuff is happening on-screen after every keypress. I usually have to add an #exit nearby just to keep things calm enough to the expansion system actually detect that I've typed \to or whatever.

[Scott Morrison]

I would love this too!

[Scott Morrison]

Even more importantly, I really want VS Code to not start creating oleans for other files unless I explicitly hit cmd-R.

[Newell Jensen]

Something that would be nice is to have Lean syntax that would not type check certain sections.

section no_check or something along those lines. That way, for larger files where you don't want to comment out sections of code just to have things run faster you could just use that. I don't think this is currently available correct?

[Newell Jensen]

This would be more for user development at least.

[Reid Barton]

Newell Jensen said:

Something that would be nice is to have Lean syntax that would not type check certain sections.

section no_check or something along those lines. That way, for larger files where you don't want to comment out sections of code just to have things run faster you could just use that. I don't think this is currently available correct?

This might even be implementable as a user I guess?