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