guix_mirror_bot pushed a commit to branch master
in repository guix.
commit 404a14f879a63898eb379018dfbb39d4c3e0e9d8
Author: Andreas Enge <[email protected]>
AuthorDate: Mon Mar 9 11:12:47 2026 +0100
gnu: Remove lean.
* gnu/packages/lean.scm (lean): Delete variable.
Fixes: guix/guix#6239
Change-Id: I373c7d5c22de924fbc5d1db6967954173403c92e
---
gnu/packages/lean.scm | 38 --------------------------------------
1 file changed, 38 deletions(-)
diff --git a/gnu/packages/lean.scm b/gnu/packages/lean.scm
index 34c7f8a075..d1e74adb83 100644
--- a/gnu/packages/lean.scm
+++ b/gnu/packages/lean.scm
@@ -48,44 +48,6 @@
#:use-module (gnu packages python-web)
#:use-module (gnu packages python-xyz))
-(define-public lean
- (package
- (name "lean")
- (version "3.51.1")
- (home-page "https://lean-lang.org"; )
- (source (origin
- (method git-fetch)
- (uri (git-reference
- (url "https://github.com/leanprover-community/lean";)
- (commit (string-append "v" version))))
- (file-name (git-file-name name version))
- (sha256
- (base32
- "17g4d3lqnbl1yfy2pjannf73v8qhc5003d2jkmrqiy05zkqs8d9n"))))
- (build-system cmake-build-system)
- (inputs
- (list gmp))
- (arguments
- (list
- #:build-type "Release" ; default upstream build type
- ;; XXX: Test phases currently fail on 32-bit sytems.
- ;; Tests for those architectures have been temporarily
- ;; disabled, pending further investigation.
- #:tests? (and (not (%current-target-system))
- (let ((arch (%current-system)))
- (not (or (string-prefix? "i686" arch)
- (string-prefix? "armhf" arch)))))
- #:phases
- #~(modify-phases %standard-phases
- (add-before 'configure 'chdir-to-src
- (lambda _ (chdir "src"))))))
- (synopsis "Theorem prover and programming language")
- (description
- "Lean is a theorem prover and programming language with a small trusted
-core based on dependent typed theory, aiming to bridge the gap between
-interactive and automated theorem proving.")
- (license license:asl2.0)))
-
(define-public lean4
(package
(name "lean4")
