Zulip Chat Archive

Stream: mathlib4

Topic: build 1 target

Johan Commelin (Feb 13 2023 at 14:49):

lake build builds the universe. On old hardware this takes a lot of time. If I am only interested in Mathlib/X/Y/Z.lean, how can I compile just that file and any deps that are out of date?

Jon Eugster (Feb 13 2023 at 14:53):

I think lake build Mathlib.Data.PNat.Basic

Floris van Doorn (Feb 13 2023 at 15:19):

From README.md of mathlib4:

You can use lake build +Mathlib.Import.Path to build a particular file, e.g. lake build +Mathlib.Algebra.Group.Defs.

Johan Commelin (Feb 13 2023 at 15:22):

Aah, thanks!

Floris van Doorn (Feb 13 2023 at 15:57):

I believe lake build Mathlib.Import.Path (without +) does roughly the same, except that it doesn't build the .ilean output file, which contains information related to jump-to-definition (within a single file) and the type-information pop-ups when mousing over something. So including the + is a little better.

Reid Barton (Feb 13 2023 at 16:05):

Is there a reason for this distinction to exist?

Reid Barton (Feb 13 2023 at 16:13):

Why would I ever not want to build the .ilean file?

Last updated: Dec 20 2023 at 11:08 UTC