Why does it always say "unknown package 'Mathlib'"? Thanks.

Stream: mathlib4

[Lewis]

Why does it always say "unknown package 'Mathlib'"? Thanks.

[Bolton Bailey]

Possibly you are working in a Lean project that does not list mathlib as a dependency. If you provide more details about what situation you are in someone is more likely to be able to help.

[Utensil Song]

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20my.20first.20lean.20program

Likely the same issue.

[Utensil Song]

I guess you are seeing this from the Lean Infoview. It's my knee-jerk reaction to fix this in command line so I forgot the details. You might just need a lake -R update mathlib and lake build.

[Utensil Song]

@Marc Huisinga might have more clues to fix it using only the VSCode extension if you provide more details.

Particularly, how did you create/open the Lean project? The result could be different for opening it from different directory.

[Kevin Buzzard]

Often the answer to this question is the far more mundane "I opened a random file called test.lean without ever setting up a lean project"

[Lewis]

Thank you for your reply. How to fix the error:

"error: [root]: no configuration file with a supported extension: ././lakefile.lean ././lakefile.toml"

when running "lake update"? Thanks a lot!

Utensil Song said:

Marc Huisinga might have more clues to fix it using only the VSCode extension if you provide more details.

Particularly, how did you create/open the Lean project? The result could be different for opening it from different directory.

[Lewis]

Kevin Buzzard said:

Often the answer to this question is the far more mundane "I opened a random file called test.lean without ever setting up a lean project"

Thank you for your reply. How to fix the error:

"error: [root]: no configuration file with a supported extension: ././lakefile.lean ././lakefile.toml"

when running "lake update"? Thanks a lot!

[Lewis]

Now running lake updatedoes not encounter the error, but why  does it still say "unknown package 'Mathlib'"? Thanks!

[Kim Morrison]

@Lewis, you're going to need to explain how you created your project, which instructions you followed, etc.

[Kim Morrison]

Posting your lakefile.lean (or lakefile.toml, depending on which you have) might also be helpful.

[Kevin Buzzard]

Again I'll conjecture that the user has no project at all and is just running lean on a standalone file, which doesn't work

[Kevin Buzzard]

Can the OP please send a screenshot of VS Code showing the error and with the file explorer open?

[Lewis]

Kevin Buzzard said:

Again I'll conjecture that the user has no project at all and is just running lean on a standalone file, which doesn't work

Here is the screenshot:

https://docsend.com/view/x4ijgz9bfhzrv8mt

Could you please help me make Mathlib importing work? Thanks a lot!

[Lewis]

Kim Morrison said:

Lewis, you're going to need to explain how you created your project, which instructions you followed, etc.

Here is the content of the file:

import Lake
open Lake DSL

package mil where
leanOptions := #[
⟨pp.unicode.fun, true⟩, -- pretty-prints fun a ↦ b ⟨autoImplicit, false⟩,
⟨`relaxedAutoImplicit, false⟩]

@[default_target]
lean_lib MIL where

require mathlib from git "https://github.com/leanprover-community/mathlib4"@"master"

Could you please help me make Mathlib importing work? Thanks a lot!

[Lewis]

Kim Morrison said:

Lewis, you're going to need to explain how you created your project, which instructions you followed, etc.

Here is the content of the file:

import Lake
open Lake DSL

package mil where
leanOptions := #[
⟨pp.unicode.fun, true⟩, -- pretty-prints fun a ↦ b ⟨autoImplicit, false⟩,
⟨`relaxedAutoImplicit, false⟩]

@[default_target]
lean_lib MIL where

require mathlib from git "https://github.com/leanprover-community/mathlib4"@"master"

Could you please help me make Mathlib importing work? Thanks a lot!

[Patrick Massot]

The project seems to be MIL so there is definitely no issue in the Lean file. The issue has to be that you don’t open the right folder in VSCode (or don’t open a folder at all but open a file).

[Patrick Massot]

We need a screenshot where we see the VSCode file explorer open.

[Utensil Song]

From the screenshot, you have only open a standalone file te.lean on desktop, with no project structure, that's causing the error. You need to check out the project structure of https://github.com/leanprover-community/mathematics_in_lean and organize the files in a similar way.

[Patrick Massot]

And no need to use an external site to post screenshot, pasting an image here is fine.

[Patrick Massot]

Utensil, you make it sound more complicated than it needs to be.

[Patrick Massot]

Lewis, you simply need to tell VSCode to open the folder containing the lakefile.

[Marc Huisinga]

Patrick Massot said:

The project seems to be MIL so there is definitely no issue in the Lean file. The issue has to be that you don’t open the right folder in VSCode (or don’t open a folder at all but open a file).

This is not necessary anymore. The problem is very likely what Kevin and Utensil suggested, namely that there is a file te.lean that is in a folder Desktop/my_project above the mathematics_in_lean folder that contains the Lean project, whereas my_project is probably not a Lean project itself. For MiL in particular it may obviously still make sense to open the right folder, though, given that the explorer view is more restrictive.

Utensil Song said:

Marc Huisinga might have more clues to fix it using only the VSCode extension if you provide more details.

Particularly, how did you create/open the Lean project? The result could be different for opening it from different directory.

The right first step here is to ask users to run the Troubleshooting: Show Setup Information command and then paste the output on Zulip. It will tell you whether Lean is running in a project or in a standalone file.