Required Project Structure?

Stream: lean4

[Marcus Rossel]

What are the requirements for the structure of a Lean 4 project?
I currently have the following structure, which is causing me problems:

* reactor-model
    * leanpkg.toml
    * Main.lean
    * src
        * General
            * Thing1.lean
            * Thing2.lean
        * Specific
            * Some1.lean
            * Some2.lean

The leanpkg.toml:

[package]
name = "reactor-model"
version = "0.1"
lean_version = "leanprover/lean4:nightly-2021-07-11"

[dependencies]
mathlib4 = { git = "https://github.com/leanprover-community/mathlib4", rev = "1fd1cdc64b9a968e302ebd34af228b40cc05eb04" }

---

First of all, I don't actually want that Main.lean at the top level. But without it I get:

`leanpkg print-paths` failed:

stderr:
configuring reactor-model 0.1
mathlib4: trying to update build/deps/mathlib4 to revision 1fd1cdc64b9a968e302ebd34af228b40cc05eb04
> git checkout --detach 1fd1cdc64b9a968e302ebd34af228b40cc05eb04    # in directory build/deps/mathlib4
HEAD is now at 1fd1cdc Update Lean version.
> /Users/marcus/.elan/toolchains/leanprover--lean4---nightly-2021-07-11/bin/leanpkg build    # in directory build/deps/mathlib4/.
configuring mathlib4 0.1
no '.lean' file found in /Users/marcus/Arbeit/reactor-model

But even with Main.lean I can't manage to (e.g.) import Thing1 into Thing2.

If I do import src.General.Thing1 I get:

object file '/Users/marcus/.elan/toolchains/leanprover--lean4---nightly-2021-07-11/lib/lean/src/General/Thing1.olean' of module src.General.Thing1 does not exist

If I do import General.Thing1 I get:

unknown package 'General'
You might need to open '/Users/marcus/Arbeit/reactor-model' as a workspace in your editor

(I'm using VS Code for this).

---

It seems like the src folder isn't considered part of the project or something. How can I fix that?

The Format of leanpkg.toml states that there is a path parameter that can be set, but also that it will be removed in the future.

[Jannis Limperg]

You need to rename Main.lean into General.lean. I wrote up a little Lean 4 project template here; maybe you'll find that useful.

[Marcus Rossel]

Jannis Limperg said:

You need to rename Main.lean into General.lean. I wrote up a little Lean 4 project template here; maybe you'll find that useful.

Considering your blog post: Shouldn't my main file be src.lean then? Kind of like your example setup has Test.lean and then the Test directory which contains the other files?