Build all Lean files inside a directory into executables

Stream: general

[Ciro Santilli]

Full details at: https://proofassistants.stackexchange.com/questions/6460/how-to-build-all-lean-files-inside-a-directory-into-executables In case someone knows of an obviously better way.

[Damiano Testa]

Does something like #general > Running lean-action in all files @ 💬 work in this case?

[Ciro Santilli]

I couldn't figure out how to use it, e.g.:

[[lean_exe]]
name = "Main.*"
root = "Main.*"

blows up:

error: lakefile.toml:25:7: expected name

The problem presumably is that it can't match name and root one by one, it would just expand both to all files.

globs itself does not seem to be a valid optoin to lean_exe: https://lean-lang.org/doc/reference/latest/Build-Tools-and-Distribution/Lake/#Lake___LeanExeConfig