[jackhill/guix/guix.git] / gnu / packages / idris.scm

;;; GNU Guix --- Functional package management for GNU
;;; Copyright © 2015 Paul van der Walt <paul@denknerd.org>
;;; Copyright © 2016, 2017 David Craven <david@craven.ch>
;;; Copyright © 2018 Alex ter Weele <alex.ter.weele@gmail.com>
;;;
;;; 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 (gnu packages idris)
  #:use-module (gnu packages haskell)
  #:use-module (gnu packages haskell-check)
  #:use-module (gnu packages haskell-web)
  #:use-module (gnu packages multiprecision)
  #:use-module (gnu packages ncurses)
  #:use-module (guix build-system gnu)
  #:use-module (guix build-system haskell)
  #:use-module (guix download)
  #:use-module (guix git-download)
  #:use-module ((guix licenses) #:prefix license:)
  #:use-module (guix packages))

(define ghc-aeson-1.1.2.0
  (package (inherit ghc-aeson)
    (version "1.1.2.0")
    (source
     (origin
       (method url-fetch)
       (uri (string-append
             "https://hackage.haskell.org/package/aeson/aeson-"
             version
             ".tar.gz"))
       (sha256
        (base32
         "1zy5z8pzvh53qkjm0nm3f4rwqfqg3867ck8ncd6mrxpcyvxqqj1p"))))))

(define ghc-trifecta-1.6.2.1
  (package (inherit ghc-trifecta)
    (version "1.6.2.1")
    (source
     (origin
       (method url-fetch)
       (uri (string-append
             "https://hackage.haskell.org/package/trifecta/"
             "trifecta-" version ".tar.gz"))
       (sha256
        (base32
         "1rgv62dlmm4vkdymx5rw5jg3w8ifpzg1745rvs1m4kzdx16p5cxs"))))))

;; ghc-cheapskate appeared too new. This follows LTS Haskell.
(define ghc-cheapskate-0.1.0.5
  (package
    (inherit ghc-cheapskate)
    (version "0.1.0.5")
    (source
     (origin
       (method url-fetch)
       (uri (string-append
             "https://hackage.haskell.org/package/cheapskate/cheapskate-"
             version
             ".tar.gz"))
       (sha256
        (base32
         "0cpsmfx5z2xykg71sv8j7pl8ga6pzyjnjdb9bxn00vcpqkzvfqvs"))))
    (arguments
     ;; LTS Haskell says data-default >=0.5 && <0.8
     `(#:configure-flags (list "--allow-newer=data-default")))))

(define-public idris
  (package
    (name "idris")
    (version "1.0")
    (source (origin
              (method url-fetch)
              (uri (string-append
                    "https://hackage.haskell.org/package/"
                    "idris-" version "/idris-" version ".tar.gz"))
              (sha256
               (base32
                "1srbz0cyvd0k1yqgbrwnfj94yg5y3z533q1kzac96z1h7v454s5h"))))
    (build-system haskell-build-system)
    (inputs
     `(("gmp" ,gmp)
       ("ncurses" ,ncurses)
       ("ghc-aeson" ,ghc-aeson-1.1.2.0)
       ("ghc-annotated-wl-pprint" ,ghc-annotated-wl-pprint)
       ("ghc-ansi-terminal" ,ghc-ansi-terminal)
       ("ghc-ansi-wl-pprint" ,ghc-ansi-wl-pprint)
       ("ghc-async" ,ghc-async)
       ("ghc-base64-bytestring" ,ghc-base64-bytestring)
       ("ghc-blaze-html" ,ghc-blaze-html)
       ("ghc-blaze-markup" ,ghc-blaze-markup)
       ("ghc-cheapskate" ,ghc-cheapskate-0.1.0.5)
       ("ghc-code-page" ,ghc-code-page)
       ("ghc-fingertree" ,ghc-fingertree)
       ("ghc-fsnotify" ,ghc-fsnotify)
       ("ghc-ieee754" ,ghc-ieee754)
       ("ghc-mtl" ,ghc-mtl)
       ("ghc-network" ,ghc-network)
       ("ghc-optparse-applicative" ,ghc-optparse-applicative)
       ("ghc-regex-tdfa" ,ghc-regex-tdfa)
       ("ghc-safe" ,ghc-safe)
       ("ghc-split" ,ghc-split)
       ("ghc-terminal-size" ,ghc-terminal-size)
       ("ghc-text" ,ghc-text)
       ("ghc-trifecta" ,ghc-trifecta-1.6.2.1)
       ("ghc-uniplate" ,ghc-uniplate)
       ("ghc-unordered-containers" ,ghc-unordered-containers)
       ("ghc-utf8-string" ,ghc-utf8-string)
       ("ghc-vector" ,ghc-vector)
       ("ghc-vector-binary-instances" ,ghc-vector-binary-instances)
       ("ghc-zip-archive" ,ghc-zip-archive)))
    (arguments
     `(#:tests? #f ; FIXME: Test suite doesn't run in a sandbox.
       #:configure-flags
       (list (string-append "--datasubdir="
                            (assoc-ref %outputs "out") "/lib/idris"))
       #:phases
       (modify-phases %standard-phases
         (add-before 'configure 'set-cc-command
           (lambda _
             (setenv "CC" "gcc")
             #t))
         (add-after 'install 'fix-libs-install-location
           (lambda* (#:key outputs #:allow-other-keys)
             (let* ((out (assoc-ref outputs "out"))
                    (lib (string-append out "/lib/idris"))
                    (modules (string-append lib "/libs")))
               (for-each
                (lambda (module)
                  (symlink (string-append modules "/" module)
                           (string-append lib "/" module)))
                '("prelude" "base" "contrib" "effects" "pruviloj"))))))))
    (native-search-paths
     (list (search-path-specification
            (variable "IDRIS_LIBRARY_PATH")
            (files '("lib/idris")))))
    (home-page "http://www.idris-lang.org")
    (synopsis "General purpose language with full dependent types")
    (description "Idris is a general purpose language with full dependent
types.  It is compiled, with eager evaluation.  Dependent types allow types to
be predicated on values, meaning that some aspects of a program's behaviour
can be specified precisely in the type.  The language is closely related to
Epigram and Agda.")
    (license license:bsd-3)))

;; Idris modules use the gnu-build-system so that the IDRIS_LIBRARY_PATH is set.
(define (idris-default-arguments name)
  `(#:modules ((guix build gnu-build-system)
               (guix build utils)
               (ice-9 ftw)
               (ice-9 match))
    #:phases
    (modify-phases %standard-phases
      (delete 'configure)
      (delete 'build)
      (delete 'check)
      (replace 'install
        (lambda* (#:key inputs outputs #:allow-other-keys)
          (let* ((out (assoc-ref outputs "out"))
                 (idris (assoc-ref inputs "idris"))
                 (idris-bin (string-append idris "/bin/idris"))
                 (idris-libs (string-append idris "/lib/idris/libs"))
                 (module-name (and (string-prefix? "idris-" ,name)
                                   (substring ,name 6)))
                 (ibcsubdir (string-append out "/lib/idris/" module-name))
                 (ipkg (string-append module-name ".ipkg"))
                 (idris-library-path (getenv "IDRIS_LIBRARY_PATH"))
                 (idris-path (string-split idris-library-path #\:))
                 (idris-path-files (apply append
                                          (map (lambda (path)
                                                 (map (lambda (dir)
                                                        (string-append path "/" dir))
                                                      (scandir path))) idris-path)))
                 (idris-path-subdirs (filter (lambda (path)
                                               (and path (match (stat:type (stat path))
                                                           ('directory #t)
                                                           (_ #f))))
                                                    idris-path-files))
                 (install-cmd (cons* idris-bin
                                     "--ibcsubdir" ibcsubdir
                                     "--build" ipkg
                                     ;; only trigger a build, as --ibcsubdir
                                     ;; already installs .ibc files.

                                     (apply append (map (lambda (path)
                                                          (list "--idrispath"
                                                                path))
                                                        idris-path-subdirs)))))
            ;; FIXME: Seems to be a bug in idris that causes a dubious failure.
            (apply system* install-cmd)
            #t))))))

(define-public idris-lightyear
  (let ((commit "6d65ad111b4bed2bc131396f8385528fc6b3678a"))
    (package
      (name "idris-lightyear")
      (version (git-version "0.1" "1" commit))
      (source (origin
                (method git-fetch)
                (uri (git-reference
                      (url "https://github.com/ziman/lightyear")
                      (commit commit)))
                (file-name (git-file-name name version))
                (sha256
                 (base32
                  "1pkxnn3ryr0v0cin4nasw7kgkc9dnnpja1nfbj466mf3qv5s98af"))))
      (build-system gnu-build-system)
      (native-inputs
       `(("idris" ,idris)))
      (arguments (idris-default-arguments name))
      (home-page "https://github.com/ziman/lightyear")
      (synopsis "Lightweight parser combinator library for Idris")
      (description "Lightweight parser combinator library for Idris, inspired
by Parsec.  This package is used (almost) the same way as Parsec, except for one
difference: backtracking.")
      (license license:bsd-2))))

(define-public idris-wl-pprint
  (let ((commit "1d365fcf4ba075859844dbc5eb96a90f57b9f338"))
    (package
      (name "idris-wl-pprint")
      (version (git-version "0.1" "1" commit))
      (source (origin
                (method git-fetch)
                (uri (git-reference
                      (url "https://github.com/shayan-najd/wl-pprint")
                      (commit commit)))
                (file-name (git-file-name name version))
                (sha256
                 (base32
                  "0g7c3y9smifdz4sivi3qmvymhdr7v9kfq45fmfmmvkqcrix0spzn"))))
      (build-system gnu-build-system)
      (native-inputs
       `(("idris" ,idris)))
      (arguments (idris-default-arguments name))
      (home-page "https://github.com/shayan-najd/wl-pprint")
      (synopsis "Pretty printing library")
      (description "A pretty printing library for Idris based on Phil Wadler's
paper A Prettier Printer and on Daan Leijen's extensions in the Haskell
wl-pprint library.")
      (license license:bsd-2))))

(define-public idris-bifunctors
  (let ((commit "53d06a6ccfe70c49c9ae8c8a4135981dd2173202"))
    (package
      (name "idris-bifunctors")
      (version (git-version "0.1" "1" commit))
      (source (origin
                (method git-fetch)
                (uri (git-reference
                      (url "https://github.com/HuwCampbell/Idris-Bifunctors")
                      (commit commit)))
                (file-name (string-append name "-" version "-checkout"))
                (sha256
                 (base32
                  "02vbsd3rmgnj0l1qq787709qcxjbr9890cbad4ykn27f77jk81h4"))))
      (build-system gnu-build-system)
      (native-inputs
       `(("idris" ,idris)))
      (arguments (idris-default-arguments name))
      (home-page "https://github.com/HuwCampbell/Idris-Bifunctors")
      (synopsis "Bifunctor library")
      (description "This is a bifunctor library for Idris based off the
excellent Haskell Bifunctors package from Edward Kmett.")
      (license license:bsd-3))))

(define-public idris-lens
  (let ((commit "26f012005f6849806cea630afe317e42cae97f29"))
    (package
      (name "idris-lens")
      (version (git-version "0.1" "1" commit))
      (source (origin
                (method git-fetch)
                (uri (git-reference
                      (url "https://github.com/HuwCampbell/idris-lens")
                      (commit commit)))
                (file-name (git-file-name name version))
                (sha256
                 (base32
                  "06jzfj6rad08rk92w8jk5byi79svmyg0mrcqhibgx8rkjjy6vmai"))))
      (build-system gnu-build-system)
      (native-inputs
       `(("idris" ,idris)))
      (propagated-inputs
       `(("idris-bifunctors" ,idris-bifunctors)))
      (arguments (idris-default-arguments name))
      (home-page "https://github.com/HuwCampbell/idris-lens")
      (synopsis "Van Laarhoven lenses for Idris")
      (description "Lenses are composable functional references.  They allow
accessing and modifying data within a structure.")
      (license license:bsd-3))))
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)
ae482ce1 DC	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)
ae482ce1 DC	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)
d661ed52 AW	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))))