RFC: lake exe variant without compilation

[Seasawher]

Proposal

add option to lake exe which simply execute an already existing binary file, without compilation.

User Experience: How does this feature improve the user experience?

lake exe command running time improvement

Beneficiaries: Which Lean users and projects benefit most from this feature/change?

repos depend on other lean packages

Community Feedback

Omit compilation and run the executable binary in the .lake

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[Seasawher]

lake exe ... command is very slow compared to simply run binary file

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

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