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