unofficial mirror of guix-patches@gnu.org 
 help / color / mirror / code / Atom feed
* [bug#49607] [PATCH] gnu: Add Idris 2.
@ 2021-07-17 15:42 Xinglu Chen
  2021-10-05 16:37 ` [bug#49607] [PATCH 1/3] gnu: ghc-cheapskate: Update to 0.1.1.2 Attila Lendvai
                   ` (6 more replies)
  0 siblings, 7 replies; 17+ messages in thread
From: Xinglu Chen @ 2021-07-17 15:42 UTC (permalink / raw)
  To: 49607; +Cc: raingloom

From: raingloom <raingloom@riseup.net>

* gnu/packages/idris.scm (idris2): New variable.

Co-authored-by: Xinglu Chen <public@yoctocell.xyz>
---
Based a previous patch by raingloom[1].

Some changes I made:

* Tests are enabled, but only the Chez backend is enabled since that’s
  the only backend we have for now.

* Some environment have been set, which should make it possible to
  import third-party packages.

* The bin/idris2_app directory has been removed, see the comment in the
  code below.

* The executable is wrapped so some environment variables can be set.

* I also changed the synopsis to the one on their GitHub page, and added
  a copyright line for raingloom.

[1]: https://issues.guix.gnu.org/46124#1

 gnu/packages/idris.scm | 120 ++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 119 insertions(+), 1 deletion(-)

diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index ca2772b904..64cb4f37f5 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -3,6 +3,8 @@
 ;;; Copyright © 2016, 2017 David Craven <david@craven.ch>
 ;;; Copyright © 2018 Alex ter Weele <alex.ter.weele@gmail.com>
 ;;; Copyright © 2019, 2021 Eric Bavier <bavier@posteo.net>
+;;; Copyrignt © 2021 raingloom <raingloom@riseup.net>
+;;; Copyright © 2021 Xinglu Chen <public@yoctocell.xyz>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -21,6 +23,8 @@
 
 (define-module (gnu packages idris)
   #:use-module (gnu packages)
+  #: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)
@@ -28,12 +32,16 @@
   #:use-module (gnu packages multiprecision)
   #:use-module (gnu packages ncurses)
   #:use-module (gnu packages perl)
+  #:use-module (gnu packages python)
+  #:use-module (gnu packages sphinx)
   #:use-module (guix build-system gnu)
   #:use-module (guix build-system haskell)
   #:use-module (guix download)
   #:use-module (guix git-download)
   #:use-module ((guix licenses) #:prefix license:)
-  #:use-module (guix packages))
+  #:use-module (guix packages)
+  #:use-module (guix utils)
+  #:use-module (ice-9 regex))
 
 (define-public idris
   (package
@@ -150,6 +158,116 @@ can be specified precisely in the type.  The language is closely related to
 Epigram and Agda.")
     (license license:bsd-3)))
 
+;; TODO: Add other backends?
+(define-public idris2
+  (package
+    (name "idris2")
+    (version "0.4.0")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/idris-lang/Idris2")
+                    (commit (string-append "v" version))))
+              (sha256
+               (base32
+                "105jybjf5s0k6003qzfxchzsfcpsxip180bh3mdmi74d464d0h8g"))))
+    (build-system gnu-build-system)
+    (arguments
+     `(#:test-target "bootstrap-test"
+       #:phases
+       (modify-phases
+           %standard-phases
+         (add-after 'unpack 'patch-paths
+           (lambda* (#:key outputs inputs #:allow-other-keys)
+             (substitute* "config.mk"
+               ((,(regexp-quote "PREFIX ?= $(HOME)/.idris2"))
+                (string-append "PREFIX = "
+                               (assoc-ref outputs "out"))))
+             (substitute* '("src/Compiler/Scheme/Chez.idr"
+                            "src/Compiler/Scheme/Racket.idr"
+                            "bootstrap/idris2_app/idris2.rkt"
+                            "bootstrap/idris2_app/idris2.ss")
+                  ((,(regexp-quote "#!/bin/sh"))
+                   (string-append "#!" (assoc-ref inputs "bash")
+                                  "/bin/sh")))))
+         ;; This is not the kind of bootstrap we want to run
+         (delete 'bootstrap)
+         (delete 'configure)            ; no configure script
+         (replace 'build
+           (lambda _
+             (invoke "make" "bootstrap"
+                     "SCHEME=scheme"
+                     ;; TODO: detect toolchain.
+                     (string-append "CC=" ,(cc-for-target)))))
+         (add-after 'build 'build-doc
+           (lambda _
+             (with-directory-excursion
+                 "docs"
+               (invoke "make" "html"))))
+         (add-before 'check 'set-cc
+           (lambda _
+             (setenv "CC" ,(cc-for-target))))
+         (add-after 'install 'install-doc
+           (lambda* (#:key outputs #:allow-other-keys)
+             (copy-recursively
+              "docs/build/html"
+              (string-append
+               (assoc-ref outputs "out")
+               "/share/doc/"
+               ,name "-" ,version))))
+         (add-after 'install-doc 'fix-ld-library-path
+           (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"))
+               (copy-file (string-append out "/bin/idris2_app/idris2.so")
+                          (string-append out "/bin/idris2"))
+               (delete-file-recursively (string-append out "/bin/idris2_app")))))
+         (add-after 'fix-ld-library-path '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"))
+                    (idris2 (string-append out "/bin/idris2"))
+                    (version ,version))
+               (wrap-program idris2
+                 `("LD_LIBRARY_PATH" ":" prefix
+                   (,(string-append out "/idris2-" version "/lib")))
+                 `("CHEZ" ":" = (,chez)))))))))
+    (inputs
+     `(("bash" ,bash-minimal)
+       ("chez-scheme" ,chez-scheme)
+       ("gmp" ,gmp)))
+    (native-inputs
+     ;; For building docs.
+     `(("python-sphinx" ,python-sphinx)
+       ("python-sphinx-rtd-theme" ,python-sphinx-rtd-theme)
+       ("python" ,python) ))
+    (native-search-paths
+     (list (search-path-specification
+            (variable "IDRIS2_PACKAGE_PATH")
+            (files (list (string-append "idris2-" version))))
+           (search-path-specification
+            (variable "IDRIS2_LIBS")
+            (files (list (string-append "idris2-" version "/lib")))
+            (file-type 'directory))
+           (search-path-specification
+            (variable "IDRIS2_DATA")
+            (files (list (string-append "idris2-" version "/support")))
+            (file-type 'directory))))
+    (home-page "https://idris-lang.org/")
+    (synopsis "Purely functional programming language with first class types")
+    (description
+     "Idris 2 is a general purpose language with dependent linear 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.  It can use multiple languages as code
+generation backends.")
+    (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)

base-commit: 9cb35c02164d929fcb8929e7f454df215df8cf25
-- 
2.32.0







^ permalink raw reply related	[flat|nested] 17+ messages in thread
end of thread, other threads:[~2022-12-08  0:43 UTC | newest]

Thread overview: 17+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
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   ` [bug#49607] [PATCH 3/3] gnu: idris: Add idris2 0.5.1, and 1.3.3-1.5545986 Attila Lendvai
2022-04-14 12:16 ` [bug#49607] [PATCH v2 1/3] gnu: idris: Use wrap-program to define IDRIS_CC 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

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).