File not found in the search path

Stream: new members

[Alberto Alfarano]

Hello,
I am a new member of the Zulip community and Lean overall!
I installed lean from https://leanprover-community.github.io/install/macos_details.html and Lean is working as expected when I do #eval 1+1.

Now I'm opening some files and from the first line I see some errors saying "file 'algebra/algebra/basic' not found in the search path
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more".

I tried lean --path and I got

"/Users/albealfa/.elan/toolchains/leanprover-community--lean---3.49.1/bin/../library",
"/Users/albealfa/.elan/toolchains/leanprover-community--lean---3.49.1/bin/../lib/lean/library",
"/Users/albealfa/<my_lean_folder>/_target/deps/mathlib/src",
"/Users/albealfa/<my_lean_folder>/./src"

and all of these files exist.

Fyi, which lean gives "/Users/albealfa/.elan/toolchains/leanprover-community--lean---3.49.1/bin/lean"

[Patrick Massot]

Are you using VSCode?

[Patrick Massot]

If yes then you should make sure to use "Open folder" and not "open file"

[Patrick Massot]

The file explorer should look like
image.png

[Alberto Alfarano]

Hi Patrick, thanks this fixed some imports. But some other imports (like algebra.floor) are still not found.

[Patrick Massot]

You may then have a mismatch between mathlib versions.

[Patrick Massot]

If you just created a project then you are using a cutting edge mathlib. You can see what currently exist on https://leanprover-community.github.io/mathlib_docs/ and there is no file algebra.floor

[Yaël Dillies]

I renamed algebra.floor to algebra.order.floor several months ago.

[Kevin Buzzard]

Where are you seeing algebra.floor? If this is in someone else's project then you could just download their project with leanproject get <github userid>/<name of project instead of making a new project. Their project might use a different version of mathlib.