Arch Linux User Repository

Search Criteria

Enter search criteria

Search by

Keywords

Out of Date

Sort by

Sort order

Per page

Package Details: lean4-git 4.22.0.rc3.r161.gd2e604f74d-1

Package Actions

Git Clone URL:	https://aur.archlinux.org/lean4-git.git (read-only, click to copy)
Package Base:	lean4-git
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.000000
First Submitted:	2021-08-06 09:09 (UTC)
Last Updated:	2025-07-09 13:57 (UTC)

Dependencies (4)

glibc (glibc-git^AUR, glibc-eac^AUR)
gmp (gmp-hg^AUR)
cmake (cmake3^AUR, cmake-git^AUR) (make)
git (git-git^AUR, git-gl^AUR) (make)

Required by (0)

Sources (1)

git+https://github.com/leanprover/lean4.git

Latest Comments

Chocobo1 commented on 2023-03-02 20:34 (UTC)

Build fails with the following error:

Should be fixed now.

jorpic commented on 2023-03-02 19:39 (UTC)

Build fails with the following error:

CMake Error at CMakeLists.txt:533 (message):
  src/lake does not exist.  Please check out the Lake submodule using `git
  submodule update --init src/lake`.

lake is a package manager for Lean and it was added as a submodule some time ago (see https://github.com/leanprover/lean4/blob/master/.gitmodules)

mdl commented on 2017-10-02 10:35 (UTC)

The PKGBUILD needs to be fixed: ==> Starting pkgver()... ==> ERROR: pkgver is not allowed to contain colons, hyphens or whitespace. ==> ERROR: pkgver() generated an invalid version: 0.2.0.r13050.v3.3.0-9-gd83b9ef3e This page has some useful information for how to write a suitable pkgver(): https://wiki.archlinux.org/index.php/VCS_package_guidelines#The_pkgver.28.29_function