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