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