faster type checking

Stream: general

[Bernd Losert]

Every time I run lean, it checks all of my .lean files. How do I generate .olean files from my .lean files so that only the changes .lean files are checked? I already have .olean files for mathlib, but I'm not sure how to do it for my own files.

[Kevin Buzzard]

Make your own olean files by running lean --make src in your project root directory

[Patrick Massot]

You can also run leanproject build

[Bernd Losert]

The --make option works nice. Thanks.

[Kevin Buzzard]

Sorry I always forget the "official solution" -- I was running lean --make before leanproject existed so I never upgraded that part of my brain.