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.5.0.rc1.r86.gad068824d0-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
Conflicts:	lean4
Provides:	lean4
Submitter:	Chocobo1
Maintainer:	Chocobo1
Last Packager:	Chocobo1
Votes:	0
Popularity:	0.000000
First Submitted:	2021-08-06 09:09 (UTC)
Last Updated:	2024-01-12 09:46 (UTC)

Dependencies (4)

glibc (glibc-git^AUR, glibc-linux4^AUR, glibc-eac^AUR, glibc-eac-bin^AUR, glibc-eac-roco^AUR)
gmp (gmp-hg^AUR)
cmake (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)