compile directory

Stream: lean4

[Kevin Buzzard]

I have a repository containing many directories called things like Chapter37 and subdirectories containing files such as statements and solutions to exercises in this chapter. How do I use lake to build all the Lean files in a subdirectory of a repo? Do I have to make an analogue of Mathlib.lean?

[Scott Morrison]

Unfortunately you need to create a file that imports everything you want compiled, or do some shell scripting...

[Martin Dvořák]

I think @Mac fixed it.

[Kevin Buzzard]

$ find M1FExplained/Chapter01/Exercises/*.lean
M1FExplained/Chapter01/Exercises/Exercise01.lean
M1FExplained/Chapter01/Exercises/Exercise02.lean
M1FExplained/Chapter01/Exercises/Exercise05.lean
M1FExplained/Chapter01/Exercises/Exercise06.lean
M1FExplained/Chapter01/Exercises/Exercise07.lean

That's about the limit of my scripting skills and even that looks a bit dubious. Now I need some regex to turn the output into something Lake can understand with .s instead of /s and no .lean at th eend?

[Martin Dvořák]

If you are on leanprover/lean4:nightly-2023-07-12 you can do it like I did:
https://github.com/madvorak/chomsky/blob/main/lakefile.lean

[Martin Dvořák]

You will probably want something like:

lean_lib «Exercises» {
  globs := #[.submodules `M1FExplained]
  moreLeanArgs := #["-DautoImplicit=false"]
}

However, I am not sure what to do if Chapter01 and so on are directly in the project directory.

[Martin Dvořák]

The above works if the project directory contains M1FExplained and that contains Chapter01 and so on.