Zulip Chat Archive

Stream: general

Topic: brew install lean


view this post on Zulip Sean Leather (Sep 04 2018 at 18:13):

Has anybody tried brew install lean on macOS lately? I thought it had stagnated, but the formula is actually up to date with v3.4.1. I just installed it and lean --version worked just fine. Haven't done anything else, yet.

view this post on Zulip Simon Hudon (Sep 04 2018 at 18:14):

Does it install elan?

view this post on Zulip Sean Leather (Sep 04 2018 at 18:14):

No.

view this post on Zulip Simon Hudon (Sep 04 2018 at 18:15):

I feel like that's the only thing it should install.

view this post on Zulip Sean Leather (Sep 04 2018 at 18:17):

Well, there was discussion recently about installing lean from GitHub and not having gmp (https://github.com/leanprover/lean/issues/1971), so I think it's important for some people to know that brew install lean might work just fine.


Last updated: May 14 2021 at 02:15 UTC