Package Details: lean 4.27.0-1

Git Clone URL: https://aur.archlinux.org/lean.git (read-only, click to copy)
Package Base: lean
Description: Lean 4 programming language and theorem prover
Upstream URL: https://github.com/leanprover/lean4
Keywords: formal-methods proof-assistant theorem-prover
Licenses: Apache-2.0
Submitter: daskol
Maintainer: daskol
Last Packager: daskol
Votes: 5
Popularity: 0.000057
First Submitted: 2024-11-07 20:23 (UTC)
Last Updated: 2026-02-07 22:49 (UTC)

Dependencies (7)

Required by (0)

Sources (1)

Latest Comments

ruffy commented on 2025-10-03 08:38 (UTC)

I think you also need to remove

options=('ccache')

from the PKGBUILD.

daskol commented on 2024-11-30 17:56 (UTC)

@xnuk Fixed.

xnuk commented on 2024-11-30 16:27 (UTC)

Error: Cannot find the ccache binary required for compiler cache usage.

Please add ccache to dependencies. I have to do pacman -S ccache to install this package.

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