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, 2022 Eric Bavier <bavier@posteo.net>
   6 ;;; Copyright © 2022 Attila Lendvai <attila@lendvai.name>
   7 ;;;
   8 ;;; This file is part of GNU Guix.
   9 ;;;
  10 ;;; GNU Guix is free software; you can redistribute it and/or modify it
  11 ;;; under the terms of the GNU General Public License as published by
  12 ;;; the Free Software Foundation; either version 3 of the License, or (at
  13 ;;; your option) any later version.
  14 ;;;
  15 ;;; GNU Guix is distributed in the hope that it will be useful, but
  16 ;;; WITHOUT ANY WARRANTY; without even the implied warranty of
  17 ;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  18 ;;; GNU General Public License for more details.
  19 ;;;
  20 ;;; You should have received a copy of the GNU General Public License
  21 ;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.
  22
  23 (define-module (gnu packages idris)
  24   #:use-module (gnu packages)
  25   #:use-module (gnu packages haskell-check)
  26   #:use-module (gnu packages haskell-web)
  27   #:use-module (gnu packages haskell-xyz)
  28   #:use-module (gnu packages libffi)
  29   #:use-module (gnu packages multiprecision)
  30   #:use-module (gnu packages ncurses)
  31   #:use-module (gnu packages perl)
  32   #:use-module (guix build-system gnu)
  33   #:use-module (guix build-system haskell)
  34   #:use-module (guix download)
  35   #:use-module (guix git-download)
  36   #:use-module (guix utils)
  37   #:use-module ((guix licenses) #:prefix license:)
  38   #:use-module (guix packages))
  39
  40 (define-public idris
  41   (package
  42     (name "idris")
  43     (version "1.3.4")
  44     (source (origin
  45               (method git-fetch)
  46               (uri (git-reference
  47                     (url "https://github.com/idris-lang/Idris-dev.git")
  48                     (commit (string-append "v" version))))
  49               (file-name (git-file-name name version))
  50               (sha256
  51                (base32
  52                 "0cd2a92323hb9a6wy8sc0cqwnisf4pv8y9y2rxvxcbyv8cs1q8g2"))
  53               (patches (search-patches "idris-test-ffi008.patch"))))
  54     (build-system haskell-build-system)
  55     (native-inputs                      ;For tests
  56      (list perl ghc-cheapskate ghc-tasty ghc-tasty-golden
  57            ghc-tasty-rerun))
  58     (inputs
  59      (list gmp
  60            ncurses
  61            ghc-aeson
  62            ghc-annotated-wl-pprint
  63            ghc-ansi-terminal
  64            ghc-ansi-wl-pprint
  65            ghc-async
  66            ghc-base64-bytestring
  67            ghc-blaze-html
  68            ghc-blaze-markup
  69            ghc-cheapskate
  70            ghc-code-page
  71            ghc-fingertree
  72            ghc-fsnotify
  73            ghc-ieee754
  74            ghc-libffi
  75            ghc-megaparsec
  76            ghc-network
  77            ghc-optparse-applicative
  78            ghc-regex-tdfa
  79            ghc-safe
  80            ghc-split
  81            ghc-terminal-size
  82            ghc-uniplate
  83            ghc-unordered-containers
  84            ghc-utf8-string
  85            ghc-vector
  86            ghc-vector-binary-instances
  87            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          (add-before 'configure 'update-constraints
 100            (lambda _
 101              (substitute* "idris.cabal"
 102                (("(aeson|ansi-terminal|haskeline|megaparsec|optparse-applicative)\\s+[^,]+" all dep)
 103                 dep))))
 104          (add-before 'configure 'set-cc-command
 105            (lambda _
 106              (setenv "CC" ,(cc-for-target))))
 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                (chmod "test/scripts/timeout" #o755) ;must be executable
 122                (setenv "TASTY_NUM_THREADS" (number->string (parallel-job-count)))
 123                (setenv "IDRIS_CC" ,(cc-for-target)) ;Needed for creating executables
 124                (setenv "PATH" (string-append out "/bin:" (getenv "PATH")))
 125                (apply (assoc-ref %standard-phases 'check) args))))
 126          (add-before 'check 'restore-libidris_rts
 127            (lambda* (#:key outputs #:allow-other-keys)
 128              ;; The Haskell build system moves this library to the
 129              ;; "static" output.  Idris only knows how to find it in the
 130              ;; "out" output, so we restore it here.
 131              (let ((out (assoc-ref outputs "out"))
 132                    (static (assoc-ref outputs "static"))
 133                    (filename "/lib/idris/rts/libidris_rts.a"))
 134                (rename-file (string-append static filename)
 135                             (string-append out filename))))))))
 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
 195 (define-public idris-lightyear
 196   (let ((commit "6d65ad111b4bed2bc131396f8385528fc6b3678a"))
 197     (package
 198       (name "idris-lightyear")
 199       (version (git-version "0.1" "1" commit))
 200       (source (origin
 201                 (method git-fetch)
 202                 (uri (git-reference
 203                       (url "https://github.com/ziman/lightyear")
 204                       (commit commit)))
 205                 (file-name (git-file-name name version))
 206                 (sha256
 207                  (base32
 208                   "1pkxnn3ryr0v0cin4nasw7kgkc9dnnpja1nfbj466mf3qv5s98af"))))
 209       (build-system gnu-build-system)
 210       (native-inputs
 211        (list idris))
 212       (arguments (idris-default-arguments name))
 213       (home-page "https://github.com/ziman/lightyear")
 214       (synopsis "Lightweight parser combinator library for Idris")
 215       (description "Lightweight parser combinator library for Idris, inspired
 216 by Parsec.  This package is used (almost) the same way as Parsec, except for one
 217 difference: backtracking.")
 218       (license license:bsd-2))))
 219
 220 (define-public idris-wl-pprint
 221   (let ((commit "1d365fcf4ba075859844dbc5eb96a90f57b9f338"))
 222     (package
 223       (name "idris-wl-pprint")
 224       (version (git-version "0.1" "1" commit))
 225       (source (origin
 226                 (method git-fetch)
 227                 (uri (git-reference
 228                       (url "https://github.com/shayan-najd/wl-pprint")
 229                       (commit commit)))
 230                 (file-name (git-file-name name version))
 231                 (sha256
 232                  (base32
 233                   "0g7c3y9smifdz4sivi3qmvymhdr7v9kfq45fmfmmvkqcrix0spzn"))))
 234       (build-system gnu-build-system)
 235       (native-inputs
 236        (list idris))
 237       (arguments (idris-default-arguments name))
 238       (home-page "https://github.com/shayan-najd/wl-pprint")
 239       (synopsis "Pretty printing library")
 240       (description "A pretty printing library for Idris based on Phil Wadler's
 241 paper A Prettier Printer and on Daan Leijen's extensions in the Haskell
 242 wl-pprint library.")
 243       (license license:bsd-2))))
 244
 245 (define-public idris-bifunctors
 246   (let ((commit "53d06a6ccfe70c49c9ae8c8a4135981dd2173202"))
 247     (package
 248       (name "idris-bifunctors")
 249       (version (git-version "0.1" "1" commit))
 250       (source (origin
 251                 (method git-fetch)
 252                 (uri (git-reference
 253                       (url "https://github.com/HuwCampbell/Idris-Bifunctors")
 254                       (commit commit)))
 255                 (file-name (string-append name "-" version "-checkout"))
 256                 (sha256
 257                  (base32
 258                   "02vbsd3rmgnj0l1qq787709qcxjbr9890cbad4ykn27f77jk81h4"))))
 259       (build-system gnu-build-system)
 260       (native-inputs
 261        (list idris))
 262       (arguments (idris-default-arguments name))
 263       (home-page "https://github.com/HuwCampbell/Idris-Bifunctors")
 264       (synopsis "Bifunctor library")
 265       (description "This is a bifunctor library for Idris based off the
 266 excellent Haskell Bifunctors package from Edward Kmett.")
 267       (license license:bsd-3))))
 268
 269 (define-public idris-lens
 270   (let ((commit "26f012005f6849806cea630afe317e42cae97f29"))
 271     (package
 272       (name "idris-lens")
 273       (version (git-version "0.1" "1" commit))
 274       (source (origin
 275                 (method git-fetch)
 276                 (uri (git-reference
 277                       (url "https://github.com/HuwCampbell/idris-lens")
 278                       (commit commit)))
 279                 (file-name (git-file-name name version))
 280                 (sha256
 281                  (base32
 282                   "06jzfj6rad08rk92w8jk5byi79svmyg0mrcqhibgx8rkjjy6vmai"))))
 283       (build-system gnu-build-system)
 284       (native-inputs
 285        (list idris))
 286       (propagated-inputs
 287        (list idris-bifunctors))
 288       (arguments (idris-default-arguments name))
 289       (home-page "https://github.com/HuwCampbell/idris-lens")
 290       (synopsis "Van Laarhoven lenses for Idris")
 291       (description "Lenses are composable functional references.  They allow
 292 accessing and modifying data within a structure.")
 293       (license license:bsd-3))))