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> |
c67ff563 | 5 | ;;; Copyright © 2019, 2021 Eric Bavier <bavier@posteo.net> |
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") | |
c67ff563 | 41 | (version "1.3.3") |
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 | |
c67ff563 EB |
49 | "1pachwc6msw3n1mz2z1r1w6h518w9gbhdvbaa5vi1qp3cn3wm6q4")) |
50 | (patches (search-patches "idris-disable-test.patch")))) | |
ae482ce1 | 51 | (build-system haskell-build-system) |
89647ff1 EB |
52 | (native-inputs ;For tests |
53 | `(("perl" ,perl) | |
c67ff563 | 54 | ("ghc-cheapskate" ,ghc-cheapskate) |
89647ff1 EB |
55 | ("ghc-tasty" ,ghc-tasty) |
56 | ("ghc-tasty-golden" ,ghc-tasty-golden) | |
57 | ("ghc-tasty-rerun" ,ghc-tasty-rerun))) | |
ae482ce1 DC |
58 | (inputs |
59 | `(("gmp" ,gmp) | |
60 | ("ncurses" ,ncurses) | |
53812aa7 | 61 | ("ghc-aeson" ,ghc-aeson) |
ae482ce1 DC |
62 | ("ghc-annotated-wl-pprint" ,ghc-annotated-wl-pprint) |
63 | ("ghc-ansi-terminal" ,ghc-ansi-terminal) | |
64 | ("ghc-ansi-wl-pprint" ,ghc-ansi-wl-pprint) | |
d661ed52 | 65 | ("ghc-async" ,ghc-async) |
ae482ce1 DC |
66 | ("ghc-base64-bytestring" ,ghc-base64-bytestring) |
67 | ("ghc-blaze-html" ,ghc-blaze-html) | |
68 | ("ghc-blaze-markup" ,ghc-blaze-markup) | |
53812aa7 | 69 | ("ghc-cheapskate" ,ghc-cheapskate) |
c53af001 | 70 | ("ghc-code-page" ,ghc-code-page) |
ae482ce1 DC |
71 | ("ghc-fingertree" ,ghc-fingertree) |
72 | ("ghc-fsnotify" ,ghc-fsnotify) | |
73 | ("ghc-ieee754" ,ghc-ieee754) | |
e16bc710 | 74 | ("ghc-libffi" ,ghc-libffi) |
03b0c92e | 75 | ("ghc-megaparsec" ,ghc-megaparsec) |
d4473202 | 76 | ("ghc-network" ,ghc-network) |
ae482ce1 | 77 | ("ghc-optparse-applicative" ,ghc-optparse-applicative) |
ae482ce1 DC |
78 | ("ghc-regex-tdfa" ,ghc-regex-tdfa) |
79 | ("ghc-safe" ,ghc-safe) | |
80 | ("ghc-split" ,ghc-split) | |
ae482ce1 | 81 | ("ghc-terminal-size" ,ghc-terminal-size) |
ae482ce1 DC |
82 | ("ghc-uniplate" ,ghc-uniplate) |
83 | ("ghc-unordered-containers" ,ghc-unordered-containers) | |
84 | ("ghc-utf8-string" ,ghc-utf8-string) | |
ae482ce1 | 85 | ("ghc-vector" ,ghc-vector) |
d661ed52 AW |
86 | ("ghc-vector-binary-instances" ,ghc-vector-binary-instances) |
87 | ("ghc-zip-archive" ,ghc-zip-archive))) | |
ae482ce1 | 88 | (arguments |
89647ff1 | 89 | `(#:configure-flags |
ae482ce1 | 90 | (list (string-append "--datasubdir=" |
e16bc710 EB |
91 | (assoc-ref %outputs "out") "/lib/idris") |
92 | "-fFFI" "-fGMP") | |
ae482ce1 DC |
93 | #:phases |
94 | (modify-phases %standard-phases | |
5aaa1995 TS |
95 | ;; This allows us to call the 'idris' binary before installing. |
96 | (add-after 'unpack 'set-ld-library-path | |
97 | (lambda _ | |
98 | (setenv "LD_LIBRARY_PATH" (string-append (getcwd) "/dist/build")) | |
99 | #t)) | |
3594b669 TS |
100 | (add-after 'unpack 'update-constraints |
101 | (lambda _ | |
102 | (substitute* "idris.cabal" | |
c67ff563 EB |
103 | (("ansi-terminal < 0\\.9") "ansi-terminal < 0.10") |
104 | (("cheapskate >= 0\\.1\\.1\\.2 && < 0\\.2") "cheapskate >= 0.1.1.1 && < 0.2")) | |
3594b669 | 105 | #t)) |
ae482ce1 DC |
106 | (add-before 'configure 'set-cc-command |
107 | (lambda _ | |
108 | (setenv "CC" "gcc") | |
109 | #t)) | |
110 | (add-after 'install 'fix-libs-install-location | |
111 | (lambda* (#:key outputs #:allow-other-keys) | |
112 | (let* ((out (assoc-ref outputs "out")) | |
113 | (lib (string-append out "/lib/idris")) | |
114 | (modules (string-append lib "/libs"))) | |
115 | (for-each | |
116 | (lambda (module) | |
117 | (symlink (string-append modules "/" module) | |
118 | (string-append lib "/" module))) | |
89647ff1 EB |
119 | '("prelude" "base" "contrib" "effects" "pruviloj"))))) |
120 | (delete 'check) ;Run check later | |
121 | (add-after 'install 'check | |
122 | (lambda* (#:key outputs #:allow-other-keys #:rest args) | |
123 | (let ((out (assoc-ref outputs "out"))) | |
c67ff563 | 124 | (chmod "test/scripts/timeout" #o755) ;must be executable |
89647ff1 EB |
125 | (setenv "TASTY_NUM_THREADS" (number->string (parallel-job-count))) |
126 | (setenv "IDRIS_CC" "gcc") ;Needed for creating executables | |
127 | (setenv "PATH" (string-append out "/bin:" (getenv "PATH"))) | |
5aaa1995 TS |
128 | (apply (assoc-ref %standard-phases 'check) args)))) |
129 | (add-before 'check 'restore-libidris_rts | |
130 | (lambda* (#:key outputs #:allow-other-keys) | |
131 | ;; The Haskell build system moves this library to the | |
132 | ;; "static" output. Idris only knows how to find it in the | |
133 | ;; "out" output, so we restore it here. | |
134 | (let ((out (assoc-ref outputs "out")) | |
135 | (static (assoc-ref outputs "static")) | |
136 | (filename "/lib/idris/rts/libidris_rts.a")) | |
137 | (rename-file (string-append static filename) | |
138 | (string-append out filename)) | |
139 | #t)))))) | |
ae482ce1 DC |
140 | (native-search-paths |
141 | (list (search-path-specification | |
142 | (variable "IDRIS_LIBRARY_PATH") | |
143 | (files '("lib/idris"))))) | |
17dea2e2 | 144 | (home-page "https://www.idris-lang.org") |
ae482ce1 DC |
145 | (synopsis "General purpose language with full dependent types") |
146 | (description "Idris is a general purpose language with full dependent | |
147 | types. It is compiled, with eager evaluation. Dependent types allow types to | |
148 | be predicated on values, meaning that some aspects of a program's behaviour | |
149 | can be specified precisely in the type. The language is closely related to | |
150 | Epigram and Agda.") | |
151 | (license license:bsd-3))) | |
ea3b38f1 DC |
152 | |
153 | ;; Idris modules use the gnu-build-system so that the IDRIS_LIBRARY_PATH is set. | |
154 | (define (idris-default-arguments name) | |
155 | `(#:modules ((guix build gnu-build-system) | |
156 | (guix build utils) | |
157 | (ice-9 ftw) | |
158 | (ice-9 match)) | |
159 | #:phases | |
160 | (modify-phases %standard-phases | |
161 | (delete 'configure) | |
162 | (delete 'build) | |
163 | (delete 'check) | |
164 | (replace 'install | |
165 | (lambda* (#:key inputs outputs #:allow-other-keys) | |
166 | (let* ((out (assoc-ref outputs "out")) | |
167 | (idris (assoc-ref inputs "idris")) | |
168 | (idris-bin (string-append idris "/bin/idris")) | |
169 | (idris-libs (string-append idris "/lib/idris/libs")) | |
170 | (module-name (and (string-prefix? "idris-" ,name) | |
171 | (substring ,name 6))) | |
172 | (ibcsubdir (string-append out "/lib/idris/" module-name)) | |
173 | (ipkg (string-append module-name ".ipkg")) | |
174 | (idris-library-path (getenv "IDRIS_LIBRARY_PATH")) | |
175 | (idris-path (string-split idris-library-path #\:)) | |
176 | (idris-path-files (apply append | |
177 | (map (lambda (path) | |
178 | (map (lambda (dir) | |
179 | (string-append path "/" dir)) | |
180 | (scandir path))) idris-path))) | |
181 | (idris-path-subdirs (filter (lambda (path) | |
182 | (and path (match (stat:type (stat path)) | |
183 | ('directory #t) | |
184 | (_ #f)))) | |
185 | idris-path-files)) | |
186 | (install-cmd (cons* idris-bin | |
187 | "--ibcsubdir" ibcsubdir | |
178670c9 PM |
188 | "--build" ipkg |
189 | ;; only trigger a build, as --ibcsubdir | |
190 | ;; already installs .ibc files. | |
191 | ||
ea3b38f1 DC |
192 | (apply append (map (lambda (path) |
193 | (list "--idrispath" | |
194 | path)) | |
195 | idris-path-subdirs))))) | |
ea3b38f1 DC |
196 | ;; FIXME: Seems to be a bug in idris that causes a dubious failure. |
197 | (apply system* install-cmd) | |
198 | #t)))))) | |
199 | ||
200 | (define-public idris-lightyear | |
201 | (let ((commit "6d65ad111b4bed2bc131396f8385528fc6b3678a")) | |
202 | (package | |
203 | (name "idris-lightyear") | |
204 | (version (git-version "0.1" "1" commit)) | |
205 | (source (origin | |
206 | (method git-fetch) | |
207 | (uri (git-reference | |
208 | (url "https://github.com/ziman/lightyear") | |
209 | (commit commit))) | |
210 | (file-name (git-file-name name version)) | |
211 | (sha256 | |
212 | (base32 | |
213 | "1pkxnn3ryr0v0cin4nasw7kgkc9dnnpja1nfbj466mf3qv5s98af")))) | |
214 | (build-system gnu-build-system) | |
215 | (native-inputs | |
216 | `(("idris" ,idris))) | |
217 | (arguments (idris-default-arguments name)) | |
218 | (home-page "https://github.com/ziman/lightyear") | |
219 | (synopsis "Lightweight parser combinator library for Idris") | |
220 | (description "Lightweight parser combinator library for Idris, inspired | |
221 | by Parsec. This package is used (almost) the same way as Parsec, except for one | |
222 | difference: backtracking.") | |
223 | (license license:bsd-2)))) | |
4e17fff3 DC |
224 | |
225 | (define-public idris-wl-pprint | |
226 | (let ((commit "1d365fcf4ba075859844dbc5eb96a90f57b9f338")) | |
227 | (package | |
228 | (name "idris-wl-pprint") | |
229 | (version (git-version "0.1" "1" commit)) | |
230 | (source (origin | |
231 | (method git-fetch) | |
232 | (uri (git-reference | |
233 | (url "https://github.com/shayan-najd/wl-pprint") | |
234 | (commit commit))) | |
235 | (file-name (git-file-name name version)) | |
236 | (sha256 | |
237 | (base32 | |
238 | "0g7c3y9smifdz4sivi3qmvymhdr7v9kfq45fmfmmvkqcrix0spzn")))) | |
239 | (build-system gnu-build-system) | |
240 | (native-inputs | |
241 | `(("idris" ,idris))) | |
242 | (arguments (idris-default-arguments name)) | |
243 | (home-page "https://github.com/shayan-najd/wl-pprint") | |
244 | (synopsis "Pretty printing library") | |
245 | (description "A pretty printing library for Idris based on Phil Wadler's | |
246 | paper A Prettier Printer and on Daan Leijen's extensions in the Haskell | |
247 | wl-pprint library.") | |
248 | (license license:bsd-2)))) | |
5a16d828 DC |
249 | |
250 | (define-public idris-bifunctors | |
251 | (let ((commit "53d06a6ccfe70c49c9ae8c8a4135981dd2173202")) | |
252 | (package | |
253 | (name "idris-bifunctors") | |
254 | (version (git-version "0.1" "1" commit)) | |
255 | (source (origin | |
256 | (method git-fetch) | |
257 | (uri (git-reference | |
258 | (url "https://github.com/HuwCampbell/Idris-Bifunctors") | |
259 | (commit commit))) | |
260 | (file-name (string-append name "-" version "-checkout")) | |
261 | (sha256 | |
262 | (base32 | |
263 | "02vbsd3rmgnj0l1qq787709qcxjbr9890cbad4ykn27f77jk81h4")))) | |
264 | (build-system gnu-build-system) | |
265 | (native-inputs | |
266 | `(("idris" ,idris))) | |
267 | (arguments (idris-default-arguments name)) | |
268 | (home-page "https://github.com/HuwCampbell/Idris-Bifunctors") | |
269 | (synopsis "Bifunctor library") | |
270 | (description "This is a bifunctor library for Idris based off the | |
271 | excellent Haskell Bifunctors package from Edward Kmett.") | |
272 | (license license:bsd-3)))) | |
3254e1ab DC |
273 | |
274 | (define-public idris-lens | |
275 | (let ((commit "26f012005f6849806cea630afe317e42cae97f29")) | |
276 | (package | |
277 | (name "idris-lens") | |
278 | (version (git-version "0.1" "1" commit)) | |
279 | (source (origin | |
280 | (method git-fetch) | |
281 | (uri (git-reference | |
282 | (url "https://github.com/HuwCampbell/idris-lens") | |
283 | (commit commit))) | |
284 | (file-name (git-file-name name version)) | |
285 | (sha256 | |
286 | (base32 | |
287 | "06jzfj6rad08rk92w8jk5byi79svmyg0mrcqhibgx8rkjjy6vmai")))) | |
288 | (build-system gnu-build-system) | |
289 | (native-inputs | |
290 | `(("idris" ,idris))) | |
291 | (propagated-inputs | |
292 | `(("idris-bifunctors" ,idris-bifunctors))) | |
293 | (arguments (idris-default-arguments name)) | |
294 | (home-page "https://github.com/HuwCampbell/idris-lens") | |
295 | (synopsis "Van Laarhoven lenses for Idris") | |
296 | (description "Lenses are composable functional references. They allow | |
297 | accessing and modifying data within a structure.") | |
298 | (license license:bsd-3)))) |