Subject: Package proposition: Idris2 v0.5.1

From: [email-masked]
Date: Tue, 23 Aug 2022 14:37:16 +0200

Dear Guixers,

This package proposition follows from a discussion which last message 
was:

   https://lists.gnu.org/archive/html/help-guix/2022-08/msg00177.html

— PHF

From 06d20e3e6ad2e08b0acd291cd4de3efeec76deb9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-Henry=20Fr=C3=B6hring?= <[email-masked]>
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 <http://www.gnu.org/licenses/>.
 
-(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