Omit compilation and run the executable binary in the .lake

Stream: Is there code for X?

[Asei Inoue]

My motivation

• I develop lean-by-example repository
• I use Lean lib mk-exercise in lean-by-example
• It takes around 600 ms in my environment to run the lake exe mk_exercise. Running mk_exercise.exe in the .lake directory will finish in a few milliseconds. running mk_exercise.exe is by far the quickest.
• I think this is because when we run lake exe mk_exercise, the compilation is performed.

[Asei Inoue]

My Question

How can we skip compilation?
Is there a variant of the lake exe command that will not compile if there is a binary in the .lake directory?

[Asei Inoue]

impossible?

[Henrik Böving]

lake exe is supposed to execute the binary that is yielded by compiling the lean_exe target that it is followed by, what would you expect to happen?

[Henrik Böving]

If you have already compiled the executable fully and your thing is still taking long that is probably the overhead from lake itself launching, lake won't do any unnecessary work.

[Henrik Böving]

And if you have not compiled your executable with the latest version of your source files then lake exe compiling the executable for you is also the correct behavior given that you probably want the up to date executable

[Asei Inoue]

I tried lake upload, but running time of lake run ... is still slow...

[Asei Inoue]

lake exe is supposed to execute the binary that is yielded by compiling the lean_exe target that it is followed by

Thank you!

[Asei Inoue]

that is probably the overhead from lake itself launching,

If so, the overhead of Lake seems to be very large...

[Henrik Böving]

Either that or you are recompiling the binary, I don't know your setup. You can profile it if you want to find out

[Asei Inoue]

lake exe is very slow, as shown in the following:

lean-by-example on  main [$!]
❯ Measure-Command { .lake/packages/mk-exercise/.lake/build/bin/mk_exercise.exe Examples/Solution Exercise }

Days              : 0
Hours             : 0
Minutes           : 0
Seconds           : 0
Milliseconds      : 19
Ticks             : 193731
TotalDays         : 2.24225694444444E-07
TotalHours        : 5.38141666666667E-06
TotalMinutes      : 0.000322885
TotalSeconds      : 0.0193731
TotalMilliseconds : 19.3731


lean-by-example on  main [$!]
❯ Measure-Command { lake exe mk_exercise Examples/Solution Exercise }

Days              : 0
Hours             : 0
Minutes           : 0
Seconds           : 0
Milliseconds      : 837
Ticks             : 8375452
TotalDays         : 9.69381018518518E-06
TotalHours        : 0.000232651444444444
TotalMinutes      : 0.0139590866666667
TotalSeconds      : 0.8375452
TotalMilliseconds : 837.5452

[Asei Inoue]

I don't know your setup.

Can you reproduce this issue?

[Henrik Böving]

Your link to lean by example above is dead so no I cant

[Asei Inoue]

Sorry, this is correct link:

https://github.com/lean-ja/lean-by-example

[Henrik Böving]

It takes more like 200ms for me but yeah lake exe is just doing some work to check if your binary is up to date:
image.png

judging from that flame graph there also appears to be a call to git that is computing lots of SHA sums for some reason, in strace I can also see that the git process ends up checking every single file in every dependency, that just takes a while, especially if your hardware isn't as recent.

@Mac Malone is it really necessary to look at every file everywhere? That sounds to me like we're going to see linear growth in startup time for lake as people build bigger and bigger projects.

[Mac Malone]

@Henrik Böving This comes from Lake's checking for local changes to dependencies (lean4#2425). I agree that this edge case is probably something not worth checking on every workspace load (especially as it does not scale). I am not sure of a good heuristic on when to check it, though.

[Asei Inoue]

@Henrik Böving Thank you!

[Asei Inoue]

@Mac Malone

Is it possible to give the lake exe command the option to simply execute an already existing binary? (without checking if it is up-to-date or not)

Alternatively, if you check that the HASH in the lake-manifest has not changed, you obviously do not need to recompile.

[Mac Malone]

@Asei Inoue An option to not build seems like a reasonable request. Feel free to make an RFC for it on the Lean 4 repo.

I do not see how the hash in the Lake manifest would imply that an exe is up-to-date?

[Asei Inoue]

@Mac Malone In this case, the binaries in the .lake directory are not necessarily up-to-date. If you change the version of mk-exercise that you refer to, the executable in the .lake directory may be out of date. The only time you should re-run the compilation for an update would be if there is an update to the lake-manifest.

[Henrik Böving]

No, if a file that is (transitvely) imported by your binary changes your binary needs to be rebuild as well.

[Asei Inoue]

I made an RFC on lean4 repo https://github.com/leanprover/lean4/issues/5238

[Henrik Böving]

Mac Malone said:

Henrik Böving This comes from Lake's checking for local changes to dependencies (lean4#2425). I agree that this edge case is probably something not worth checking on every workspace load (especially as it does not scale). I am not sure of a good heuristic on when to check it, though.

Maybe we could first check the condition that make does (i.e. ensure the file touch date thing) and only if files were touched check them against their expected hash? That would remove hash computation in basically all use cases.

[Asei Inoue]

@Mac Malone @Hening Xu

A command to install binaries in Lake would solve this problem.

For example,

1. running lake install mk-exercise will copy the mk-exercise pre-built binary to the ~/.lake/bin/mk-exercise directory.
2. Add .lake/bin/mk-exercise to the PATH
3. From then on, the mk-exercise command can be executed without using the lake exe.

Could you tell me your opinion on this?

There must be others besides me who need a solution to this problem.

[Kim Morrison]

There is a tracking issue for lake install at lean#3423.

However, @Mac Malone's plans for this have changed, and I don't remember what they actually are now. @Mac Malone, any chance you could leave a comment on that issue with the current plan?

[Mac Malone]

A command along the lines of @Asei Inoue's lake install is a future plan. However, it has not yet become a priority. It is also different from the lake install of lean4#3423, which is for binaries with Lean toolchain integration (and thus need different binaries for different oolchains), whereas the one Asei is proposing would a one-and-done binary (like cargo install).

[Kim Morrison]

(@Mac Malone, could you leave that comment on the issue so it is findable?)