Importing local file

Stream: lean4

[Sophie Morel]

Today in "really really stupid questions": I made this shiny new Lean4 project use lake, started coding, mathlib imports work fine, life is beautiful. Then I decided to split the project into several files, so I wrote a file GreatResults.lean, then created another file MorelGreatResults.lean and tried to start it with an import GreatResults. And now Lean says unknown package 'GreatResults'. :cry: (I'm using VSCode and I did try opening the directory of my project, but it doesn't seem to make a difference.)
But, I don't get it, that was working fine in Lean3 and the sections of TPIL3/4 on importing don't look that different. The only thing I noticed is that TPIL3 says that import foo imports the file foo.lean, while TPIL4 imports the file foo.olean. So I tried building the project and then quickly discovered that I had no idea how to do that. (I did a lake init GreatResults.lean followed by a lake build, and it created a lot of stuff but I don't see any olean files there. The lean files didn't have any errors in VSCode, though it did have a couple of sorry's.)

[Jannis Limperg]

Your project should have this structure:

lakefile.lean
lean-toolchain
GreatResults.lean
GreatResults/Morel.lean
GreatResults/...

I.e. all Lean files other than the toplevel GreatResults.lean go into the GreatResults directory. (Other setups are also possible, but need fiddling with the lakefile.)

The stuff about oleans is a red herring; they have the same function as in Lean 3 and importing also works similarly. lake build generates oleans, but places them into the build directory.

[Adam Topaz]

TDLR: Put your great results in the GreatResults folder, and in the parent GreatResults.lean file you can import GreatResults.RiemannHypothesis.

[Adam Topaz]

Also, in GreatResults/RiemannHypothesis.lean you will be able to import GreatResults.ZetaFunction

[Sophie Morel]

Wait, I am not sure that I follow. Does that mean that I need to have one top-level file (say GreatResults.lean) that can import a bunch of other lean files that have to be in the GreatResults directory, but these other lean files cannot import each other ?

[Adam Topaz]

no, the files in the GreatResults folder can indeed import others in the same folder, just with the name GreatResults.OtherFile instead of OtherFile

[Sophie Morel]

Ah, that is what your second message meant!

[Sophie Morel]

Do I need to have a src folder like in Lean3 ? That is what I did, but maybe I shouldn't have.

[Adam Topaz]

No, src is gone in lean4+lake

[Adam Topaz]

Take a look at the folder structure of std4, for example: https://github.com/leanprover/std4

[Adam Topaz]

mathlib4 is similar, but the lake setup is more complicated there: https://github.com/leanprover-community/mathlib4

[Sophie Morel]

Ok, I created a folder AwesomeProject, put my lean files there, and now they can import each other (and the imports also work in the toplevel file AwesomeProject.lean). Whew, thanks Adam and Jannis !