mathlib and Lean 3.4.2

Stream: new members

[Alexandre Rademaker]

Is mathlib compatible with the Lean 3.4.2 official release?

[Bryan Gin-ge Chen]

The lean-3.4.2 branch is, but current master is not.

edit: fixed branch name

[Alexandre Rademaker]

Thank you. So I am missing something. After leanpkg install leanprover-community/mathlib I stil get invalid : import data.real.basicin my test.lean file.

[Bryan Gin-ge Chen]

leanpkg install is not recommended, since this will create a single global installation of mathlib, as opposed to having a copy of mathlib local to your project.

Did you see the install instructions using leanproject here: #install ?

[Alexandre Rademaker]

Thank you. But despite the problem of a single global installation, there is any reason for this particular error?

[Bryan Gin-ge Chen]

The error just means that Lean isn't finding the imports. You could run lean --path in the same directory and see whether the result makes sense.

I don't have much experience with the global install, unfortunately. Are you trying to use VS Code with a global install of mathlib? I'm not sure how well-supported that is.

[Alexandre Rademaker]

I am using emacs

[Alexandre Rademaker]

Thank you. I will try the suggested setup