Zulip Chat Archive
Stream: general
Topic: VScode extension on macOS
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?
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
Ryan Smith (Oct 04 2018 at 05:33):
On mac or linux?
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.
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.
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
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
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.
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
Ryan Smith (Oct 04 2018 at 05:57):
ah I just installed lean via binary download
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
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?
Bryan Gin-ge Chen (Oct 04 2018 at 06:10):
I've been using leanpkg as described here.
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.
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.
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.
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
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."
Kevin Sullivan (Oct 08 2018 at 14:07):
On OSX, do "brew install gmp"
Last updated: Dec 20 2023 at 11:08 UTC