Package Details: lean4-bin 4.16.0-1

Git Clone URL: https://aur.archlinux.org/lean4-bin.git (read-only, click to copy)
Package Base: lean4-bin
Description: An interactive theorem prover
Upstream URL: https://leanprover.github.io/
Licenses: Apache-2.0
Conflicts: lean4
Provides: lean4
Submitter: Chocobo1
Maintainer: Chocobo1
Last Packager: Chocobo1
Votes: 4
Popularity: 0.000045
First Submitted: 2021-08-06 08:02 (UTC)
Last Updated: 2025-02-03 07:45 (UTC)

Latest Comments

rnbguy commented on 2024-07-11 10:31 (UTC)

Following the weird release, package() should cd into lean-4.9.0-linux*.

Chocobo1 commented on 2022-02-01 18:52 (UTC)

Instead, move this package to "$pkgdir/opt/leanprover"

Good idea, done.

add a script at "/etc/profile.d/leanprover.sh" to deal with environment variables.

I'm concerned that this would only work on the next login, so I choose to link directly to the installed executables instead.

I've checked executables by "ldd ./bin/*", All executables links with relative path properly.

Good to know, thanks!

t3476 commented on 2022-02-01 14:39 (UTC)

New version also conflicts with many system libraries(glibc, llvm-libs, zlib) which are in HoldPkg, not resolvable by adding them in conflict list.

Instead, move this package to "$pkgdir/opt/leanprover", remove clang and lld from conflict list, add a script at "/etc/profile.d/leanprover.sh" to deal with environment variables.

export PATH=$PATH:/opt/leanprover/bin

I've checked executables by "ldd ./bin/*", All executables links with relative path properly. Neither LD_LIBRARY_PATH nor adding conflict list are required.