From: contact@phfrohring.com
To: 49607@debbugs.gnu.org
Subject: [bug#49607] Package proposition: Idris2 v0.5.1
Date: Tue, 23 Aug 2022 14:37:16 +0200 [thread overview]
Message-ID: <d764852f8ff1019e8e6a96cb0f2dc2f3@phfrohring.com> (raw)
In-Reply-To: <ee2e60c3f133981cc5695ef93e1b4e87dff87c04.1626536112.git.public@yoctocell.xyz>
[-- Attachment #1: Type: text/plain, Size: 170 bytes --]
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
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #2: 0001-gnu-Add-idris2-v0.5.1.patch --]
[-- Type: text/x-diff; name=0001-gnu-Add-idris2-v0.5.1.patch, Size: 10349 bytes --]
From 06d20e3e6ad2e08b0acd291cd4de3efeec76deb9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-Henry=20Fr=C3=B6hring?= <contact@phfrohring.com>
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
next prev parent reply other threads:[~2022-08-23 12:48 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 ` [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 ` contact [this message]
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
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=d764852f8ff1019e8e6a96cb0f2dc2f3@phfrohring.com \
--to=contact@phfrohring.com \
--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 external index
https://git.savannah.gnu.org/cgit/guix.git
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.