archlinux

Stream: general

[Kevin Buzzard]

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]

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

[Frédéric Dupuis]

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]

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

[Johan Commelin]

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

[Edward Ayers]

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]

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]

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

[Edward Ayers]

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

[Patrick Massot]

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]

Yeah something for lean4 maybe