blob: 49836d5dea063f1386895577e6bf5528004e35fc (
plain)
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
124
125
126
127
128
|
;;; 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 agda-build-system)
#:use-module ((guix build gnu-build-system) #:prefix gnu:)
#:use-module (guix build utils)
#:use-module (srfi srfi-26)
#:use-module (srfi srfi-34)
#:use-module (srfi srfi-35)
#:use-module (ice-9 ftw)
#:use-module (ice-9 match)
#:export (%standard-phases
agda-build))
(define* (set-locpath #:key inputs native-inputs #:allow-other-keys)
(let ((locales (assoc-ref (or native-inputs inputs) "locales")))
(setenv "GUIX_LOCPATH" (string-append locales "/lib/locale"))))
(define %agda-possible-extensions
(cons
".agda"
(map (cute string-append ".lagda" <>)
'(""
".md"
".org"
".rst"
".tex"))))
(define (pattern-predicate pattern)
(define compiled-rx (make-regexp pattern))
(lambda (file stat)
(regexp-exec compiled-rx file)))
(define* (build #:key plan #:allow-other-keys)
(for-each
(match-lambda
((pattern . options)
(for-each
(lambda (file)
(apply invoke (cons* "agda" file options)))
(let ((files (find-files "." (pattern-predicate pattern))))
(if (null? files)
(raise
(make-compound-condition
(condition
(&message
(message (format #f "Plan pattern `~a' did not match any files"
pattern))))
(condition
(&error))))
files))))
(x
(raise
(make-compound-condition
(condition
(&message
(message (format #f "Malformed plan element `~a'" x))))
(condition
(&error))))))
plan))
(define* (install #:key outputs name extra-files #:allow-other-keys)
(define libdir (string-append (assoc-ref outputs "out") "/lib/agda/" name))
(define agda-version
(car (scandir "./_build/"
(lambda (entry)
(not (member entry '("." "..")))))))
(define agdai-files
(with-directory-excursion
(string-join (list "." "_build" agda-version "agda") "/")
(find-files ".")))
(define (install-source agdai)
(define dir (dirname agdai))
;; Drop .agdai
(define no-ext (string-drop-right agdai 6))
(define source
(match (filter file-exists? (map (cute string-append no-ext <>)
%agda-possible-extensions))
((single) single)
(res (raise
(make-compound-condition
(condition
(&message
(message
(format #f
"Cannot find unique source file for agdai file `~a`, got `~a`"
agdai res))))
(condition
(&error)))))))
(install-file source (string-append libdir "/" dir)))
(for-each install-source agdai-files)
(copy-recursively "_build" (string-append libdir "/_build"))
(for-each
(lambda (pattern)
(for-each
(lambda (file)
(install-file file libdir))
(find-files "." (pattern-predicate pattern))))
extra-files))
(define %standard-phases
(modify-phases gnu:%standard-phases
(add-before 'install-locale 'set-locpath set-locpath)
(delete 'bootstrap)
(delete 'configure)
(replace 'build build)
(delete 'check) ;; No universal checker
(replace 'install install)))
(define* (agda-build #:key inputs (phases %standard-phases)
#:allow-other-keys #:rest args)
"Build the given Agda package, applying all of PHASES in order."
(apply gnu:gnu-build #:inputs inputs #:phases phases args))
|