## Stream: general

### Topic: archlinux

#### Kevin Buzzard (Oct 12 2020 at 18:21):

There seem to be 5 lean packages on aur.archlinux.org (this just tripped someone up at Imperial). e.g.

https://aur.archlinux.org/packages/lean-community/

(and all the other Lean packages it conflicts with). Is that really maintained by the Lean community?

#### Julian Berman (Oct 12 2020 at 18:25):

The most popular (and I guess correct) one says it's maintained by/in https://github.com/ouuan/AUR-packages

#### Frédéric Dupuis (Oct 13 2020 at 02:45):

It mi ght be good to include a warning somewhere to advise against installing Lean via package managers -- it's very tempting and almost certainly leads to trouble.

#### Frédéric Dupuis (Oct 13 2020 at 02:47):

I even went as far as writing a PKGBUILD for mathlib at some point before I realized the error of my ways.

#### Johan Commelin (Oct 13 2020 at 05:40):

@Frédéric Dupuis You mean that you don't run pacman -Syu 5 times per day? :rofl:

#### Edward Ayers (Nov 25 2020 at 12:31):

Frédéric Dupuis said:

I even went as far as writing a PKGBUILD for mathlib at some point before I realized the error of my ways.

What were the issues?

#### Frédéric Dupuis (Nov 25 2020 at 12:44):

mathlib just moves too fast for a PKGBUILD to be convenient, using leanproject is much better adapted to the task. This way, you can have a separate copy of mathlib for every project that you can update independently instead of a system-wide install. Besides, nowadays I only work directly on mathlib, so it would make even less sense.

#### Edward Ayers (Nov 25 2020 at 13:50):

I see. Maybe a pkgbuild that installs elan and leanproject would make sense

#### Edward Ayers (Nov 25 2020 at 13:51):

I really wish that elan, leanproject and leanpkg were the same thing

#### Patrick Massot (Nov 25 2020 at 13:58):

Merging leanproject and leanpkg would be trivial. I didn't see the point of redoing leanpkg inside leanproject but that would be very easy. Merging this with elan would take a bit more work (but of course there is no obstruction in principle).

#### Edward Ayers (Nov 25 2020 at 14:13):

Yeah something for lean4 maybe

Last updated: May 12 2021 at 23:13 UTC