From 06d20e3e6ad2e08b0acd291cd4de3efeec76deb9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Henry=20Fr=C3=B6hring?= Date: Tue, 23 Aug 2022 14:29:23 +0200 Subject: [PATCH] gnu: Add idris2 v0.5.1. * gnu/packages/idris.scm (idris2): New variable. --- gnu/packages/idris.scm | 180 +++++++++++++++++++++++++++++++++++++---- 1 file changed, 163 insertions(+), 17 deletions(-) diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm index 8f08ed3a3e..34511012ec 100644 --- a/gnu/packages/idris.scm +++ b/gnu/packages/idris.scm @@ -20,22 +20,36 @@ ;;; You should have received a copy of the GNU General Public License ;;; along with GNU Guix. If not, see . -(define-module (gnu packages idris) - #:use-module (gnu packages) - #:use-module (gnu packages haskell-check) - #:use-module (gnu packages haskell-web) - #:use-module (gnu packages haskell-xyz) - #:use-module (gnu packages libffi) - #:use-module (gnu packages multiprecision) - #:use-module (gnu packages ncurses) - #:use-module (gnu packages perl) - #:use-module (guix build-system gnu) - #:use-module (guix build-system haskell) - #:use-module (guix download) - #:use-module (guix git-download) - #:use-module (guix utils) - #:use-module ((guix licenses) #:prefix license:) - #:use-module (guix packages)) +(define-module (gnu packages idris)) + +(use-modules + (gnu) + (guix gexp) + (guix utils) + (guix store) + (guix derivations) + (guix packages) + (guix download) + (guix git-download) + (guix build-system gnu) + (guix build-system haskell) + (guix build utils) + ((guix licenses) #:prefix license:)) + +(use-package-modules + haskell-check + haskell-web + haskell-xyz + libffi + ncurses + perl + gcc + multiprecision + bash + base + linux + python + chez) (define-public idris (package @@ -146,6 +160,138 @@ (define-public idris Epigram and Agda.") (license license:bsd-3))) +(define-public idris2 + (package + (name "idris2") + (version "0.5.1") + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/idris-lang/Idris2") + (commit (string-append "v" version)))) + (sha256 + (base32 + "09k5fxnplp6fv3877ynz1lwq9zapxcxbvfvkn6g68yb0ivrff978")) + (file-name (git-file-name name version)))) + (build-system gnu-build-system) + (arguments + (list #:make-flags #~(list "SCHEME=chez-scheme" + (string-append "CC=" + #$(cc-for-target)) + (string-append "PREFIX=" + #$output)) + #:phases #~(modify-phases %standard-phases + (add-after 'set-paths 'patch-paths + (lambda* _ + (define (add value var) + (let ((prev (getenv var))) + (if prev + (setenv var + (string-join (list prev value) ":")) + (setenv var value)))) + (add (string-append #$output "/lib") + "LD_LIBRARY_PATH") + (add (string-append #$output "/bin") "PATH"))) + (add-after 'unpack 'patch-shebangs + (lambda* (#:key inputs #:allow-other-keys) + (substitute* '("src/Compiler/Scheme/ChezSep.idr" + "src/Compiler/Scheme/Chez.idr" + "src/Compiler/Scheme/Racket.idr" + "bootstrap/idris2_app/idris2.rkt" + "bootstrap/idris2_app/idris2.ss") + (("(#!) *(/bin/sh)" _ shebang exec) + (string-append shebang " " + (assoc-ref inputs "bash-minimal") + exec))))) + (delete 'bootstrap) + (delete 'configure) + (add-before 'build 'bootstrap + (lambda* (#:key make-flags #:allow-other-keys) + (apply invoke "make" "bootstrap" make-flags) + (apply invoke "make" "install" make-flags))) + (replace 'build + (lambda* (#:key make-flags #:allow-other-keys) + (apply invoke "make" "clean" make-flags) + (apply invoke "make" "all" make-flags))) + (add-after 'install 'patch-/bin/idris2 + (lambda* _ + (let ((idris2 (string-append #$output "/bin/" + #$name)) + (idris2_app (string-append #$output + "/bin/idris2_app"))) + (delete-file idris2) + (rename-file (string-append idris2_app + "/idris2.so") idris2) + (delete-file-recursively idris2_app)))) + (add-after 'patch-/bin/idris2 'wrap-idris2 + (lambda* (#:key inputs #:allow-other-keys) + (let* ((chez (string-append (assoc-ref inputs + "chez-scheme") + "/bin/chez-scheme")) + (idris2-prefix #$output) + (idris2-version (string-append + idris2-prefix "/" + #$name "-" + #$version)) + (idris2-lib (string-append idris2-version + "/lib")) + (idris2-support (string-append + idris2-version "/support")) + (idris2-bin (string-append idris2-prefix + "/bin/" + #$name))) + (wrap-program idris2-bin + (list "CHEZ" + '= + (list chez)) + (list "IDRIS2_PREFIX" + '= + (list idris2-prefix)) + (list "IDRIS2_LIBS" + 'suffix + (list idris2-lib)) + (list "IDRIS2_DATA" + 'suffix + (list idris2-support)) + (list "IDRIS2_PACKAGE_PATH" + 'suffix + (list idris2-version)) + (list "LD_LIBRARY_PATH" + 'suffix + (list idris2-lib)) + (list "DYLD_LIBRARY_PATH" + 'suffix + (list idris2-lib)))))) + (add-before 'check 'set-INTERACTIVE-IDRIS2 + (lambda* _ + (setenv "INTERACTIVE" "") + (setenv "IDRIS2" + (string-append #$output "/bin/" + #$name)))) + (add-after 'build 'build-doc + (lambda* (#:key make-flags #:allow-other-keys) + (apply invoke "make" "install-libdocs" make-flags)))) + #:test-target "test" + #:parallel-build? #f)) + (inputs (list gcc-12 + chez-scheme + gmp + coreutils + bash-minimal + python)) + (home-page "https://www.idris-lang.org/") + (synopsis + "Programming language designed to encourage Type-Driven Development") + (description + "Idris is a programming language designed to encourage Type-Driven Development. + +In type-driven development, types are tools for constructing programs. We +treat the type as the plan for a program, and use the compiler and type +checker as our assistant, guiding us to a complete program that satisfies the +type. The more expressive the type is that we give up front, the more +confidence we can have that the resulting program will be correct.") + (license license:bsd-3))) + ;; 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) @@ -178,7 +324,7 @@ (define (idris-default-arguments name) (and path (match (stat:type (stat path)) ('directory #t) (_ #f)))) - idris-path-files)) + idris-path-files)) (install-cmd (cons* idris-bin "--ibcsubdir" ibcsubdir "--build" ipkg -- 2.37.2