Import my own lean files

Stream: mathlib4

[Esteban Martínez Vañó]

Hi everyone.

How can I import my own lean files to another lean file?

I've tried several things but everything gives me an error.

Also, how can I update mathlib? Because in the documentation page for mathlib there are files that I don't have in my computer, I suppose because it has been updated.

[María Inés de Frutos Fernández]

Have you read this page?

[Esteban Martínez Vañó]

Okay, I hadn't read the last part. It is clear now how to update Mathlib

[Esteban Martínez Vañó]

But, I still don't know how to import my own files. I mean, if in a project I create some file "Example.lean" with some definitions and theorems, and after that I create another file "Example2.lean", how can I call the definitions and theorem in Example.lean?

[Edward van de Meent]

likely something along the lines of import MyProject.Path.To.Example might work

[Edward van de Meent]

i think the path is relative to the root folder.

[Esteban Martínez Vañó]

It doen't work. It says that no directory or file with that name exists. And, if I put it in one of the folders it says is looking at, it says that there is no .olean file with that name

[Yaël Dillies]

Can you take a screenshot of your directory tree in vscode?

[Esteban Martínez Vañó]

imagen.png

[Kevin Buzzard]

Can you post your lakefile.lean?

[Esteban Martínez Vañó]

Here it is, altough it is a new project I've created using the steps in the link above and I haven't changed anything apart from copying an archive to the root folder and trying to import that same archive.

lakefile.lean

[Kim Morrison]

You need to add lean_lib Nets where to your lakefile.lean

[Kim Morrison]

and then add Nets.lean in the root directory that imports everything from Nets.

[Kim Morrison]

You can add @[default_target] before lean_lib if you want lake build to automatically build it.

[Kim Morrison]

Otherwise you will need to use lake build Nets.

[Kevin Buzzard]

Right now Lean probably expects to see Lean files in a directory called FunctionalAnalysis judging by the lakefile, which doesn't mention Nets at all right now so I guess the error message is not surprising.

[Esteban Martínez Vañó]

Kim Morrison ha dicho:

You need to add lean_lib Nets where to your lakefile.lean

That worked. Thanks!

I suppose I'll have to do that for every new folder I create?

[Kim Morrison]

@Mac Malone I really think we need to change the default so that lake build at least builds everything in the main project directory. It seems the current choices we offer are:

• users must remember to add each file as an import line to the main Project.lean manually, as they create them.
• somehow find the glob incantation (e.g. I can never remember/find it, so can't recommend it to people)
• set up their own ad-hoc scripts to keep Project.lean up to date.

All of these choices are bad, right??

[Kim Morrison]

(@Esteban Martínez Vañó, sorry to hijack your thread, but yes.)

[Mac Malone]

@Kim Morrison Note that none of these would solve the issue of this thread, which is adding Lean files outside (next to) the library directory / file.

[Kim Morrison]

Yes, that's true. But still!

[Dan Velleman]

This is a point on which I think documentation could be improved. When I first starting using Lean, I assumed that any Lean file could import any other Lean file. I didn't know what "build" meant, I didn't know what an olean was, and I didn't know what a library was. I eventually figured those things out, but it took me a while. Is this all explained somewhere? In my reading, I didn't find it.

[Kim Morrison]

What would be the right places to put this documentation? (I agree, by the way, that there is some significant missing documentation here. lake shouldn't be assuming that its users know what "a build system" is, or have ever used one before.)

I think that the right approach here is to put paragraph long comments into the default lakefile.toml that Lake creates (cf. #4106), explaining how everything works (including down to the level of detail "here is where you put new files, and this is what you need to do to make sure lake build will include them).

[Mario Carneiro]

I would prefer minimal new comments in the lakefile, but a line linking to an online manual or quickstart seems fine

[Mario Carneiro]

I think it is worth at least thinking about what such a landing page should look like, the lake readme is not very discoverable and it's also trying to do too many things at once

[Mario Carneiro]

it should probably be rewritten as a subsection of the lean manual

[Dan Velleman]

I think that in addition to explaining what "build" means, it would be good to explain what "import" does. As I understand it (and someone please correct me if I've got it wrong), if you put import foo at the top of a file, then what gets imported is foo.olean, not foo.lean. And that means that you have to make sure that your lakefile is set up so that Lean will produce foo.olean. If you just put foo.lean in the top directory of your project, then Lean will be willing to open it and process it, but it won't produce foo.olean. You have to put foo.lean in a library to get Lean to produce foo.olean.

[Mario Carneiro]

This is true, but I think it would be best to explain this without including the concept of olean files, because you also can't just put a pre-compiled foo.olean at the top of your project and get import foo to work. The short version is that without a lakefile, import can only import files in lean core (i.e. Lean.*, Std.* and Lake.*). If you need anything else (including mathlib or your own project files) you need a project setup