1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
| | ;;; GNU Guix --- Functional package management for GNU
;;; Copyright © 2024 Antero Mejr <mail@antr.me>
;;;
;;; This file is part of GNU Guix.
;;;
;;; GNU Guix is free software; you can redistribute it and/or modify it
;;; under the terms of the GNU General Public License as published by
;;; the Free Software Foundation; either version 3 of the License, or (at
;;; your option) any later version.
;;;
;;; GNU Guix is distributed in the hope that it will be useful, but
;;; WITHOUT ANY WARRANTY; without even the implied warranty of
;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
;;; GNU General Public License for more details.
;;;
;;; You should have received a copy of the GNU General Public License
;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>.
(define-module (guix build lean-build-system)
#:use-module ((guix build gnu-build-system) #:prefix gnu:)
#:use-module (guix build utils)
#:use-module (ice-9 match)
#:use-module (ice-9 ftw)
#:use-module (ice-9 format)
#:use-module (srfi srfi-1)
#:use-module (srfi srfi-26)
#:export (%standard-phases
add-installed-lean-path
lean-build))
(define (lean-version lean)
(let* ((version (last (string-split lean #\-)))
(components (string-split version #\.))
(major+minor (take components 2)))
(string-join major+minor ".")))
(define (lib-dir inputs outputs)
"Return the path of the current output's Lean package directory."
(let ((out (assoc-ref outputs "out"))
(lean (assoc-ref inputs "lean")))
(string-append out "/lib/lean" (lean-version lean) "/packages")))
(define (add-installed-lean-path inputs outputs)
"Prepend the site-package of OUTPUT to LEAN_PATH. This is useful when
running checks after installing the package."
(let ((path-env (getenv "LEAN_PATH")))
(if path-env
(setenv "LEAN_PATH" (string-append (lib-dir inputs outputs) ":"
path-env))
(setenv "LEAH_PATH" (string-append (lib-dir inputs outputs))))))
(define* (build #:key lean-lake-targets #:allow-other-keys)
"Build a given Lean 4 package."
(let ((call (cons* "lake" "build" lean-lake-targets)))
(format #t "running: ~s\n" call)
(apply invoke call)))
(define* (check #:key tests? #:allow-other-keys)
"Run all the tests"
(when tests?
(let ((call '("lake" "test")))
(format #t "running: ~s\n" call)
(apply invoke call))))
(define* (install #:key inputs outputs #:allow-other-keys)
"Install a given Lean 4 package."
(let ((out (lib-dir inputs outputs)))
(format #t "installing Lean library to: ~s\n" out)
(copy-recursively ".lake/build/lib" out)))
(define* (wrap #:key inputs outputs #:allow-other-keys)
(define (list-of-files dir)
(find-files dir (lambda (file stat)
(and (eq? 'regular (stat:type stat))
(not (wrapped-program? file))))))
(define bindirs
(append-map (match-lambda
((_ . dir)
(list (string-append dir "/bin")
(string-append dir "/sbin"))))
outputs))
;; Do not require "bash" to be present in the package inputs
;; even when there is nothing to wrap.
;; Also, calculate (sh) only once to prevent some I/O.
(define %sh (delay (search-input-file inputs "bin/bash")))
(define (sh) (force %sh))
(let* ((var `("LEAN_PATH" prefix
,(search-path-as-string->list
(or (getenv "LEAN_PATH") "")))))
(for-each (lambda (dir)
(let ((files (list-of-files dir)))
(for-each (cut wrap-program <> #:sh (sh) var)
files)))
bindirs)))
(define* (add-install-to-lean-path #:key inputs outputs #:allow-other-keys)
"A phase that just wraps the 'add-installed-lean-path' procedure."
(add-installed-lean-path inputs outputs))
(define %standard-phases
(modify-phases gnu:%standard-phases
(delete 'bootstrap)
(delete 'configure)
(replace 'build build)
(replace 'check check)
(replace 'install install)
(add-after 'install 'add-install-to-lean-path add-install-to-lean-path)
(add-after 'add-install-to-lean-path 'wrap wrap)))
(define* (lean-build #:key inputs (phases %standard-phases)
#:allow-other-keys #:rest args)
"Build the given Lean package, applying all of PHASES in order."
(apply gnu:gnu-build #:inputs inputs #:phases phases args))
|