From: Xinglu Chen <public@yoctocell.xyz>
To: 49607@debbugs.gnu.org
Cc: raingloom <raingloom@riseup.net>
Subject: [bug#49607] [PATCH] gnu: Add Idris 2.
Date: Sat, 17 Jul 2021 17:42:55 +0200 [thread overview]
Message-ID: <ee2e60c3f133981cc5695ef93e1b4e87dff87c04.1626536112.git.public@yoctocell.xyz> (raw)
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
next reply other threads:[~2021-07-17 15:44 UTC|newest]
Thread overview: 17+ messages / expand[flat|nested] mbox.gz Atom feed top
2021-07-17 15:42 Xinglu Chen [this message]
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
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=ee2e60c3f133981cc5695ef93e1b4e87dff87c04.1626536112.git.public@yoctocell.xyz \
--to=public@yoctocell.xyz \
--cc=49607@debbugs.gnu.org \
--cc=raingloom@riseup.net \
/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.