Adding directories to LEAN_PATH

Stream: new members

[ROCKY KAMEN-RUBIO]

I'm trying to import a file that is not part of mathlib, but am getting an error that file 'tuto_lib' not found in the LEAN_PATH. I'm in VSCode and this file is in my current src directory. I've also tried moving it inside mathlib, right next to data (which I am able to open and use) but that still gives me the same error. I tried closing and reopening VSCode, and reloading all the files.

Context: This is on section 5 of @Patrick Massot 's tutorials.

[ROCKY KAMEN-RUBIO]

Here is the link to Patrick's post with the tutorial files https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Tutorials.20update/near/196123657

[Jalex Stark]

I think if it's at src/subproject/tuto_lib.lean then you can do import subproject.tuto_lib from anywhere
(where of course subproject is a variable)

[Kevin Buzzard]

If you're working in a Lean project, then just put all your Lean files in src and you should be able to import any files in that directory.

[ROCKY KAMEN-RUBIO]

Kevin Buzzard said:

If you're working in a Lean project, then just put all your Lean files in src and you should be able to import any files in that directory.

I tried putting it directly in the src folder (not in a subfolder of src) but still got the error.

Jalex Stark said:

I think if it's at src/subproject/tuto_lib.lean then you can do import subproject.tuto_lib from anywhere
(where of course subproject is a variable)

This seems to have resolved the issue. I'm confused why the other two things I tried (moving it to src and moving it into mathlib) didn't work though.

[Patrick Massot]

@ROCKY KAMEN-RUBIO You should never have to do something like this. Either you messed up or I messed up.

[Patrick Massot]

I cloned the tutorials project following instructions and can't reproduce this issue. It seems I didn't mess up.

[ROCKY KAMEN-RUBIO]

Patrick Massot said:

I cloned the tutorials project following instructions and can't reproduce this issue. It seems I didn't mess up.

Interesting. I'll poke around a little more. The error continues through the rest of the tutorials (but is fixed with @Jalex Stark 's suggestion).

[Patrick Massot]

But suggestion is precisely to stop "poking around". We can help you only if you describe which instructions you didn't follow.

[Patrick Massot]

Thinking about this away from keyboard, I realized the previous message in this thread probably sounds harsh. I apologize. This is only my frustration that we work like crazy to help beginners and it still doesn't work.

[Patrick Massot]

Let's get back to https://github.com/leanprover-community/tutorials/blob/master/README.md. After running leanproject get tutorials, you should have a folder tutorials containing:

tutorials/
├── leanpkg.path
├── leanpkg.toml
├── LICENSE
├── mk_exercises.py
├── README.md
├── src
│   ├── exercises
│   │   ├── 00_first_proofs.lean
│   │   ├── 01_equality_rewriting.lean
│   │   ├── 02_iff_if_and.lean
│   │   ├── 03_forall_or.lean
│   │   ├── 04_exists.lean
│   │   ├── 05_sequence_limits.lean
│   │   ├── 06_sub_sequences.lean
│   │   ├── 07bis_abstract_negations.lean
│   │   ├── 07_first_negations.lean
│   │   ├── 08_limits_negation.lean
│   │   └── 09_limits_final.lean
│   └── solutions
│       ├── 00_first_proofs.lean
│       ├── 01_equality_rewriting.lean
│       ├── 02_iff_if_and.lean
│       ├── 03_forall_or.lean
│       ├── 04_exists.lean
│       ├── 05_sequence_limits.lean
│       ├── 06_sub_sequences.lean
│       ├── 07bis_abstract_negations.lean
│       ├── 07_first_negations.lean
│       ├── 08_limits_negation.lean
│       ├── 09_limits_final.lean
│       └── tuto_lib.lean
└── _target
    └── deps
        └── mathlib ...

with a lot more stuff inside mathlib. Then the next instructions was to copy exercices as some other subfolder of src. Say you called it my_work. It should contain exactly the same list of files as exercices but those files may contains less sorries and more proofs. In particular tuto_lib.lean hasn't been moved anywhere, it is still in src/solutions

[Patrick Massot]

Also, you should be able to run from the tutorials folder:

$ cat leanpkg.path
builtin_path
path _target/deps/mathlib/src
path ./src/solutions

[Patrick Massot]

Which tells us that, if you correctly open this folder in VScode, Lean will find tuto_lib since it will look in ./src/solutions.