Lake shipping pre-compiled binaries?

Stream: lean4

[Andrés Goens]

A question that popped up in #Lean Together 2025 > Marcus Rossel: Egg: An Equality Saturation Tactic in Lean @ 💬:

AFAIK Lake currently doesn't allow to ship pre-compiled binaries to avoid dependencies right now, right? Is that something that is potentially in the horizon? (@Mac Malone )

[Andrés Goens]

I guess that's potentially a lake + reservoir question rather, in some sense

[Malvin Gattinger]

I don't know anything about lake, but I would wonder how this works for different (combinations of) operating systems and CPU architectures. Would packages then include binaries for each? Or can a package say "I only exist/work on amd64"?

[Andrés Goens]

yep, in other package managers (e.g. pip in python, etc), bundled binaries often just come separately for each architecture (triple)

[Abdalrhman M Mohamed]

@Andrés Goens You can run lake upload <tag> to pack everything in the .lake/build directory (including binaries) into an artifact and upload it to a GitHub release with the same tag. If your package is a dependency of another package and has the preferReleaseBuild option set to true, lake will download the artifact instead of rebuilding your package (assuming the versions match). I did this for the lean-cvc5 FFI and can confirm that it works for Linux and macOS (I haven't tried it on Windows yet). And yes! You need a seperate artifact for each target triple.

[Marcus Rossel]

@Abdalrhman M Mohamed Thanks! I've managed to build a release based on your steps :) A problem I'm running into now is that when I create a project with lean-egg as a dependency, it still tries to build lean-egg from source. Have you run into issues like that with lean-cvc5?

I think I'm setting the required properties correctly in the lakefile. And I'm referring to the tag of the release when importing lean-egg in another project:

[[require]]
name = "egg"
git  = "https://github.com/marcusrossel/lean-egg"
rev  = "nightly-2025-01-22"

So I don't understand why it's trying to build from source anyway.

[Abdalrhman M Mohamed]

@Marcus Rossel, apologies for the delayed response. I have encountered this issue as well. It appears that Lake downloads the artifact and builds it in parallel, likely treating them as independent jobs. Adding pkg.afterBuildCacheAsync to the external library target should resolve this problem.

[Marcus Rossel]

lean4#7032

[Marcus Rossel]

Ahh, it seems afterBuildCacheAsync isn't exactly what we need for lean-egg. The given function still always runs the subsequent build job, even if it was able to fetch the cached files:

/--
Perform a build job after first checking for an (optional) cached build
for the package (e.g., from Reservoir or GitHub).
-/
def Package.afterBuildCacheAsync (self : Package) (build : JobM (Job α)) : FetchM (Job α) := do
  if self.name ≠ (← getRootPackage).name then
    (← self.maybeFetchBuildCache).bindM fun _ => do
      setTrace nilTrace -- ensure both branches start with the same trace
      build
  else
    build

(Our goal is to only run cargo if we were unable to retrieve the cached files.)

Is there some way to run the build only if the cached files could not be retrieved? Or does there exist a notion of an "empty job" which could be returned in that case?

[Mauricio Collares]

Mathlib depends on ProofWidgets, which has a compilation step (with npm instead of cargo) that's usually skipped. Maybe you can imitate the relevant part of the lakefile?