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