incremental compilation

Stream: general

[Matthew Pocock]

In any reasonably sized lean file, when you are editing in the top half, there is a really noticeable delay as it rebuilds everything below, constantly. Including on things like whitespace, comment editing, that can not even in principle alter the type checking or evaluation of anything below. Are there any plans to make a more clever incremental compiler that only re-does work where changes to the text invalidates old values? I know that the scala compiler uses a combination of timestamps and checksums to enable this, in effect making the entire compiler into a reactive, time-indexed computation.

[Scott Morrison]

Yes, Sebastian has many plans in this direction. His WITP slides have some outlines about the module system. For inside a single file, there is the possibility of parallel elaboration of independent pieces (e.g. elaborating proofs of theorems without holding up the rest of the file). You may have to wait a bit for him to have time to explain detailed plans.

[Scott Morrison]

Also don't forget: you can split files in multiple smaller files. :-)

[Scott Morrison]

I've long wished we had a 1000 line linter in Mathlib!

[Damiano Testa]

A low-brow version of achieving this is to place #exit after the declaration that you are modifying, to prevent further compilation.

Also, I used to intersperse my code with #eval 0s, since editing a declaration had the effect of recompiling the one above it. This behaviour may have changed now, though.

When dealing with long proofs, sorrying or stopping already solved branches also helps.

[Matthew Pocock]

@Damiano Testa yup - I added an #exit for my sanity sake. At least I know this is on the radar of the devs.

[Ioannis Konstantoulas]

I didn't know about #exit! This is very convenient.

[Joachim Breitner]

“Very convenient” seems an exaggeration; I'd say it's a “decent workaround” for a relevant usability issue. I hope eventually interactive editing will be fully smooth :-)