Lean Incremental Compilation?

Stream: new members

[Andrew Elsey]

Hi, I'm currently parsing output from a lean file just by calling lean in a loop. We can't compile all of the files involved and it goes very slowly. We've been trying to figure out what the plugin is doing and it looks like it's using lean's --server option, for which there is limited but some documentation. I think mainly all we need is incremental compilation. I just wanted to check for those familiar if indeed implementing a client for the server mode is indeed the right rabbit hole to go down.

[Eric Wieser]

I assume your loop that calls into lean is also modifying the files?

[Andrew Elsey]

Usually yes. Although right now I'm just printing off the file from scratch every turn, but eventually yes, should only change one or perhaps a few lines every iteration

[Jason Rute]

First, make sure you are not starting up the server every time, (although if you keep it running but work with different files, you might have memory leaks). However, even if you leave the server open every sync will take 200ms, so you can’t do better than that really. It is a hard coded delay in the code.

[Jason Rute]

You can compile an individual file with lean —make. It will also compile the dependencies if they are not already compiled, but if you know what the dependencies are and they don’t change, that will speed things up.

[Andrew Elsey]

Jason Rute said:

First, make sure you are not starting up the server every time, (although if you keep it running but work with different files, you might have memory leaks). However, even if you leave the server open every sync will take 200ms, so you can’t do better than that really. It is a hard coded delay in the code.

Thanks!