Zulip Chat Archive

Stream: general

Topic: Problems with the installation of mathlib (Linux)


view this post on Zulip Bruno Bentzen (Oct 10 2018 at 03:22):

Hello,

I am trying to get mathlib working in a new package of mine. I did the following

leanpkg new my_project
cd my_project
leanpkg add leanprover/mathlib

then I created a test.lean file with import group_theory.subgroup and then #check is_subgroup, and I run

leanpkg build

but although I can see all .olean files in my_project/_target/deps/mathlib/group_theory/, I get the following error message in VS Code:

"invalid import: group_theory.subgroup
could not resolve import: group_theory.subgroup"

(although I heard that it is less crucial now, I also installed elan as described in https://github.com/leanprover/mathlib/blob/master/docs/elan.md).

After a few unsuccessful attempts, I decided to install mathlib globally instead with

leanpkg install leanprover/mathlib

now I have all .olean files in ~/.lean/_target/deps/mathlib but I am still getting the same error.

Finally, I am using Ubuntu and VS Code works perfectly in other Lean projects without mathlib.

Any help would be greatly appreciated!

Best,
Bruno

view this post on Zulip Bryan Gin-ge Chen (Oct 10 2018 at 03:38):

Hi Bruno, I'm guessing you didn't get any errors when you ran leanpkg build from the console? What happens if you run lean test.lean from the VS code console?

view this post on Zulip Mario Carneiro (Oct 10 2018 at 03:46):

Make sure you have opened vscode to the folder "my_project"

view this post on Zulip Bruno Bentzen (Oct 10 2018 at 03:53):

Hi Bryan and Mario! Thank you for your prompt response. I am sorry, I am a still a VS code newbie --- could you please tell me how do I run lean test.lean from the VS code console and how do I open VS code to the my_project folder?

view this post on Zulip Bryan Gin-ge Chen (Oct 10 2018 at 04:09):

When you open VS Code, you can choose "Open folder" from the "File" menu, click on your my_project directory and press open.

To open a console in VS Code, choose "Terminal" from the "View" menu. That will open a terminal in the directory that you've opened in VS Code.

view this post on Zulip Bruno Bentzen (Oct 10 2018 at 05:10):

Hi Bryan (and Mario), yes, opening the folder solved the issue! (I'm sorry for the silly question, by the way!)

view this post on Zulip Scott Morrison (Oct 10 2018 at 05:22):

No problem! We're still sorting out the document and tutorials for these things, so it's great to have questions, so we know what needs to be said!

view this post on Zulip Bruno Bentzen (Oct 10 2018 at 05:24):

I see, Scott! Thank you guys!

view this post on Zulip Kevin Buzzard (Oct 10 2018 at 05:38):

Hi Bryan (and Mario), yes, opening the folder solved the issue! (I'm sorry for the silly question, by the way!)

It's not a silly question at all -- in fact it's a valuable data point! The community is currently desperately trying to get some comprehensible and failsafe instructions up and running.

view this post on Zulip Bruno Bentzen (Oct 10 2018 at 06:52):

I am glad to hear that, thanks Kevin! :)


Last updated: May 12 2021 at 22:15 UTC