unofficial mirror of guix-patches@gnu.org 
 help / color / mirror / code / Atom feed
From: Attila Lendvai <attila@lendvai.name>
To: 49607@debbugs.gnu.org
Cc: Attila Lendvai <attila@lendvai.name>
Subject: [bug#49607] [PATCH 3/3] gnu: idris: Add idris2 0.5.1, and 1.3.3-1.5545986.
Date: Tue,  5 Oct 2021 18:37:58 +0200	[thread overview]
Message-ID: <20211005163757.29637-3-attila@lendvai.name> (raw)
In-Reply-To: <20211005163757.29637-1-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





  parent reply	other threads:[~2021-10-05 18:22 UTC|newest]

Thread overview: 17+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2021-07-17 15:42 [bug#49607] [PATCH] gnu: Add Idris 2 Xinglu Chen
2021-10-05 16:37 ` [bug#49607] [PATCH 1/3] gnu: ghc-cheapskate: Update to 0.1.1.2 Attila Lendvai
2021-10-05 16:37   ` [bug#49607] [PATCH 2/3] gnu: idris: Use wrap-program to define IDRIS_CC Attila Lendvai
2021-10-05 16:37   ` Attila Lendvai [this message]
2022-04-14 12:16 ` [bug#49607] [PATCH v2 1/3] " Attila Lendvai
2022-04-14 12:16   ` [bug#49607] [PATCH 2/3] gnu: idris: Add idris2 0.5.1, and update idris to 1.3.4 Attila Lendvai
2022-04-20 13:50     ` Eric Bavier
2022-04-14 12:16   ` [bug#49607] [PATCH 3/3] gnu: idris: Add doc output and build the html documentation Attila Lendvai
2022-04-14 15:53 ` [bug#49607] a note Attila Lendvai
2022-04-28 13:28 ` [bug#49607] [PATCH v3 1/3] gnu: idris: Use wrap-program to define IDRIS_CC Attila Lendvai
2022-04-28 13:28   ` [bug#49607] [PATCH v3 2/3] gnu: idris: Add idris2 0.5.1 Attila Lendvai
2022-04-28 13:28   ` [bug#49607] [PATCH v3 3/3] gnu: idris: Add doc output and build the html documentation Attila Lendvai
2022-05-17 20:04   ` [bug#49607] [PATCH v3 1/3] gnu: idris: Use wrap-program to define IDRIS_CC Eric Bavier
2022-05-18 17:22     ` Attila Lendvai
2022-07-11 10:41 ` [bug#49607] why not to propagate gcc as a dependency Attila Lendvai
2022-08-23 12:37 ` [bug#49607] Package proposition: Idris2 v0.5.1 contact
2022-12-08  0:42 ` [bug#49607] idris bootstrap, bailing out Attila Lendvai

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

  List information: https://guix.gnu.org/

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20211005163757.29637-3-attila@lendvai.name \
    --to=attila@lendvai.name \
    --cc=49607@debbugs.gnu.org \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
Code repositories for project(s) associated with this public inbox

	https://git.savannah.gnu.org/cgit/guix.git

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).