faster `leanproject build`?

Stream: general

[Michael Stoll]

Sometimes it makes sense to add some definitions or lemmas to a mathlib file (like data.nat.prime or algebra.parity) that is imported by a lot of other files. When I do this and run leanproject build to get up-to-date oleans, this takes a very long time. On the other hand, I would think that just adding stuff cannot possibly break anything (unless a naming conflict arises), so it should be possible to get by with only recompiling the file that was changed and checking for name conflicts in the other files. Is there a way of doing this so that the build process is faster?

[Johan Commelin]

If you add a simp lemma, then the simp set changes, so many proofs could potentially break.

[Oliver Nash]

Sadly no but you can run lean --make src/path/to/high/level/file.lean rather than leanproject build to recompile just the oleans in between the low-level file you touched and the high-level file you're working on.

[Johan Commelin]

Idem dito, if you add an instance, some typeclass resolution might fail

[Johan Commelin]

@Michael Stoll My strategy is to develop things in a new file. And by the time I want to PR things, I move them in the right place, and send off the PR. A while later, the cloud will have generated the oleans for me.

[Michael Stoll]

OK, thanks for the explanations and advice!

[Alex J. Best]

Also see https://leanprover-community.github.io/tips_and_tricks.html#old-mode for one way to get files compiling quickly if you are sure you really only added something

[Yury G. Kudryashov]

I always use --old-mode and recompile only the files I touched. Then lean just uses existing oleans.