guix_mirror_bot pushed a commit to branch master
in repository guix.
commit 106a020473eca33e231cea04ebe76aa6bcbe3039
Author: Carlo Zancanaro <[email protected]>
AuthorDate: Fri Sep 4 23:11:57 2026 +1000
gnu: lean4: Add native search paths.
* gnu/packages/lean.scm (lean4): Add native search paths to match Lake's
output path.
Signed-off-by: Ludovic Courtès <[email protected]>
---
gnu/packages/lean.scm | 9 +++++++++
1 file changed, 9 insertions(+)
diff --git a/gnu/packages/lean.scm b/gnu/packages/lean.scm
index da40a1d2ea3..423555caa01 100644
--- a/gnu/packages/lean.scm
+++ b/gnu/packages/lean.scm
@@ -6,6 +6,7 @@
;;; Copyright © 2023 Zhu Zihao <[email protected]>
;;; Copyright © 2025 Luca Di Sera <[email protected]>
;;; Copyright © 2026 Lîm Tsú-thuàn <[email protected]>
+;;; Copyright © 2026 Carlo Zancanaro <[email protected]>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -145,6 +146,14 @@
(for-each delete-file-recursively
(find-files "../source/src/lake/tests" "^\\.git$"
#:directories? #t)))))))
+ (native-search-paths
+ ;; Lean packages are a full build tree for the package, which stores its
+ ;; build results in this directory. This fits with how Lake expects to
+ ;; find things, so it all works out. Hopefully upstream improves this
+ ;; over time: https://github.com/leanprover/lean4/issues/5122
+ (list (search-path-specification
+ (variable "LEAN_PATH")
+ (files (list ".lake/build/lib/lean")))))
(synopsis "Theorem prover and programming language")
(description
"Lean is a theorem prover and programming language with a small trusted
