Search Criteria
Package Details: lean4 4.0.0.rc4-1
Package Actions
| Git Clone URL: | https://aur.archlinux.org/lean4.git (read-only, click to copy) |
|---|---|
| Package Base: | lean4 |
| Description: | Lean 4 programming language and theorem prover |
| Upstream URL: | https://github.com/leanprover/lean4 |
| Licenses: | Apache2 |
| Submitter: | dariost |
| Maintainer: | dariost |
| Last Packager: | dariost |
| Votes: | 4 |
| Popularity: | 0.000000 |
| First Submitted: | 2021-01-24 14:07 (UTC) |
| Last Updated: | 2023-08-31 05:05 (UTC) |
Latest Comments
lfairy commented on 2023-09-25 05:37 (UTC) (edited on 2023-09-25 05:39 (UTC) by lfairy)
If you're here to program in Lean (as opposed to building another AUR package that depends on Lean) then I recommend not installing Lean from AUR.
Either install elan directly from upstream (https://leanprover-community.github.io/install/linux.html), or – if you really want to use AUR – you can install elan-lean from AUR.
This is because, like other contemporary language toolchains, Lean updates quickly. Having one global version of the toolchain might work for slower-changing languages like C, but it'll fall flat when every Lean project requires a different version of the compiler.
t3476 commented on 2022-02-02 20:59 (UTC) (edited on 2022-02-02 21:00 (UTC) by t3476)
Submodule lake is required at 'src/lake' for lean to be built.
git submodules in PKGBUILD
lake