Leanproject flagging changed files

Stream: general

[Yakov Pechersky]

We often have users report of long compilation times, which might have to do with a modified in their directory that doesn't match the cached oleans. Would it be possible to have a script that flags which .lean do not match their corresponding .olean files? That is, the ones that would trigger a rebuild. This could even print out core lean filenames if they were somehow modified. Then, a lot of debugging for such users would first start with "leanproject identify-modifications | wc -l".

[Yakov Pechersky]

lean --make ... does something related as part of its compilation of the target file or folder. I'm proposing a tool just for identification of the files that are the "root" of the recompilation