beginner question: imports

Stream: new members

[Dean Young]

Here's an example that works:

import data.int.basic

What happens when I import something? Where on my computer is data.int.basic?

[Shreyas Srinivas]

There is an elan folder usually in the home directory, that contains all your toolchains.

[Shreyas Srinivas]

Within it, you would find, among other things, some basic library files. Mathlib imports (and anything else downloaded by lake as a dependency) are stored inside a folder called lake-packages inside the project directory.

[James Gallicchio]

(^ at least in Lean4 if you're using Lake; lean3 package system was a lot more ad-hoc I believe)

[Notification Bot]

This topic was moved here from #mathlib4 > beginner question: imports by Floris van Doorn.

[Floris van Doorn]

This seems to be a question about Lean 3, so moving it to a different stream.

[Floris van Doorn]

In Lean 3 every project is supposed to have a leanpkg.toml file which contains all the dependencies. Then, if you import a file, it will look at:

• The current project
• Any dependency as marked by the leanpkg.toml file, which usually exists in a _target subdirectory.
• The Lean core library itself (the elan tool should take care of putting these in a subfolder of your home directory).

[Eric Wieser]

Slightly more precisely, when you run leanpkg configure it reads your leanpkg.toml and outputs a leanpkg.path. It is this .path file (or the LEAN_PATH environment variable in its absence) that is what is used to resolve import data.int.basic to some_folder/data/int/basic.lean.

[Eric Wieser]

You can run lean --path to see how lean processed the leanpkg.path file.

[Dean Young]

Thanks for all of your help, this is good info!