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
| | (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)
,@%gnu-build-system-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)))
|