Zulip Chat Archive

Stream: general

Topic: building lean on arch fails


view this post on Zulip Lennard Henze (Aug 21 2019 at 18:49):

trying to build lean on 5.2.6-arch1-1-ARCH, but the build process fails. Anyone else using lean on arch? I can provide more information if someone is interested

view this post on Zulip Koundinya Vajjha (Aug 21 2019 at 19:32):

I'm using Lean on Arch, and i think I installed it using the instructions here: https://github.com/leanprover-community/mathlib/blob/a152f3a62f72395aaaa0f9199fdc207b918cf5ea/docs/install/linux.md

view this post on Zulip Koundinya Vajjha (Aug 21 2019 at 19:33):

I'm on 5.2.6-arch1-1-ARCH as well.

view this post on Zulip Lennard Henze (Aug 22 2019 at 12:49):

okay thanks, I want to use emacs, but if I dont find a solution soon, Ill probably use VSCode as well

view this post on Zulip Jesse Michael Han (Aug 22 2019 at 12:52):

those instructions also work with emacs

emacs doesn't require you to build lean from source

view this post on Zulip Jesse Michael Han (Aug 22 2019 at 12:53):

i'm using lean with emacs on manjaro, and used the same install instructions

view this post on Zulip Jesse Michael Han (Aug 22 2019 at 12:53):

you'll want to install elan first, though


Last updated: May 12 2021 at 04:19 UTC