Zulip Chat Archive
Stream: lean4
Topic: building executables from packages
Jon Eugster (Dec 08 2023 at 14:56):
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 (Dec 08 2023 at 14:58):
lake build
only builds the default target
Utensil Song (Dec 08 2023 at 15:02):
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 (Dec 08 2023 at 15:07):
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 (Dec 08 2023 at 15:08):
probably just copying what mathlib does in its post-update-hook should work, I think
Jon Eugster (Dec 08 2023 at 15:28):
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 (Dec 09 2023 at 08:41):
@Jon Eugster Regarding the TODO, I believe the following should do what you want here:
discard <| runBuild gameserver.build >>= (·.await)
Last updated: Dec 20 2023 at 11:08 UTC