Prevent rebuilding package dependency

Stream: lean4

[Tomas Skrivan]

I have a package A that depends on package B through a github link. Now when I create a new project with lake and add package A as a dependency by pointing to A's directory. On building this new project, lake downloads and rebuilds package B. How can I prevent that? B is already in A's directory, downloaded and built.

[Mac]

@Tomas Skrivan use a local dependency rather than a git dependency. See, for instance, the foo lakefile in the deps example for the syntax.

[Tomas Skrivan]

Hmm, but what if I'm not a creator of A? Do I have to go an manually change dependency of A on B? What if I have a chain of packages A depends on B that depends on C all thought github.

My project then depends on A, I would have to go in and manually modify all those dependencies from github to local dependency?

[Arthur Paulino]

I'm facing something similar. lake is successfully able to find B if I use a local dependency but the only problem is that I'm not being able to choose the target build directory when I say (using Tomas' example) $ lake build B. Am I able to make it build at lean_packages/B/build/ instead of wherever B is located at?

[Mac]

@Tomas Skrivan sorry, I misread your initial statement. What your described is Lake working as expected. Lake creates a copy of each remote for the each workspace, so if package A and new package C both depend on the remote they will both get a copy of B in their lean_packages.

Part of the reason for this is that dependencies are transitive in Lean. So, if new package C has different workspace configurations from package A it needs to make sure it applies those when configuring B. Package C could also depend on a newer version of B than A as well, which is another reason for the copy. The plan is even to eventually hoist the build directory for packages into the top-level workspace as well eventually.

[Mac]

Arthur Paulino said:

Am I able to make it build at lean_packages/B/build/ instead of wherever B is located at?

No, but as I mentioned, build directories will hopefully be hoisted to the top-level workspace as well eventually (which would do something very similar to this).

[Tomas Skrivan]

I see, well I have probably slightly unusual use case of Lean in this scenario and I'm maybe taking the wrong approach. I want to use Lean as a scripting language in Houdini, something like Blender. I have a package HouLean that wraps some Houdini API into Lean's functions. This package depends on SciLean and that one depends on mathlib4.

Now each script I want to run, I create a new lake project that depends on HouLean through local dependency. However, compiling it with lake downloads whole SciLean and mathlib4 to this script project and rebuilds it. This takes some time. These scripts are supposed to be short and require very little customization. So I was thinking they might reuse already downloaded and built version of SciLean and mathlib4 from HouLean directory.

Alternatively, I should try to have all scripts in one lake project. Then each script would not get its own copy of those libraries.