How do I import a file?

Stream: lean4

[Victor Maia]

how do I import a file in the same dir? I'm trying import Base, but it says nat_exp.lean:1:0: error: unknown package 'Base', even though there is a file named Base.lean on the same directory, which type-checks just fine

[Kevin Buzzard]

I don't know much about Lean 4 but I do know that in the maths library they are always doing import Mathlib.Logic.Basic etc. If you're in a package then try aopending the package name?

[Victor Maia]

I'm not in a package I guess, I just created a directory and added 2 Lean files, and attempted to import one into another. I guess I'm missing something about how packages work

[Victor Maia]

also, import .Base results in nat_exp.lean:1:7: error: expected identifier

[Kevin Buzzard]

Again I don't know much about Lean 4, but in Lean 3 you can't just create random files and expect imports to work. A Lean 3 project is set up with some infrastructure which tells the system where to look when trying to import files. Aah! See https://leanprover.github.io/lean4/doc/quickstart.html , section "Create a Lean Project". This is for Lean 4 and it also says that imports won't work unless you make a new package or project or whatever these things are called in Lean 4 (they seem to be called both?)

[Adam Topaz]

I think the preferred way to make a new project is using lake new Foo (perhaps with some additional flags).

[Victor Maia]

i used lake new Foo, and then attempted lean Main.lean inside it, and I got Main.lean:1:0: error: unknown package 'Foo'

[Adam Topaz]

what are you trying to do? Build the package? Run the executable?

[Victor Maia]

I just want to type-check a file Main.lean which imports another file Base.lean. That's all. I don't want packages nor anything fancy

[Adam Topaz]

Anyway, this is all accomplished with lake. lake build will typecheck (and build) everything

[Victor Maia]

I want to type-check just a single file though. I have a Base.lean file which a bunch of definitions, and File_0.lean, File_1.lean, File_2.lean etc. etc., which import Base.lean. I want to type-check each file independently, to benchmark. But using lean File_0.lean tells me Base isn't a package.

[Adam Topaz]

I see. Unfortunately, I don't know how to accomplish that in Lean4.

[Adam Topaz]

Someone who knows will surely come along and help out soon.

[Victor Maia]

It is okay. Thanks for your patience!

[James Gallicchio]

Does lean Base.lean File_1.lean work?

[James Gallicchio]

I think lake figures out which files to pass to lean, but you can do that manually

[Juan Pablo Romero]

you have to declare it as library in lakefile.lean:

-- file: lakefile.lean
lean_lib Base

-- file: Main.lean
import Base

[Chris Lovett]

You will get real time type checking while you edit if you use VS Code. There's some lean4 sample with a demo video showing how easy it is to set this up on gitpod. Or if you want to use your local machine see Quick Tour of lean4 in VS Code.

[Sebastian Ullrich]

Victor Maia said:

I want to type-check just a single file though. I have a Base.lean file which a bunch of definitions, and File_0.lean, File_1.lean, File_2.lean etc. etc., which import Base.lean. I want to type-check each file independently, to benchmark. But using lean File_0.lean tells me Base isn't a package.

Once you have lake build working, you can run individual files using lake env lean File_0.lean.