summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndreas Enge <andreas@enge.fr>2026-03-09 11:12:47 +0100
committerAndreas Enge <andreas@enge.fr>2026-03-09 11:12:50 +0100
commit404a14f879a63898eb379018dfbb39d4c3e0e9d8 (patch)
tree71eaa484deab5c3a48166a83d5fa68e2d15c8c56
parent5bff31a54788de12c20f4e8c6f74f0de33c7c20e (diff)
gnu: Remove lean.
* gnu/packages/lean.scm (lean): Delete variable. Fixes: guix/guix#6239 Change-Id: I373c7d5c22de924fbc5d1db6967954173403c92e
-rw-r--r--gnu/packages/lean.scm38
1 files changed, 0 insertions, 38 deletions
diff --git a/gnu/packages/lean.scm b/gnu/packages/lean.scm
index 34c7f8a075f..d1e74adb837 100644
--- a/gnu/packages/lean.scm
+++ b/gnu/packages/lean.scm
@@ -48,44 +48,6 @@
48 #:use-module (gnu packages python-web) 48 #:use-module (gnu packages python-web)
49 #:use-module (gnu packages python-xyz)) 49 #:use-module (gnu packages python-xyz))
50 50
51(define-public lean
52 (package
53 (name "lean")
54 (version "3.51.1")
55 (home-page "https://lean-lang.org" )
56 (source (origin
57 (method git-fetch)
58 (uri (git-reference
59 (url "https://github.com/leanprover-community/lean")
60 (commit (string-append "v" version))))
61 (file-name (git-file-name name version))
62 (sha256
63 (base32
64 "17g4d3lqnbl1yfy2pjannf73v8qhc5003d2jkmrqiy05zkqs8d9n"))))
65 (build-system cmake-build-system)
66 (inputs
67 (list gmp))
68 (arguments
69 (list
70 #:build-type "Release" ; default upstream build type
71 ;; XXX: Test phases currently fail on 32-bit sytems.
72 ;; Tests for those architectures have been temporarily
73 ;; disabled, pending further investigation.
74 #:tests? (and (not (%current-target-system))
75 (let ((arch (%current-system)))
76 (not (or (string-prefix? "i686" arch)
77 (string-prefix? "armhf" arch)))))
78 #:phases
79 #~(modify-phases %standard-phases
80 (add-before 'configure 'chdir-to-src
81 (lambda _ (chdir "src"))))))
82 (synopsis "Theorem prover and programming language")
83 (description
84 "Lean is a theorem prover and programming language with a small trusted
85core based on dependent typed theory, aiming to bridge the gap between
86interactive and automated theorem proving.")
87 (license license:asl2.0)))
88
89(define-public lean4 51(define-public lean4
90 (package 52 (package
91 (name "lean4") 53 (name "lean4")