building lean on arch fails

Stream: general

[Lennard Henze]

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

[Koundinya Vajjha]

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

[Koundinya Vajjha]

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

[Lennard Henze]

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

[Jesse Michael Han]

those instructions also work with emacs

emacs doesn't require you to build lean from source

[Jesse Michael Han]

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

[Jesse Michael Han]

you'll want to install elan first, though