Commit | Line | Data |
---|---|---|
ae482ce1 DC |
1 | ;;; GNU Guix --- Functional package management for GNU |
2 | ;;; Copyright © 2015 Paul van der Walt <paul@denknerd.org> | |
3 | ;;; Copyright © 2016, 2017 David Craven <david@craven.ch> | |
d661ed52 | 4 | ;;; Copyright © 2018 Alex ter Weele <alex.ter.weele@gmail.com> |
ae482ce1 DC |
5 | ;;; |
6 | ;;; This file is part of GNU Guix. | |
7 | ;;; | |
8 | ;;; GNU Guix is free software; you can redistribute it and/or modify it | |
9 | ;;; under the terms of the GNU General Public License as published by | |
10 | ;;; the Free Software Foundation; either version 3 of the License, or (at | |
11 | ;;; your option) any later version. | |
12 | ;;; | |
13 | ;;; GNU Guix is distributed in the hope that it will be useful, but | |
14 | ;;; WITHOUT ANY WARRANTY; without even the implied warranty of | |
15 | ;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
16 | ;;; GNU General Public License for more details. | |
17 | ;;; | |
18 | ;;; You should have received a copy of the GNU General Public License | |
19 | ;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>. | |
20 | ||
21 | (define-module (gnu packages idris) | |
22 | #:use-module (gnu packages haskell) | |
a06b9b50 | 23 | #:use-module (gnu packages haskell-check) |
44b7374a | 24 | #:use-module (gnu packages haskell-web) |
ae482ce1 DC |
25 | #:use-module (gnu packages multiprecision) |
26 | #:use-module (gnu packages ncurses) | |
ea3b38f1 | 27 | #:use-module (guix build-system gnu) |
ae482ce1 | 28 | #:use-module (guix build-system haskell) |
ae482ce1 DC |
29 | #:use-module (guix download) |
30 | #:use-module (guix git-download) | |
31 | #:use-module ((guix licenses) #:prefix license:) | |
32 | #:use-module (guix packages)) | |
33 | ||
9c7e17fd AW |
34 | (define ghc-aeson-1.1.2.0 |
35 | (package (inherit ghc-aeson) | |
36 | (version "1.1.2.0") | |
37 | (source | |
38 | (origin | |
39 | (method url-fetch) | |
40 | (uri (string-append | |
41 | "https://hackage.haskell.org/package/aeson/aeson-" | |
42 | version | |
43 | ".tar.gz")) | |
44 | (sha256 | |
45 | (base32 | |
46 | "1zy5z8pzvh53qkjm0nm3f4rwqfqg3867ck8ncd6mrxpcyvxqqj1p")))))) | |
47 | ||
78dc985b AW |
48 | (define ghc-trifecta-1.6.2.1 |
49 | (package (inherit ghc-trifecta) | |
50 | (version "1.6.2.1") | |
51 | (source | |
52 | (origin | |
53 | (method url-fetch) | |
54 | (uri (string-append | |
55 | "https://hackage.haskell.org/package/trifecta/" | |
56 | "trifecta-" version ".tar.gz")) | |
57 | (sha256 | |
58 | (base32 | |
59 | "1rgv62dlmm4vkdymx5rw5jg3w8ifpzg1745rvs1m4kzdx16p5cxs")))))) | |
60 | ||
866b1908 AW |
61 | ;; ghc-cheapskate appeared too new. This follows LTS Haskell. |
62 | (define ghc-cheapskate-0.1.0.5 | |
63 | (package | |
64 | (inherit ghc-cheapskate) | |
65 | (version "0.1.0.5") | |
66 | (source | |
67 | (origin | |
68 | (method url-fetch) | |
69 | (uri (string-append | |
70 | "https://hackage.haskell.org/package/cheapskate/cheapskate-" | |
71 | version | |
72 | ".tar.gz")) | |
73 | (sha256 | |
74 | (base32 | |
75 | "0cpsmfx5z2xykg71sv8j7pl8ga6pzyjnjdb9bxn00vcpqkzvfqvs")))) | |
76 | (arguments | |
77 | ;; LTS Haskell says data-default >=0.5 && <0.8 | |
78 | `(#:configure-flags (list "--allow-newer=data-default"))))) | |
79 | ||
ae482ce1 DC |
80 | (define-public idris |
81 | (package | |
82 | (name "idris") | |
b74f2247 | 83 | (version "1.0") |
ae482ce1 DC |
84 | (source (origin |
85 | (method url-fetch) | |
86 | (uri (string-append | |
87 | "https://hackage.haskell.org/package/" | |
88 | "idris-" version "/idris-" version ".tar.gz")) | |
89 | (sha256 | |
90 | (base32 | |
b74f2247 | 91 | "1srbz0cyvd0k1yqgbrwnfj94yg5y3z533q1kzac96z1h7v454s5h")))) |
ae482ce1 DC |
92 | (build-system haskell-build-system) |
93 | (inputs | |
94 | `(("gmp" ,gmp) | |
95 | ("ncurses" ,ncurses) | |
d661ed52 | 96 | ("ghc-aeson" ,ghc-aeson-1.1.2.0) |
ae482ce1 DC |
97 | ("ghc-annotated-wl-pprint" ,ghc-annotated-wl-pprint) |
98 | ("ghc-ansi-terminal" ,ghc-ansi-terminal) | |
99 | ("ghc-ansi-wl-pprint" ,ghc-ansi-wl-pprint) | |
d661ed52 | 100 | ("ghc-async" ,ghc-async) |
ae482ce1 DC |
101 | ("ghc-base64-bytestring" ,ghc-base64-bytestring) |
102 | ("ghc-blaze-html" ,ghc-blaze-html) | |
103 | ("ghc-blaze-markup" ,ghc-blaze-markup) | |
d661ed52 | 104 | ("ghc-cheapskate" ,ghc-cheapskate-0.1.0.5) |
c53af001 | 105 | ("ghc-code-page" ,ghc-code-page) |
ae482ce1 DC |
106 | ("ghc-fingertree" ,ghc-fingertree) |
107 | ("ghc-fsnotify" ,ghc-fsnotify) | |
108 | ("ghc-ieee754" ,ghc-ieee754) | |
109 | ("ghc-mtl" ,ghc-mtl) | |
110 | ("ghc-network" ,ghc-network) | |
111 | ("ghc-optparse-applicative" ,ghc-optparse-applicative) | |
ae482ce1 DC |
112 | ("ghc-regex-tdfa" ,ghc-regex-tdfa) |
113 | ("ghc-safe" ,ghc-safe) | |
114 | ("ghc-split" ,ghc-split) | |
ae482ce1 DC |
115 | ("ghc-terminal-size" ,ghc-terminal-size) |
116 | ("ghc-text" ,ghc-text) | |
d661ed52 | 117 | ("ghc-trifecta" ,ghc-trifecta-1.6.2.1) |
ae482ce1 DC |
118 | ("ghc-uniplate" ,ghc-uniplate) |
119 | ("ghc-unordered-containers" ,ghc-unordered-containers) | |
120 | ("ghc-utf8-string" ,ghc-utf8-string) | |
ae482ce1 | 121 | ("ghc-vector" ,ghc-vector) |
d661ed52 AW |
122 | ("ghc-vector-binary-instances" ,ghc-vector-binary-instances) |
123 | ("ghc-zip-archive" ,ghc-zip-archive))) | |
ae482ce1 DC |
124 | (arguments |
125 | `(#:tests? #f ; FIXME: Test suite doesn't run in a sandbox. | |
126 | #:configure-flags | |
127 | (list (string-append "--datasubdir=" | |
128 | (assoc-ref %outputs "out") "/lib/idris")) | |
129 | #:phases | |
130 | (modify-phases %standard-phases | |
131 | (add-before 'configure 'set-cc-command | |
132 | (lambda _ | |
133 | (setenv "CC" "gcc") | |
134 | #t)) | |
135 | (add-after 'install 'fix-libs-install-location | |
136 | (lambda* (#:key outputs #:allow-other-keys) | |
137 | (let* ((out (assoc-ref outputs "out")) | |
138 | (lib (string-append out "/lib/idris")) | |
139 | (modules (string-append lib "/libs"))) | |
140 | (for-each | |
141 | (lambda (module) | |
142 | (symlink (string-append modules "/" module) | |
143 | (string-append lib "/" module))) | |
144 | '("prelude" "base" "contrib" "effects" "pruviloj")))))))) | |
145 | (native-search-paths | |
146 | (list (search-path-specification | |
147 | (variable "IDRIS_LIBRARY_PATH") | |
148 | (files '("lib/idris"))))) | |
149 | (home-page "http://www.idris-lang.org") | |
150 | (synopsis "General purpose language with full dependent types") | |
151 | (description "Idris is a general purpose language with full dependent | |
152 | types. It is compiled, with eager evaluation. Dependent types allow types to | |
153 | be predicated on values, meaning that some aspects of a program's behaviour | |
154 | can be specified precisely in the type. The language is closely related to | |
155 | Epigram and Agda.") | |
156 | (license license:bsd-3))) | |
ea3b38f1 DC |
157 | |
158 | ;; Idris modules use the gnu-build-system so that the IDRIS_LIBRARY_PATH is set. | |
159 | (define (idris-default-arguments name) | |
160 | `(#:modules ((guix build gnu-build-system) | |
161 | (guix build utils) | |
162 | (ice-9 ftw) | |
163 | (ice-9 match)) | |
164 | #:phases | |
165 | (modify-phases %standard-phases | |
166 | (delete 'configure) | |
167 | (delete 'build) | |
168 | (delete 'check) | |
169 | (replace 'install | |
170 | (lambda* (#:key inputs outputs #:allow-other-keys) | |
171 | (let* ((out (assoc-ref outputs "out")) | |
172 | (idris (assoc-ref inputs "idris")) | |
173 | (idris-bin (string-append idris "/bin/idris")) | |
174 | (idris-libs (string-append idris "/lib/idris/libs")) | |
175 | (module-name (and (string-prefix? "idris-" ,name) | |
176 | (substring ,name 6))) | |
177 | (ibcsubdir (string-append out "/lib/idris/" module-name)) | |
178 | (ipkg (string-append module-name ".ipkg")) | |
179 | (idris-library-path (getenv "IDRIS_LIBRARY_PATH")) | |
180 | (idris-path (string-split idris-library-path #\:)) | |
181 | (idris-path-files (apply append | |
182 | (map (lambda (path) | |
183 | (map (lambda (dir) | |
184 | (string-append path "/" dir)) | |
185 | (scandir path))) idris-path))) | |
186 | (idris-path-subdirs (filter (lambda (path) | |
187 | (and path (match (stat:type (stat path)) | |
188 | ('directory #t) | |
189 | (_ #f)))) | |
190 | idris-path-files)) | |
191 | (install-cmd (cons* idris-bin | |
192 | "--ibcsubdir" ibcsubdir | |
178670c9 PM |
193 | "--build" ipkg |
194 | ;; only trigger a build, as --ibcsubdir | |
195 | ;; already installs .ibc files. | |
196 | ||
ea3b38f1 DC |
197 | (apply append (map (lambda (path) |
198 | (list "--idrispath" | |
199 | path)) | |
200 | idris-path-subdirs))))) | |
ea3b38f1 DC |
201 | ;; FIXME: Seems to be a bug in idris that causes a dubious failure. |
202 | (apply system* install-cmd) | |
203 | #t)))))) | |
204 | ||
205 | (define-public idris-lightyear | |
206 | (let ((commit "6d65ad111b4bed2bc131396f8385528fc6b3678a")) | |
207 | (package | |
208 | (name "idris-lightyear") | |
209 | (version (git-version "0.1" "1" commit)) | |
210 | (source (origin | |
211 | (method git-fetch) | |
212 | (uri (git-reference | |
213 | (url "https://github.com/ziman/lightyear") | |
214 | (commit commit))) | |
215 | (file-name (git-file-name name version)) | |
216 | (sha256 | |
217 | (base32 | |
218 | "1pkxnn3ryr0v0cin4nasw7kgkc9dnnpja1nfbj466mf3qv5s98af")))) | |
219 | (build-system gnu-build-system) | |
220 | (native-inputs | |
221 | `(("idris" ,idris))) | |
222 | (arguments (idris-default-arguments name)) | |
223 | (home-page "https://github.com/ziman/lightyear") | |
224 | (synopsis "Lightweight parser combinator library for Idris") | |
225 | (description "Lightweight parser combinator library for Idris, inspired | |
226 | by Parsec. This package is used (almost) the same way as Parsec, except for one | |
227 | difference: backtracking.") | |
228 | (license license:bsd-2)))) | |
4e17fff3 DC |
229 | |
230 | (define-public idris-wl-pprint | |
231 | (let ((commit "1d365fcf4ba075859844dbc5eb96a90f57b9f338")) | |
232 | (package | |
233 | (name "idris-wl-pprint") | |
234 | (version (git-version "0.1" "1" commit)) | |
235 | (source (origin | |
236 | (method git-fetch) | |
237 | (uri (git-reference | |
238 | (url "https://github.com/shayan-najd/wl-pprint") | |
239 | (commit commit))) | |
240 | (file-name (git-file-name name version)) | |
241 | (sha256 | |
242 | (base32 | |
243 | "0g7c3y9smifdz4sivi3qmvymhdr7v9kfq45fmfmmvkqcrix0spzn")))) | |
244 | (build-system gnu-build-system) | |
245 | (native-inputs | |
246 | `(("idris" ,idris))) | |
247 | (arguments (idris-default-arguments name)) | |
248 | (home-page "https://github.com/shayan-najd/wl-pprint") | |
249 | (synopsis "Pretty printing library") | |
250 | (description "A pretty printing library for Idris based on Phil Wadler's | |
251 | paper A Prettier Printer and on Daan Leijen's extensions in the Haskell | |
252 | wl-pprint library.") | |
253 | (license license:bsd-2)))) | |
5a16d828 DC |
254 | |
255 | (define-public idris-bifunctors | |
256 | (let ((commit "53d06a6ccfe70c49c9ae8c8a4135981dd2173202")) | |
257 | (package | |
258 | (name "idris-bifunctors") | |
259 | (version (git-version "0.1" "1" commit)) | |
260 | (source (origin | |
261 | (method git-fetch) | |
262 | (uri (git-reference | |
263 | (url "https://github.com/HuwCampbell/Idris-Bifunctors") | |
264 | (commit commit))) | |
265 | (file-name (string-append name "-" version "-checkout")) | |
266 | (sha256 | |
267 | (base32 | |
268 | "02vbsd3rmgnj0l1qq787709qcxjbr9890cbad4ykn27f77jk81h4")))) | |
269 | (build-system gnu-build-system) | |
270 | (native-inputs | |
271 | `(("idris" ,idris))) | |
272 | (arguments (idris-default-arguments name)) | |
273 | (home-page "https://github.com/HuwCampbell/Idris-Bifunctors") | |
274 | (synopsis "Bifunctor library") | |
275 | (description "This is a bifunctor library for Idris based off the | |
276 | excellent Haskell Bifunctors package from Edward Kmett.") | |
277 | (license license:bsd-3)))) | |
3254e1ab DC |
278 | |
279 | (define-public idris-lens | |
280 | (let ((commit "26f012005f6849806cea630afe317e42cae97f29")) | |
281 | (package | |
282 | (name "idris-lens") | |
283 | (version (git-version "0.1" "1" commit)) | |
284 | (source (origin | |
285 | (method git-fetch) | |
286 | (uri (git-reference | |
287 | (url "https://github.com/HuwCampbell/idris-lens") | |
288 | (commit commit))) | |
289 | (file-name (git-file-name name version)) | |
290 | (sha256 | |
291 | (base32 | |
292 | "06jzfj6rad08rk92w8jk5byi79svmyg0mrcqhibgx8rkjjy6vmai")))) | |
293 | (build-system gnu-build-system) | |
294 | (native-inputs | |
295 | `(("idris" ,idris))) | |
296 | (propagated-inputs | |
297 | `(("idris-bifunctors" ,idris-bifunctors))) | |
298 | (arguments (idris-default-arguments name)) | |
299 | (home-page "https://github.com/HuwCampbell/idris-lens") | |
300 | (synopsis "Van Laarhoven lenses for Idris") | |
301 | (description "Lenses are composable functional references. They allow | |
302 | accessing and modifying data within a structure.") | |
303 | (license license:bsd-3)))) |