Using mathlib in Lean project created using leanpkg

Stream: new members

[Donald Sebastian Leung]

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]

Are you sure you launch VScode from the correct folder?

[Patrick Massot]

please use cd project and then code .

[Donald Sebastian Leung]

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

[Patrick Massot]

yes

[Patrick Massot]

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

[Donald Sebastian Leung]

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

[Patrick Massot]

Aren't you using VScode?

[Patrick Massot]

What OS are you using?

[Donald Sebastian Leung]

macOS Catalina

So I can access the terminal from VSCode?

[Patrick Massot]

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

[Patrick Massot]

Forget about the command line then.

[Patrick Massot]

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

[Patrick Massot]

Then try again importing a mathlib file.

[Donald Sebastian Leung]

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]

wow, a fellow HongKonger!

[Kevin Buzzard]

This looks absolutely fine!

[Patrick Massot]

Could you paste the content of leanpkg.path?

[Donald Sebastian Leung]

Sure:

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

[Kevin Buzzard]

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]

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]

Well spotted Kevin!

[Kevin Buzzard]

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]

So Donald now needs to learn about update-mathlib

[Kevin Buzzard]

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

[Donald Sebastian Leung]

Oh ...

Thanks for pointing this out @Kevin Buzzard

[Daniel Keys]

@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]

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

[Kevin Buzzard]

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]

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]

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]

All this nonsense will disappear very soon.

[Kevin Buzzard]

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]

(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]

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]

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]

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

[Patrick Massot]

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

[Daniel Keys]

Read "GitHub" as git, the problem persists.

[Kevin Buzzard]

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]

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

[Daniel Keys]

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]

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