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
117
118
119
120
121
122
123
| | ;;; GNU Guix --- Functional package management for GNU
;;; Copyright © 2023 Josselin Poiret <dev@jpoiret.xyz>
;;;
;;; 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-system agda)
#:use-module (guix build-system)
#:use-module (guix build-system gnu)
#:use-module (guix build-system haskell)
#:use-module (guix gexp)
#:use-module (guix monads)
#:use-module (guix packages)
#:use-module (guix search-paths)
#:use-module (guix store)
#:use-module (guix utils)
#:export (default-agda
%agda-build-system-modules
agda-build-system))
(define (default-agda)
;; Lazily resolve the binding to avoid a circular dependency.
(let ((agda (resolve-interface '(gnu packages agda))))
(module-ref agda 'agda)))
(define %agda-build-system-modules
`((guix build agda-build-system)
,@%default-gnu-imported-modules))
(define %default-modules
'((guix build agda-build-system)
(guix build utils)))
(define* (lower name
#:key source inputs native-inputs outputs system target
(agda (default-agda))
gnu-and-haskell?
#:allow-other-keys
#:rest arguments)
"Return a bag for NAME."
(define private-keywords
'(#:target #:agda #:gnu-and-haskell? #:inputs #:native-inputs))
;; TODO: cross-compilation support
(and (not target)
(bag
(name name)
(system system)
(host-inputs `(,@(if source
`(("source" ,source))
'())
,@inputs))
(build-inputs `(("agda" ,agda)
,@(if gnu-and-haskell?
(cons*
(list "ghc" (default-haskell))
(standard-packages))
'())
,(assoc "locales" (standard-packages))
,@native-inputs))
(outputs outputs)
(build agda-build)
(arguments (strip-keyword-arguments private-keywords arguments)))))
(define* (agda-build name inputs
#:key
source
(phases '%standard-phases)
(outputs '("out"))
(search-paths '())
(unpack-path "")
(build-flags ''())
(tests? #t)
(system (%current-system))
(guile #f)
plan
(extra-files '("^\\./.*\\.agda-lib$"))
(imported-modules %agda-build-system-modules)
(modules %default-modules))
(define builder
(with-imported-modules imported-modules
#~(begin
(use-modules #$@(sexp->gexp modules))
(agda-build #:name #$name
#:source #+source
#:system #$system
#:phases #$phases
#:outputs #$(outputs->gexp outputs)
#:search-paths '#$(sexp->gexp
(map search-path-specification->sexp
search-paths))
#:unpack-path #$unpack-path
#:build-flags #$build-flags
#:tests? #$tests?
#:inputs #$(input-tuples->gexp inputs)
#:plan '#$plan
#:extra-files '#$extra-files))))
(mlet %store-monad ((guile (package->derivation (or guile (default-guile))
system #:graft? #f)))
(gexp->derivation name builder
#:system system
#:guile-for-build guile)))
(define agda-build-system
(build-system
(name 'agda)
(description
"Build system for Agda libraries")
(lower lower)))
|