Zulip Chat Archive

Stream: new members

Topic: mathlib and Lean 3.4.2


view this post on Zulip Alexandre Rademaker (Jul 02 2020 at 00:51):

Is mathlib compatible with the Lean 3.4.2 official release?

view this post on Zulip Bryan Gin-ge Chen (Jul 02 2020 at 00:51):

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

edit: fixed branch name

view this post on Zulip Alexandre Rademaker (Jul 02 2020 at 01:05):

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.

view this post on Zulip Bryan Gin-ge Chen (Jul 02 2020 at 01:11):

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 ?

view this post on Zulip Alexandre Rademaker (Jul 02 2020 at 01:22):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 02 2020 at 01:28):

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.

view this post on Zulip Alexandre Rademaker (Jul 02 2020 at 01:57):

I am using emacs

view this post on Zulip Alexandre Rademaker (Jul 02 2020 at 01:57):

Thank you. I will try the suggested setup


Last updated: May 14 2021 at 06:16 UTC