Canonical project folder structure

Stream: new members

[Max Nowak]

Simple question because I can't quite figure it out based on the Lake github repo: What is the recommended way to structure my projects? I am used to the by-convention, and the 1:1 folder <-> namespace approach of Cargo.

So looking at https://github.com/leanprover/lake/tree/master/examples/deps/foo confuses me. Which file is the "root", is it Main.lean or Foo.lean? Is there a 1:1 mapping of files+folders to namespaces? Ideally there is some docs that I missed somewhere.

[Kevin Buzzard]

Is this a lean 3 or lean 4 question? If lean 4 then it will be more likely to be noticed in the lean 4 stream.

[Max Nowak]

Lean4. Ah..

[Henrik Böving]

There is no documentation regarding structuring of projects

There is also no 1:1 correspondence between files and namespaces since you can arbitrarily open any namespace in any file at any point in time via the namespace command to add definitions to it.

The standard structure is usually:

• a Main.lean (if your thing is a library only you can get rid of this requirement as demonstrated here: https://github.com/leanprover-community/mathlib4/blob/master/lakefile.lean) which contains your main function, think main.rs from rust
• a top level file called the same as your project, think lib.rs from rust
• a directory with the name of your project
• the top level file imports all relevant modules from the subdirectory so your project can be "imported as one" so to speak

Regarding submodules the compiler uses a style that basically replicates the one of the top level file and directory like here: https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Deriving.lean https://github.com/leanprover/lean4/tree/master/src/Lean/Elab/Deriving

sometimes you'll also see this "import file" containing relevant code on its own.