Zulip Chat Archive

Stream: general

Topic: brew install lean

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.

Simon Hudon (Sep 04 2018 at 18:14):

Does it install elan?

Sean Leather (Sep 04 2018 at 18:14):

No.

Simon Hudon (Sep 04 2018 at 18:15):

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

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: Dec 20 2023 at 11:08 UTC