Zulip Chat Archive

Stream: general

Topic: VScode extension on macOS


view this post on Zulip Ryan Smith (Oct 04 2018 at 05:21):

Do you need to append your lean/bin directory onto $PATH and then launch vscode from the command line in order for the extension to locate lean on macOS?

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

I put my elan path into my .bash_profile and then VS code was able to figure out the rest

view this post on Zulip Ryan Smith (Oct 04 2018 at 05:33):

On mac or linux?

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

On macOS 10.13 until a few days ago and macOS 10.14 since then.

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

It's also possible to just put the full path to your lean executable in the lean VS code extension settings and that ought to work as well.

view this post on Zulip Ryan Smith (Oct 04 2018 at 05:49):

Invoking lean from the command line as a sanity check produces:
dyld: Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib
Referenced from: /Users/bixbyr/lean-3.4.1/bin/./lean
Reason: image not found
Abort trap: 6

view this post on Zulip Ryan Smith (Oct 04 2018 at 05:52):

Nvm that looks like a more general brew issue to fix and probably doesn't have anything to do with lean

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

yeah, you just need to do brew install gmp. The fact that this isn't stated anywhere obvious is a well-known issue.

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

https://github.com/leanprover/lean/issues/1971 Supposedly, installing lean itself via homebrew should include gmp

view this post on Zulip Ryan Smith (Oct 04 2018 at 05:57):

ah I just installed lean via binary download

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

Yeah, I think the current recommended procedure might be to use elan https://github.com/Kha/elan

view this post on Zulip Ryan Smith (Oct 04 2018 at 06:06):

git clone mathlib to include/ or is there a more elegant way to get it and bring it into scope?

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

I've been using leanpkg as described here.

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

There's a strong possibility that you'll run into this issue if you're running lean 3.4.1.

view this post on Zulip Kevin Buzzard (Oct 04 2018 at 09:32):

A push was made to document elan properly at https://github.com/leanprover-community/mathlib/blob/elan-docs/docs/elan.md . If this document does not answer all your questions then please flag this here or even better submit a PR. It's time this was fixed. Sebastian is very busy with Lean 4, but we as a community can definitely make things like this better.

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

I think the merged version of that file in mathlib is actually more recent. However, as mentioned here and in the zulip conversation I linked above, Reid pointed out that those instructions won't get you the most recent version of mathlib since mathlib's leanpkg.toml specifies lean 3.4.1 and leanpkg add gives you the lean-3.4.1 branch, which is several months out of date.

view this post on Zulip Reid Barton (Oct 04 2018 at 14:59):

You can ignore that part of the instructions though and still use the instructions for installing elan

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

Right. To be fully explicit, I think the instructions should be edited to say something like "If you want to include an up-to-date version of mathlib in your project, use elan install nightly to install the latest version of lean. Then use leanpkg new my-project and leanpkg add <link to mathlib>. Make sure that leanpkg.toml in my-project has a line saying lean_version = nightly-something. Then run leanpkg upgrade, etc."

view this post on Zulip Kevin Sullivan (Oct 08 2018 at 14:07):

On OSX, do "brew install gmp"


Last updated: May 11 2021 at 00:31 UTC