[bug#49607] [PATCH 3/3] gnu: idris: Add idris2 0.5.1, and 1.3.3-1.5545986.

[Attila Lendvai <attila@lendvai.name>]

This generality is there because with this it is possible to bootstrap Idris
HEAD all the way down from GHC. It requires patching past releases, which
requires importing them into separate git branches. This has not been merged
into upstream yet, therefore this commit only contains a single use of
MAKE-IDRIS-PACKAGE, but that will change in the future.

Add a symlink to a versioned binary; e.g. add a `bin/idris-1.3.3`.

* gnu/packages/idris.scm (idris-1.3.3-1): New variable, the latest git commit
from the v1.x line of Idris.
(make-idris-package): New function to instantiate a package of Idris2.
(idris2-0.5.1): New variable.
---
 gnu/packages/idris.scm | 182 ++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 179 insertions(+), 3 deletions(-)

diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index 1f6e984a90..4ef18c6da4 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -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)
-- 
2.33.0