guix_mirror_bot pushed a commit to branch master
in repository guix.
commit 9c9b0244ba3656177391b0ff6243ba4afc1ad125
Author: Carlo Zancanaro <[email protected]>
AuthorDate: Mon Sep 7 20:03:53 2026 +1000
gnu: Add lean4-batteries.
* gnu/packages/lean.scm (lean4-batteries): New variable.
Signed-off-by: Ludovic Courtès <[email protected]>
Modified-by: Ludovic Courtès <[email protected]>
---
gnu/packages/lean.scm | 41 +++++++++++++++++++++++++++++++++++++++++
1 file changed, 41 insertions(+)
diff --git a/gnu/packages/lean.scm b/gnu/packages/lean.scm
index a0b5d65e0be..b0a4b390f0e 100644
--- a/gnu/packages/lean.scm
+++ b/gnu/packages/lean.scm
@@ -33,6 +33,7 @@
#:use-module (gnu packages maths)
#:use-module (gnu packages multiprecision)
#:use-module (guix build-system cmake)
+ #:use-module (guix build-system gnu)
#:use-module (guix build-system pyproject)
#:use-module ((guix licenses) #:prefix license:)
#:use-module (guix gexp)
@@ -192,6 +193,46 @@ find the dependencies of PACKAGE."
find the dependencies of the current package."
(make-package-overrides.json this-package))
+(define-public lean4-batteries
+ (package
+ (name "lean4-batteries")
+ (version (package-version lean4))
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/leanprover-community/batteries";)
+ (commit (string-append "v" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "013bh6anafhwgq8mav7yswqy7ym86gwvf5m6h39s45dnd25h6hmh"))))
+ (build-system gnu-build-system)
+ (arguments
+ (list
+ #:phases
+ #~(modify-phases %standard-phases
+ (delete 'configure)
+ (replace 'build
+ (lambda _
+ (setenv "CC" "gcc")
+ (invoke "lake" "build" "--packages"
+ #$(package-overrides.json) "Batteries:static")))
+ (delete 'check)
+ (replace 'install
+ (lambda _
+ (copy-recursively "."
+ #$output))))))
+ (native-inputs (list lean4))
+ (home-page "https://github.com/leanprover-community/batteries";)
+ (synopsis
+ "Collection of maths/computer science data structures and tactics")
+ (description
+ "Batteries is the the \"batteries included\" extended library for Lean 4.
+This is a collection of data structures and tactics intended for use by both
+computer-science applications and mathematics applications of Lean 4.")
+ (license license:asl2.0)
+ (properties '((lean-package-name . "batteries")))))
+
(define-public python-mathlibtools
(package
(name "python-mathlibtools")
