search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.66k stars 419 forks source link

RFC: `lake exe` variant without compilation #5238

Open Seasawher opened 2 months ago

Seasawher commented 2 months ago

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 :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

Seasawher commented 2 months ago

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