Zulip Chat Archive

Stream: general

Topic: faster `leanproject build`?

Michael Stoll (Apr 21 2022 at 14:01):

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 (Apr 21 2022 at 14:03):

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

Oliver Nash (Apr 21 2022 at 14:04):

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 (Apr 21 2022 at 14:04):

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

Johan Commelin (Apr 21 2022 at 14:05):

@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 (Apr 21 2022 at 14:05):

OK, thanks for the explanations and advice!

Alex J. Best (Apr 21 2022 at 14:41):

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 (Jul 01 2022 at 20:22):

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

Last updated: Dec 20 2023 at 11:08 UTC