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

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)

Required by (0)

Sources (1)

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