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