Zulip Chat Archive

Stream: new members

Topic: MacOS install using MacPorts?


view this post on Zulip Philip Vetter (Jul 15 2020 at 07:13):

How to install using MacPorts, if possible?

view this post on Zulip Johan Commelin (Jul 15 2020 at 07:14):

I don't know of any Mac users using such a set up...

view this post on Zulip Johan Commelin (Jul 15 2020 at 07:14):

I think brew is the more popular route

view this post on Zulip Philip Vetter (Jul 15 2020 at 07:15):

I am under the impression that Brew and MacPorts do not well coexist.

view this post on Zulip Johan Commelin (Jul 15 2020 at 07:15):

I don't know anything about MacPorts, but my guess is that you can adapt https://leanprover-community.github.io/install/macos_details.html to MacPorts

view this post on Zulip Philip Vetter (Jul 15 2020 at 07:17):

It looks like you only use Brew to install python3 and pipe. Am I missing anything? Using MacPorts should be equivalent.

brew install python3 pipx
pipx ensurepath
pipx install mathlibtools

view this post on Zulip Johan Commelin (Jul 15 2020 at 07:18):

brew install gmp coreutils

view this post on Zulip Johan Commelin (Jul 15 2020 at 07:18):

If you scroll up a bit (I linked to the middle of the page :face_palm: )

view this post on Zulip Johan Commelin (Jul 15 2020 at 07:19):

Btw, I don't really know Mac... so this is just hearsay.

view this post on Zulip Philip Vetter (Jul 15 2020 at 07:22):

Right you are. Thanks for the pointers!

view this post on Zulip Philip Vetter (Jul 15 2020 at 07:26):

Reading is Fundamental! ;)

view this post on Zulip Philip Vetter (Jul 15 2020 at 07:41):

sudo port install coreutils
appears to install both GNU coreutils and GNU GMP as a dependency. So that's good so far.

view this post on Zulip Philip Vetter (Jul 15 2020 at 07:43):

Is python3.8 (or 3.7?) an acceptable choice? MacPorts seems to want a particular 3.x choice of python3

view this post on Zulip Johan Commelin (Jul 15 2020 at 07:43):

The newer the better

view this post on Zulip Philip Vetter (Jul 15 2020 at 07:50):

Python 3.8 then. One advantage -- it will be supported until 2024-10. That's a whole 50 months!

view this post on Zulip Scott Morrison (Jul 15 2020 at 07:52):

I use to install Lean's dependencies via macports, but haven't for ~2 years. homebrew is better :-)

view this post on Zulip Amos Turchet (Jul 15 2020 at 07:57):

I've done with MacPorts and everything works fine

view this post on Zulip Amos Turchet (Jul 15 2020 at 07:57):

I installed through ports python 3.8 pipx and coreutils

view this post on Zulip Philip Vetter (Jul 15 2020 at 13:24):

something went wrong with dyld; VSC error:
dyld: Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib
Referenced from: /Users/a/.elan/toolchains/stable/bin/lean
Reason: image not found

INSTALL ERROR:
$ leanproject get lftcm2020
Cloning from https://github.com/leanprover-community/lftcm2020.git
info: downloading component 'lean'
7.2 MiB / 7.2 MiB (100 %) 1.7 MiB/s ETA: 0 s
info: installing component 'lean'
dyld: Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib
Referenced from: /Users/a/.elan/toolchains/leanprover-community-lean-3.17.1/bin/lean
Reason: image not found
Command '['leanpkg', 'configure']' died with <Signals.SIGABRT: 6>.

view this post on Zulip Markus Himmel (Jul 15 2020 at 13:27):

Looks like @Scott Morrison had the same problem two years ago, and the answer seemed to be to switch to homebrew: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/nightly.20version.20stapling/near/124795748

view this post on Zulip Bryan Gin-ge Chen (Jul 15 2020 at 13:29):

Where does macports install libgmp? Maybe you just have to make a symbolic link in /usr/local/opt/... that points to the macports gmp location.

(Though I would also second the recommendation to just use homebrew.)

view this post on Zulip Scott Morrison (Jul 15 2020 at 13:33):

I never looked back. :-)

view this post on Zulip Amos Turchet (Jul 15 2020 at 13:39):

When I installed everything through MacPorts there was an issue at the end about paths where the stuff was installed that has been solved by using pipx instead of pip and then manually adding the .profile path to the .bash_profile path

view this post on Zulip Amos Turchet (Jul 15 2020 at 13:39):

not sure if this solves your issue (that didn't happen to me) but could be worth trying

view this post on Zulip Amos Turchet (Jul 15 2020 at 13:39):

(I meant the .profile path to the .bash_profile file)

view this post on Zulip Philip Vetter (Jul 15 2020 at 13:41):

Ah MacPorts puts things in places like
/opt/local/lib/libgmp.10.dylib

view this post on Zulip Philip Vetter (Jul 15 2020 at 13:42):

ensurepath didn't seem to make the changes it claimed it did. Maybe because Catalina shifted from bash to zsh and I'm still using bash. I will try Amos's suggestion.

view this post on Zulip Philip Vetter (Jul 15 2020 at 14:11):

I think there is an early problem with the elan-init.sh. It seems to work correctly but says
stable installed - (error reading lean version). <==== !

info: syncing channel updates for 'stable'
info: latest update on stable, lean version v3.17.1
info: downloading component 'lean'
7.2 MiB / 7.2 MiB (100 %) 1.1 MiB/s ETA: 0 s
info: installing component 'lean'
info: default toolchain set to 'stable'
stable installed - (error reading lean version)
Elan is installed now. Great!

view this post on Zulip Scott Morrison (Jul 15 2020 at 14:47):

Unfortunately I don't think any regulars have moved to Catalina yet, so Lean on Catalina is entirely untested.

view this post on Zulip Scott Morrison (Jul 15 2020 at 14:48):

Knowing whether it works with the standard install instruction (i.e. homebrew) would be much more useful than knowing about behaviour under macports, however.

view this post on Zulip Jalex Stark (Jul 15 2020 at 17:29):

i'm on macOS catalina 10.15.4
i set things up with brew


Last updated: May 13 2021 at 05:21 UTC