Zulip Chat Archive

Stream: new members

Topic: Using mathlib in Lean project created using leanpkg


Donald Sebastian Leung (Feb 23 2020 at 14:42):

Suppose I create a Lean project as follows:

$ leanpkg new project
$ cd project
$ leanpkg add leanprover-community/mathlib

I then create a new file Preloaded.lean in src/. Now, say I want to import data/real/cau_seq.lean from mathlib. How do I do so? I've tried import data.real.cau_seq but Lean complains that it is not in the LEAN path. I've also tried import .._target.deps.mathlib.src.data.real.cau_seq, i.e. using relative paths as described in 6.1. Importing Files in TPIL but it emits a host of warnings and errors on imports within data/real/cau_seq.lean itself. Any help would be much appreciated :smile:

Patrick Massot (Feb 23 2020 at 14:43):

Are you sure you launch VScode from the correct folder?

Patrick Massot (Feb 23 2020 at 14:44):

please use cd project and then code .

Donald Sebastian Leung (Feb 23 2020 at 14:45):

Thanks for your reply. Is code . a Terminal command?

Patrick Massot (Feb 23 2020 at 14:45):

yes

Patrick Massot (Feb 23 2020 at 14:46):

You could also do that by clicking, but typing commands in a terminal is much easier

Donald Sebastian Leung (Feb 23 2020 at 14:46):

Hmmm ... I get a "command not found" error. Is code part of a proper Lean installation?

Patrick Massot (Feb 23 2020 at 14:46):

Aren't you using VScode?

Patrick Massot (Feb 23 2020 at 14:46):

What OS are you using?

Donald Sebastian Leung (Feb 23 2020 at 14:46):

macOS Catalina

So I can access the terminal from VSCode?

Patrick Massot (Feb 23 2020 at 14:47):

Ok, you are making your life difficult by using a user-hostile OS.

Patrick Massot (Feb 23 2020 at 14:47):

Forget about the command line then.

Patrick Massot (Feb 23 2020 at 14:48):

Launch VScode and find "Open" in the menus. Now select your "project" folder, not one of its subfolders.

Patrick Massot (Feb 23 2020 at 14:48):

Then try again importing a mathlib file.

Donald Sebastian Leung (Feb 23 2020 at 14:50):

Done (I think?), but apparently Lean is still complaining.

If you don't mind, I would like to include a screenshot here (my project folder is 0.999... = 1? Prove it!):

螢幕截圖-2020-02-23-22.50.16.png

Kenny Lau (Feb 23 2020 at 14:51):

wow, a fellow HongKonger!

Kevin Buzzard (Feb 23 2020 at 14:51):

This looks absolutely fine!

Patrick Massot (Feb 23 2020 at 14:51):

Could you paste the content of leanpkg.path?

Donald Sebastian Leung (Feb 23 2020 at 14:52):

Sure:

builtin_path
path _target/deps/mathlib/src
path ./src

Kevin Buzzard (Feb 23 2020 at 14:52):

The error says that you can't import data.real.cau_se which is correct, because without the q isn't not a valid import.

Kevin Buzzard (Feb 23 2020 at 14:52):

When you typed the q, Lean succeeded in importing the file, and that's why there's an orange bar on the left

Patrick Massot (Feb 23 2020 at 14:52):

Well spotted Kevin!

Kevin Buzzard (Feb 23 2020 at 14:53):

the old error is not cleared, but it will be once that file is compiled, which will take a very long time if you didn't already compile mathlib

Patrick Massot (Feb 23 2020 at 14:53):

So Donald now needs to learn about update-mathlib

Kevin Buzzard (Feb 23 2020 at 14:53):

so what you need is the mathlib olean files, which are usually obtained by update-mathlib on the command line

Donald Sebastian Leung (Feb 23 2020 at 14:53):

Oh ...

Thanks for pointing this out @Kevin Buzzard

Daniel Keys (Feb 23 2020 at 14:54):

@Donald Sebastian Leung Donald, in VS Code go to View -> Command Palette; type Shell Command in the line that appears and choose "Install code command in PATH"

Daniel Keys (Feb 23 2020 at 14:55):

Then you can run "code ." in your project directory.

Kevin Buzzard (Feb 23 2020 at 14:55):

He has opened the folder in VS Code now so this problem is solved (just not in the way Patrick initially suggested)

Donald Sebastian Leung (Feb 23 2020 at 14:55):

Daniel Keys said:

Donald Sebastian Leung Donald, in VS Code go to View -> Command Palette; type Shell Command in the line that appears and choose "Install code command in PATH"

Done, thanks

Kevin Buzzard (Feb 23 2020 at 14:56):

The only problem left is that the olean files need to be created. After leanpkg add leanprover-community/mathlib the usual mantra is leanpkg configure followed by update-mathlib

Patrick Massot (Feb 23 2020 at 14:58):

All this nonsense will disappear very soon.

Kevin Buzzard (Feb 23 2020 at 14:59):

Actually perhaps leanpkg add leanprover-community/mathlib already does everything leanpkg configure would do, so perhaps the only missing step is update-mathlib which should download all the olean files from "the cloud"

Kevin Buzzard (Feb 23 2020 at 15:00):

(thus saving you the 30 minutes or however long it takes to compile mathlib yourself these days, something I have not done for a long time now)

Daniel Keys (Feb 23 2020 at 15:02):

Here's a piece of advice from my experience with mathlib: avoid creating your project in a directory mapped onto cloud storage. I had a lot of trouble with the timestamps being messed up/rewritten by regular syncing with the cloud, and it took me a long time to figure it out. Local directory on your machine w/o continuous sync is best.

Patrick Massot (Feb 23 2020 at 15:03):

Everything in this ecosystem assumes you'll be using Git for storage, sharing, synchronization. Using a Dropbox-like thing on top is clearly asking for trouble.

Daniel Keys (Feb 23 2020 at 15:05):

That is indeed the case. The problem is that not everyone has GitHub experience to start with.

Patrick Massot (Feb 23 2020 at 15:06):

It doesn't have to be GitHub, you could host git repository anywhere you want.

Daniel Keys (Feb 23 2020 at 15:06):

Read "GitHub" as git, the problem persists.

Kevin Buzzard (Feb 23 2020 at 15:11):

I store all my lean projects in an EncFS encrypted directory and the encrypted directory is in my Dropbox, and it works fine on Linux. My impression is that the different OSs have different issues with timestamps

Kevin Buzzard (Feb 23 2020 at 15:11):

But I can absolutely update mathlib at home and then it works in the office

Daniel Keys (Feb 23 2020 at 15:14):

Yes Kevin, I think there are differences. I use mainly a Mac. When I switch temporarily to Linux and back, trouble arises. Besides, there are different cloud storage suppliers, with Dropbox sync among the best. Just something to be aware of.

Patrick Massot (Feb 23 2020 at 15:18):

Feel free to PR a line adding a warning to https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md


Last updated: Dec 20 2023 at 11:08 UTC