Zulip Chat Archive

Stream: new members

Topic: MacOS install using MacPorts?

Philip Vetter (Jul 15 2020 at 07:13):

How to install using MacPorts, if possible?

Johan Commelin (Jul 15 2020 at 07:14):

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

Johan Commelin (Jul 15 2020 at 07:14):

I think brew is the more popular route

Philip Vetter (Jul 15 2020 at 07:15):

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

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

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

Johan Commelin (Jul 15 2020 at 07:18):

brew install gmp coreutils

Johan Commelin (Jul 15 2020 at 07:18):

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

Johan Commelin (Jul 15 2020 at 07:19):

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

Philip Vetter (Jul 15 2020 at 07:22):

Right you are. Thanks for the pointers!

Philip Vetter (Jul 15 2020 at 07:26):

Reading is Fundamental! ;)

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.

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

Johan Commelin (Jul 15 2020 at 07:43):

The newer the better

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!

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 :-)

Amos Turchet (Jul 15 2020 at 07:57):

I've done with MacPorts and everything works fine

Amos Turchet (Jul 15 2020 at 07:57):

I installed through ports python 3.8 pipx and coreutils

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>.

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

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.)

Scott Morrison (Jul 15 2020 at 13:33):

I never looked back. :-)

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

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

Amos Turchet (Jul 15 2020 at 13:39):

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

Philip Vetter (Jul 15 2020 at 13:41):

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

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.

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!

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.

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.

Jalex Stark (Jul 15 2020 at 17:29):

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

Last updated: Dec 20 2023 at 11:08 UTC