building executables from packages

Stream: lean4

[Jon Eugster]

Can I somehow modify my lakefile to automatically build a certain executable of a dependency? I'm looking at these lake docs but I'm not quite sure what to use, maybe extraDepTargets?

Ill demonstrate here with a project depending on mathlib and look at the cache executable, although my use case is a different package and different executable. In the example below, I would like to have the executable be built after calling lake build

# clean start
$ rm -rf .lake

# build the project
$ lake build
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git to './.lake/packages/mathlib'
...
[0/2] Fetching proofwidgets cloud release
[1/33] Building Aesop.Nanos
...
[403/404] Building Game

# e.g. the `cache` executable is not built yet
$ ls .lake/packages/mathlib/.lake/build/
ir  lib

# executing it, will build it first
$ lake exe cache
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: [5/9] Compiling Cache.Requests
info: [5/9] Building Cache.Main
info: [7/9] Compiling Cache.Main
info: [9/9] Linking cache
Mathlib4 caching CLI
Usage: cache [COMMAND]
...

# now it exists
$ ls .lake/packages/mathlib/.lake/build/bin/
cache  cache.hash  cache.trace

[Utensil Song]

lake build only builds the default target

[Utensil Song]

Annotating lean_exe with @[default_target] is what you need for building the executable by default. lake build cache is what you need to build and not run cache.

[Jon Eugster]

It is tagged by @[default_target] just in the dependency's lakefile.

lake build cache is doing the right thing, thanks! Now I wonder how I manage that I can simply call lake update -R && lake build instead of lake update -R && lake build && lake build cache :thinking:

Can I mark cache as default_target in my lakefile even if it comes from another package? Or can I maybe call lake build cache in a post-update hook in my lakefile :thinking:

[Jon Eugster]

probably just copying what mathlib does in its post-update-hook should work, I think

[Jon Eugster]

Indeed, adding the following hook to the package defining the executable seems to work:

/--
When a package depending on GameServer updates its dependencies,
build the `gameserver` executable.
-/
post_update pkg do
  let rootPkg ← getRootPackage
  if rootPkg.name = pkg.name then
    return -- do not run in GameServer itself

  /- TODO: Could we use the Lake API instead of spawning a new process? -/
  let toolchain := ← IO.FS.readFile <| pkg.dir / "lean-toolchain"
  let exitCode ← IO.Process.spawn {
    cmd := "elan"
    args := #["run", toolchain.trim, "lake", "build", "gameserver"]
  } >>= (·.wait)
  if exitCode ≠ 0 then
    logError s!"{pkg.name}: failed to build gameserver"

Thanks @Utensil Song !

[Mac Malone]

@Jon Eugster Regarding the TODO, I believe the following should do what you want here:

discard <| runBuild gameserver.build >>= (·.await)

[Jon Eugster]

@Mac Malone in v.4.7.0 I had the following post_update-hook, but Lake.LeanExeConfig.build does not exist anymore. Since the PR removing it (lean4#3835) is quite big, could you please help me adjusting the following snippet?

@[default_target]
lean_exe gameserver {
  root := `GameServer
  supportInterpreter := true
}

post_update pkg do
  let rootPkg ← getRootPackage
  if rootPkg.name = pkg.name then
    return
  discard <| runBuild gameserver.build >>= (·.await) -- error: environment does not contain Lake.LeanExeConfig.build

[Mac Malone]

@Jon Eugster I believe runBuild gameserver.fetch should work.

[Jon Eugster]

Almost, thanks!

Now it's just

invalid field 'await', the environment does not contain 'System.FilePath.await'
  x✝
has type
  FilePath

but I think I might figure that out in a minute

[Jon Eugster]

Oh just removing the >>= (·.await) entirely, thanks!