Unexpected leanpkg build behavior

Stream: lean4

[François G. Dorais]

Suppose we have two packages A and B, where B depends on A.

Package A has two files A/One.lean and A/Two.lean but the root A.lean imports A.One but not A.Two. Running leanpkg build for package A builds oleans for A.lean and A/One.lean but not A/Two.lean. So far this is good and economical.

However, package B has one file which imports A.Two. I would expect this to work since A/Two.lean is in package B's deps. But leanpkg build fails since it doesn't generate an olean file for A/Two.lean when building the dependency.

I can see how this behavior can make sense but I did not expect that. Is this a bug or is it the intended behavior?

[Mac]

Oh, this is actually a regression due to the basic leanpkg build no longer using leanmake and instead building files based on the imports of A.lean. If you run leanpkg build lib or leanpkg build bin, it will build every lean file in A.

[Mac]

See this comment in leanmake -- https://github.com/leanprover/lean4/blob/e8a958d8f363a8c56c1937a4e2c18ff9084b2060/src/lean.mk.in#L5 -- which states that every lean file within the package's directory (e.g., A in your case) is compiled.

[Mac]

To the question of whether this is a bug or feature, one of core developers (ex. @Sebastian Ullrich ) would need to comment as to whether, in the future, the plan is to only build imports (as the basic leanpkg build currently does) or to build every .lean in the package directory (as leanmake does).