@@ -19,9 +19,22 @@
;;; You should have received a copy of the GNU General Public License
;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>.
+;;; TODO
+;;;
+;;; - Idris has multiple backends, but we only register Chez as an
+;;; input. Decide how to make backends optional, and/or which ones to package
+;;; by default.
+;;;
+;;; - Set RUNPATH instead of using LD_LIBRARY_PATH. See
+;;; http://blog.tremily.us/posts/rpath/ This needs patching Idris so that it
+;;; stops using a wrapper script and finds its libidris_support.so
+;;; e.g. relative to the executable.
+
(define-module (gnu packages idris)
#:use-module (gnu packages)
+ #:use-module (gnu packages base)
#:use-module (gnu packages bash)
+ #:use-module (gnu packages chez)
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
#:use-module (gnu packages haskell-xyz)
@@ -29,14 +42,21 @@
#:use-module (gnu packages llvm)
#:use-module (gnu packages multiprecision)
#:use-module (gnu packages ncurses)
+ #:use-module (gnu packages node)
#:use-module (gnu packages perl)
+ #:use-module (gnu packages racket)
+ #:use-module (gnu packages version-control)
#:use-module (guix build-system gnu)
#:use-module (guix build-system haskell)
#:use-module (guix download)
+ #:use-module (guix git)
#:use-module (guix git-download)
#:use-module ((guix licenses) #:prefix license:)
#:use-module (guix packages)
- #:use-module (guix utils))
+ #:use-module (guix utils)
+ #:use-module (ice-9 match)
+ #:use-module (ice-9 regex)
+ #:export (make-idris-package))
(define-public idris-1.3.3
(package
@@ -148,8 +168,10 @@
(let* ((out (assoc-ref outputs "out"))
(exe (string-append out "/bin/idris")))
(wrap-program exe
- `("IDRIS_CC" = (,',(cc-for-target)))))
- #true)))))
+ `("IDRIS_CC" = (,',(cc-for-target))))
+ (with-directory-excursion (string-append out "/bin/")
+ (symlink ,name (string-append ,name "-" ,version))))
+ #t)))))
(native-search-paths
(list (search-path-specification
(variable "IDRIS_LIBRARY_PATH")
@@ -165,6 +187,160 @@ Epigram and Agda.")
(define-public idris idris-1.3.3)
+(define-public idris-1.3.3-1
+ ;; This is the current latest from the v1.x branch.
+ (let ((commit "55459867fc3f1ac34527a5dd998c37e72b15d488")
+ (revision "1"))
+ (package
+ (inherit idris-1.3.3)
+ (version (git-version "1.3.3" revision commit))
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/attila-lendvai/Idris2")
+ (commit commit)))
+ (sha256
+ (base32
+ "0qsn1953jy74pgppwkax8yrlswb3v46x541ahbl95rshf666nsj6"))
+ (file-name (git-file-name "idris" version))))
+ (inputs
+ (append (package-inputs idris-1.3.3)
+ `(("ghc-haskeline-0.8" ,ghc-haskeline-0.8)))))))
+
+(define* (make-idris-package source version
+ #:key bootstrap-idris
+ (ignore-test-failures? #false)
+ (unwrap? #true)
+ (tests? #true)
+ (files-to-patch-for-shell
+ '("src/Compiler/Scheme/Chez.idr"
+ "src/Compiler/Scheme/Racket.idr"
+ "src/Compiler/Scheme/Gambit.idr"
+ "src/Compiler/ES/Node.idr"
+ "bootstrap/idris2_app/idris2.rkt"
+ "bootstrap/idris2_app/idris2.ss"))
+ (with-bootstrap-shortcut? #true))
+ (package
+ (name "idris2")
+ (version version)
+ (source (match source
+ ((commit hash . url)
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url (if (null? url)
+ "https://github.com/idris-lang/Idris2.git"
+ (car url)))
+ (commit commit)))
+ (sha256 (base32 hash))
+ (file-name (git-file-name name version))))
+ ((? git-checkout?)
+ source)))
+ (build-system gnu-build-system)
+ (native-inputs
+ `(,@(if with-bootstrap-shortcut?
+ `(("chez-scheme" ,chez-scheme))
+ `(("bootstrap-idris" ,bootstrap-idris)))
+ ("cc" ,clang-toolchain-12) ; clang or older clang-toolchain's don't have a bin/cc
+ ("coreutils" ,coreutils)
+ ("git" ,git)
+ ("node" ,node) ; only for the tests
+ ("racket" ,racket) ; only for the tests
+ ("sed" ,sed)))
+ (inputs
+ `(("bash" ,bash-minimal)
+ ("chez-scheme" ,chez-scheme)
+ ("gmp" ,gmp)))
+ (arguments
+ `(#:tests? ,tests?
+ #:make-flags
+ (list (string-append "CC=" ,(cc-for-target))
+ ,@(if with-bootstrap-shortcut?
+ '((string-append "SCHEME="
+ (assoc-ref %build-inputs "chez-scheme")
+ "/bin/scheme"))
+ `((string-append "BOOTSTRAP_IDRIS="
+ (assoc-ref %build-inputs "bootstrap-idris")
+ "/bin/" ,(package-name bootstrap-idris))))
+ (string-append "PREFIX=" (assoc-ref %outputs "out"))
+ "-j1")
+ #:phases
+ (modify-phases %standard-phases
+ (delete 'bootstrap)
+ (delete 'configure)
+ (delete 'check) ; check must happen after install and wrap-program
+ (add-after 'unpack 'patch-paths
+ (lambda* (#:key inputs #:allow-other-keys)
+ (substitute* ',files-to-patch-for-shell
+ ((,(regexp-quote "#!/bin/sh"))
+ (string-append "#!" (assoc-ref inputs "bash") "/bin/sh"))
+ (("/usr/bin/env")
+ (string-append (assoc-ref inputs "coreutils") "/bin/env")))
+ #true))
+ ,@(if unwrap?
+ `((add-after 'install 'unwrap
+ (lambda* (#:key outputs #:allow-other-keys)
+ ;; The bin/idris2 calls bin/idris2_app/idris2.so which is
+ ;; the real executable, but it sets LD_LIBRARY_PATH
+ ;; incorrectly. Remove bin/idris2 and replace it with
+ ;; bin/idris2_app/idris2.so instead.
+ (let ((out (assoc-ref outputs "out")))
+ (delete-file (string-append out "/bin/idris2"))
+ (rename-file (string-append out "/bin/idris2_app/idris2.so")
+ (string-append out "/bin/idris2"))
+ (delete-file-recursively (string-append out "/bin/idris2_app"))
+ (delete-file-recursively (string-append out "/lib")))
+ #true)))
+ '())
+ ,@(if with-bootstrap-shortcut?
+ `((replace 'build
+ (lambda* (#:key make-flags #:allow-other-keys)
+ ;; i.e. do not build it using the previous version of
+ ;; Idris, but rather compile the comitted compiler
+ ;; output.
+ (apply invoke "make" "bootstrap" make-flags))))
+ '())
+ (add-after 'unwrap 'wrap-program
+ (lambda* (#:key outputs inputs #:allow-other-keys)
+ (let* ((chez (string-append (assoc-ref inputs "chez-scheme")
+ "/bin/scheme"))
+ (out (assoc-ref outputs "out"))
+ (exe (string-append out "/bin/" ,name))
+ (version ,version))
+ (wrap-program exe
+ `("IDRIS2_PREFIX" = (,out))
+ `("LD_LIBRARY_PATH" prefix (,(string-append out "/idris2-" version "/lib")))
+ `("CC" = (,',(cc-for-target)))
+ `("CHEZ" = (,chez)))
+ (with-directory-excursion (string-append out "/bin/")
+ (symlink ,name (string-append ,name "-" ,version))))
+ #true))
+ (add-after 'wrap-program 'check
+ (lambda* (#:key outputs make-flags #:allow-other-keys)
+ (,(if ignore-test-failures?
+ 'false-if-exception
+ 'begin)
+ (apply invoke "make"
+ "INTERACTIVE="
+ (string-append "IDRIS2="
+ (assoc-ref outputs "out")
+ "/bin/" ,name)
+ "test" make-flags))
+ #true)))))
+ (home-page "https://www.idris-lang.org")
+ (synopsis "General purpose language with full dependent types")
+ (description "Idris is a general purpose language with full dependent
+types. It is compiled, with eager evaluation. Dependent types allow types to
+be predicated on values, meaning that some aspects of a program's behaviour
+can be specified precisely in the type. The language is closely related to
+Epigram and Agda.")
+ (license license:bsd-3)))
+
+(define-public idris2-0.5.1
+ (make-idris-package '("v0.5.1"
+ "09k5fxnplp6fv3877ynz1lwq9zapxcxbvfvkn6g68yb0ivrff978")
+ "0.5.1"))
+
;; Idris modules use the gnu-build-system so that the IDRIS_LIBRARY_PATH is set.
(define (idris-default-arguments name)
`(#:modules ((guix build gnu-build-system)