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          ;; This allows us to call the 'idris' binary before installing.
  94          (add-after 'unpack 'set-ld-library-path
  95            (lambda _
  96              (setenv "LD_LIBRARY_PATH" (string-append (getcwd) "/dist/build"))
  97              #t))
  98          (add-after 'unpack 'update-constraints
  99            (lambda _
 100              (substitute* "idris.cabal"
 101                (("ansi-terminal < 0\\.9") "ansi-terminal < 0.10"))
 102              #t))
 103          (add-before 'configure 'set-cc-command
 104            (lambda _
 105              (setenv "CC" "gcc")
 106              #t))
 107          (add-after 'install 'fix-libs-install-location
 108            (lambda* (#:key outputs #:allow-other-keys)
 109              (let* ((out (assoc-ref outputs "out"))
 110                     (lib (string-append out "/lib/idris"))
 111                     (modules (string-append lib "/libs")))
 112                (for-each
 113                 (lambda (module)
 114                   (symlink (string-append modules "/" module)
 115                            (string-append lib "/" module)))
 116                 '("prelude" "base" "contrib" "effects" "pruviloj")))))
 117          (delete 'check)                ;Run check later
 118          (add-after 'install 'check
 119            (lambda* (#:key outputs #:allow-other-keys #:rest args)
 120              (let ((out (assoc-ref outputs "out")))
 121                (setenv "TASTY_NUM_THREADS" (number->string (parallel-job-count)))
 122                (setenv "IDRIS_CC" "gcc") ;Needed for creating executables
 123                (setenv "PATH" (string-append out "/bin:" (getenv "PATH")))
 124                (apply (assoc-ref %standard-phases 'check) args))))
 125          (add-before 'check 'restore-libidris_rts
 126            (lambda* (#:key outputs #:allow-other-keys)
 127              ;; The Haskell build system moves this library to the
 128              ;; "static" output.  Idris only knows how to find it in the
 129              ;; "out" output, so we restore it here.
 130              (let ((out (assoc-ref outputs "out"))
 131                    (static (assoc-ref outputs "static"))
 132                    (filename "/lib/idris/rts/libidris_rts.a"))
 133                (rename-file (string-append static filename)
 134                             (string-append out filename))
 135                #t))))))
 136     (native-search-paths
 137      (list (search-path-specification
 138             (variable "IDRIS_LIBRARY_PATH")
 139             (files '("lib/idris")))))
 140     (home-page "https://www.idris-lang.org")
 141     (synopsis "General purpose language with full dependent types")
 142     (description "Idris is a general purpose language with full dependent
 143 types.  It is compiled, with eager evaluation.  Dependent types allow types to
 144 be predicated on values, meaning that some aspects of a program's behaviour
 145 can be specified precisely in the type.  The language is closely related to
 146 Epigram and Agda.")
 147     (license license:bsd-3)))
 148
 149 ;; Idris modules use the gnu-build-system so that the IDRIS_LIBRARY_PATH is set.
 150 (define (idris-default-arguments name)
 151   `(#:modules ((guix build gnu-build-system)
 152                (guix build utils)
 153                (ice-9 ftw)
 154                (ice-9 match))
 155     #:phases
 156     (modify-phases %standard-phases
 157       (delete 'configure)
 158       (delete 'build)
 159       (delete 'check)
 160       (replace 'install
 161         (lambda* (#:key inputs outputs #:allow-other-keys)
 162           (let* ((out (assoc-ref outputs "out"))
 163                  (idris (assoc-ref inputs "idris"))
 164                  (idris-bin (string-append idris "/bin/idris"))
 165                  (idris-libs (string-append idris "/lib/idris/libs"))
 166                  (module-name (and (string-prefix? "idris-" ,name)
 167                                    (substring ,name 6)))
 168                  (ibcsubdir (string-append out "/lib/idris/" module-name))
 169                  (ipkg (string-append module-name ".ipkg"))
 170                  (idris-library-path (getenv "IDRIS_LIBRARY_PATH"))
 171                  (idris-path (string-split idris-library-path #\:))
 172                  (idris-path-files (apply append
 173                                           (map (lambda (path)
 174                                                  (map (lambda (dir)
 175                                                         (string-append path "/" dir))
 176                                                       (scandir path))) idris-path)))
 177                  (idris-path-subdirs (filter (lambda (path)
 178                                                (and path (match (stat:type (stat path))
 179                                                            ('directory #t)
 180                                                            (_ #f))))
 181                                                     idris-path-files))
 182                  (install-cmd (cons* idris-bin
 183                                      "--ibcsubdir" ibcsubdir
 184                                      "--build" ipkg
 185                                      ;; only trigger a build, as --ibcsubdir
 186                                      ;; already installs .ibc files.
 187
 188                                      (apply append (map (lambda (path)
 189                                                           (list "--idrispath"
 190                                                                 path))
 191                                                         idris-path-subdirs)))))
 192             ;; FIXME: Seems to be a bug in idris that causes a dubious failure.
 193             (apply system* install-cmd)
 194             #t))))))
 195
 196 (define-public idris-lightyear
 197   (let ((commit "6d65ad111b4bed2bc131396f8385528fc6b3678a"))
 198     (package
 199       (name "idris-lightyear")
 200       (version (git-version "0.1" "1" commit))
 201       (source (origin
 202                 (method git-fetch)
 203                 (uri (git-reference
 204                       (url "https://github.com/ziman/lightyear")
 205                       (commit commit)))
 206                 (file-name (git-file-name name version))
 207                 (sha256
 208                  (base32
 209                   "1pkxnn3ryr0v0cin4nasw7kgkc9dnnpja1nfbj466mf3qv5s98af"))))
 210       (build-system gnu-build-system)
 211       (native-inputs
 212        `(("idris" ,idris)))
 213       (arguments (idris-default-arguments name))
 214       (home-page "https://github.com/ziman/lightyear")
 215       (synopsis "Lightweight parser combinator library for Idris")
 216       (description "Lightweight parser combinator library for Idris, inspired
 217 by Parsec.  This package is used (almost) the same way as Parsec, except for one
 218 difference: backtracking.")
 219       (license license:bsd-2))))
 220
 221 (define-public idris-wl-pprint
 222   (let ((commit "1d365fcf4ba075859844dbc5eb96a90f57b9f338"))
 223     (package
 224       (name "idris-wl-pprint")
 225       (version (git-version "0.1" "1" commit))
 226       (source (origin
 227                 (method git-fetch)
 228                 (uri (git-reference
 229                       (url "https://github.com/shayan-najd/wl-pprint")
 230                       (commit commit)))
 231                 (file-name (git-file-name name version))
 232                 (sha256
 233                  (base32
 234                   "0g7c3y9smifdz4sivi3qmvymhdr7v9kfq45fmfmmvkqcrix0spzn"))))
 235       (build-system gnu-build-system)
 236       (native-inputs
 237        `(("idris" ,idris)))
 238       (arguments (idris-default-arguments name))
 239       (home-page "https://github.com/shayan-najd/wl-pprint")
 240       (synopsis "Pretty printing library")
 241       (description "A pretty printing library for Idris based on Phil Wadler's
 242 paper A Prettier Printer and on Daan Leijen's extensions in the Haskell
 243 wl-pprint library.")
 244       (license license:bsd-2))))
 245
 246 (define-public idris-bifunctors
 247   (let ((commit "53d06a6ccfe70c49c9ae8c8a4135981dd2173202"))
 248     (package
 249       (name "idris-bifunctors")
 250       (version (git-version "0.1" "1" commit))
 251       (source (origin
 252                 (method git-fetch)
 253                 (uri (git-reference
 254                       (url "https://github.com/HuwCampbell/Idris-Bifunctors")
 255                       (commit commit)))
 256                 (file-name (string-append name "-" version "-checkout"))
 257                 (sha256
 258                  (base32
 259                   "02vbsd3rmgnj0l1qq787709qcxjbr9890cbad4ykn27f77jk81h4"))))
 260       (build-system gnu-build-system)
 261       (native-inputs
 262        `(("idris" ,idris)))
 263       (arguments (idris-default-arguments name))
 264       (home-page "https://github.com/HuwCampbell/Idris-Bifunctors")
 265       (synopsis "Bifunctor library")
 266       (description "This is a bifunctor library for Idris based off the
 267 excellent Haskell Bifunctors package from Edward Kmett.")
 268       (license license:bsd-3))))
 269
 270 (define-public idris-lens
 271   (let ((commit "26f012005f6849806cea630afe317e42cae97f29"))
 272     (package
 273       (name "idris-lens")
 274       (version (git-version "0.1" "1" commit))
 275       (source (origin
 276                 (method git-fetch)
 277                 (uri (git-reference
 278                       (url "https://github.com/HuwCampbell/idris-lens")
 279                       (commit commit)))
 280                 (file-name (git-file-name name version))
 281                 (sha256
 282                  (base32
 283                   "06jzfj6rad08rk92w8jk5byi79svmyg0mrcqhibgx8rkjjy6vmai"))))
 284       (build-system gnu-build-system)
 285       (native-inputs
 286        `(("idris" ,idris)))
 287       (propagated-inputs
 288        `(("idris-bifunctors" ,idris-bifunctors)))
 289       (arguments (idris-default-arguments name))
 290       (home-page "https://github.com/HuwCampbell/idris-lens")
 291       (synopsis "Van Laarhoven lenses for Idris")
 292       (description "Lenses are composable functional references.  They allow
 293 accessing and modifying data within a structure.")
 294       (license license:bsd-3))))