Caching and slow files; saving snapshots to disk?

Stream: lean4

[Eric Wieser]

I have a ~300 line file, which on "my" machine (read: Gitpod) takes maybe 10 minutes to compile. I want to edit the proof at the very end of the file.

Right now, every time the lean process restarts (vscode closed, branch switched, etc), I have to pay this 10 minute penalty all over again.

Can save / stop help me here? Is there any plan yo serializing the "snapshots" that the LSP uses such that I can resume where I left off by loading from disk?

[Mac Malone]

@Eric Wieser I think the general advice here would be to split the file up, so the time-consuming portion is self-contained and thus can be cached in the disk via the olean. It also somewhat concerns me that you have a ~300 line file that take 10 minutes to compile.

[Scott Morrison]

But yes, Sebastian is working on this!