Feature Request : Update on Save

[Shreyas4991]

A feature in which users will have an option to turn on 'update-on-save', which behaves as follows: When enabled, the elaborator re-run and infoview update happen whenever the current file is saved, instead of being triggered automatically at periodic intervals.

For details see this zulip thread

[kmill]

I'll mention another related idea, which is to be able to disable automatic elaboration and have a command that elaborates up to the end of the command that contains the cursor (Zulip). There could be another command to elaborate the whole file too (maybe it could be saving the file, like your suggestion).

[Shreyas4991]

This sounds a bit like vscoq. It would definitely be a nice-to-have option. Especially for running lean in machines with low resources or cloud environments which charge by resource usage.