gnu/packages/idris.scm

   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 ;;; Copyright © 2018 Alex ter Weele <alex.ter.weele@gmail.com>
   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)
  23   #:use-module (gnu packages haskell-check)
  24   #:use-module (gnu packages haskell-web)
  25   #:use-module (gnu packages multiprecision)
  26   #:use-module (gnu packages ncurses)
  27   #:use-module (guix build-system gnu)
  28   #:use-module (guix build-system haskell)
  29   #:use-module (guix download)
  30   #:use-module (guix git-download)
  31   #:use-module ((guix licenses) #:prefix license:)
  32   #:use-module (guix packages))
  33
  34 (define-public idris
  35   (package
  36     (name "idris")
  37     (version "1.3.0")
  38     (source (origin
  39               (method url-fetch)
  40               (uri (string-append
  41                     "https://hackage.haskell.org/package/"
  42                     "idris-" version "/idris-" version ".tar.gz"))
  43               (sha256
  44                (base32
  45                 "1w5i2z88li4niykwc6yrgxgfp25ll6ih95cip0ri7d8i7ik03c48"))))
  46     (build-system haskell-build-system)
  47     (inputs
  48      `(("gmp" ,gmp)
  49        ("ncurses" ,ncurses)
  50        ("ghc-aeson" ,ghc-aeson)
  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-async" ,ghc-async)
  55        ("ghc-base64-bytestring" ,ghc-base64-bytestring)
  56        ("ghc-blaze-html" ,ghc-blaze-html)
  57        ("ghc-blaze-markup" ,ghc-blaze-markup)
  58        ("ghc-cheapskate" ,ghc-cheapskate)
  59        ("ghc-code-page" ,ghc-code-page)
  60        ("ghc-fingertree" ,ghc-fingertree)
  61        ("ghc-fsnotify" ,ghc-fsnotify)
  62        ("ghc-ieee754" ,ghc-ieee754)
  63        ("ghc-megaparsec" ,ghc-megaparsec)
  64        ("ghc-network" ,ghc-network)
  65        ("ghc-optparse-applicative" ,ghc-optparse-applicative)
  66        ("ghc-regex-tdfa" ,ghc-regex-tdfa)
  67        ("ghc-safe" ,ghc-safe)
  68        ("ghc-split" ,ghc-split)
  69        ("ghc-terminal-size" ,ghc-terminal-size)
  70        ("ghc-text" ,ghc-text)
  71        ("ghc-uniplate" ,ghc-uniplate)
  72        ("ghc-unordered-containers" ,ghc-unordered-containers)
  73        ("ghc-utf8-string" ,ghc-utf8-string)
  74        ("ghc-vector" ,ghc-vector)
  75        ("ghc-vector-binary-instances" ,ghc-vector-binary-instances)
  76        ("ghc-zip-archive" ,ghc-zip-archive)))
  77     (arguments
  78      `(#:tests? #f ; FIXME: Test suite doesn't run in a sandbox.
  79        #:configure-flags
  80        (list (string-append "--datasubdir="
  81                             (assoc-ref %outputs "out") "/lib/idris"))
  82        #:phases
  83        (modify-phases %standard-phases
  84          (add-before 'configure 'set-cc-command
  85            (lambda _
  86              (setenv "CC" "gcc")
  87              #t))
  88          (add-before 'configure 'update-constraints
  89            (lambda _
  90              (substitute* "idris.cabal"
  91                (("aeson >= 0\\.6 && < 1\\.3")
  92                 "aeson >= 0.6 && < 1.4"))))
  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)))
 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
 151                                      "--build" ipkg
 152                                      ;; only trigger a build, as --ibcsubdir
 153                                      ;; already installs .ibc files.
 154
 155                                      (apply append (map (lambda (path)
 156                                                           (list "--idrispath"
 157                                                                 path))
 158                                                         idris-path-subdirs)))))
 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))))
 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))))
 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))))
 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))))