From: raingloom <raingloom@riseup.net>
To: Xinglu Chen <public@yoctocell.xyz>
Cc: 46124@debbugs.gnu.org
Subject: [bug#46124] [PATCH] Idris 2
Date: Mon, 26 Apr 2021 17:22:40 +0200 [thread overview]
Message-ID: <20210426172240.683c4c2b@riseup.net> (raw)
In-Reply-To: <87r1j267c6.fsf@yoctocell.xyz>
[-- Attachment #1: Type: text/plain, Size: 434 bytes --]
On Thu, 22 Apr 2021 10:39:53 +0200
Xinglu Chen <public@yoctocell.xyz> wrote:
> I think you forgot the attach the patch. ;)
>
Ah heck. That might have been the case.
Here it is.
There hasn't been a tagged release since then, so I'm sending my
original patch, but I should note that in my channel I've been tracking
the latest commit, which does seem to work, although it's been a while
since I used Idris for anything complicated.
[-- Attachment #2: 0001-gnu-Added-Idris-2.patch --]
[-- Type: text/x-patch, Size: 4609 bytes --]
From 7554e53ad682e5baa40fee0776ab88cffc1a7772 Mon Sep 17 00:00:00 2001
From: raingloom <raingloom@riseup.net>
Date: Wed, 27 Jan 2021 06:21:01 +0100
Subject: [PATCH] gnu: Added Idris 2.
* gnu/packages/idris.scm (idris2): New variable.
---
gnu/packages/idris.scm | 80 +++++++++++++++++++++++++++++++++++++++++-
1 file changed, 79 insertions(+), 1 deletion(-)
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index ca2772b904..14de2762a1 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -21,6 +21,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 +30,15 @@
#: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 (ice-9 regex))
(define-public idris
(package
@@ -150,6 +155,79 @@ can be specified precisely in the type. The language is closely related to
Epigram and Agda.")
(license license:bsd-3)))
+(define-public idris2
+ (package
+ (name "idris2")
+ (version "0.3.0")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/idris-lang/Idris2")
+ (commit (string-append "v" version))))
+ (sha256
+ (base32
+ "0sa2lpb7n6xqfknwld9rzm4bnb6qcd0ja1n63cnc5v8wdzr8q7kh"))))
+ (build-system gnu-build-system)
+ (arguments
+ `(#:tests? #f ;; they are run as part of other targets
+ #: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"))))
+ (for-each
+ (lambda (f)
+ (substitute* f
+ ((,(regexp-quote "#!/bin/sh"))
+ (string-append "#!" (assoc-ref inputs "sh")
+ "/bin/sh"))))
+ (list "src/Compiler/Scheme/Chez.idr"
+ "src/Compiler/Scheme/Racket.idr"
+ "bootstrap/idris2_app/idris2.rkt"
+ "bootstrap/idris2_app/idris2.ss"))))
+ ;; this is not the kind of bootstrap we want to run
+ (delete 'bootstrap)
+ (delete 'configure)
+ (replace 'build
+ (lambda _
+ (invoke "make" "bootstrap"
+ "SCHEME=scheme"
+ ;; TODO detect toolchain
+ "CC=gcc")))
+ (add-after 'build 'build-doc
+ (lambda _
+ (with-directory-excursion
+ "docs"
+ (invoke "make" "html"))))
+ (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)))))))
+ (inputs
+ `(("sh" ,bash-minimal)
+ ("chez-scheme" ,chez-scheme)))
+ (native-inputs
+ `(("python-sphinx" ,python-sphinx)
+ ("python-sphinx-rtd-theme" ,python-sphinx-rtd-theme)
+ ("python" ,python)))
+ (home-page "https://idris-lang.org/")
+ (synopsis "A dependently typed programming language, a successor to Idris")
+ (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)
--
2.31.1
next prev parent reply other threads:[~2021-04-26 20:47 UTC|newest]
Thread overview: 10+ messages / expand[flat|nested] mbox.gz Atom feed top
2021-01-27 5:43 [bug#46124] [PATCH] Idris 2 raingloom
[not found] ` <87r1j267c6.fsf@yoctocell.xyz>
2021-04-26 15:22 ` raingloom [this message]
2021-04-26 21:27 ` Maxime Devos
2021-04-29 18:43 ` raingloom
2021-04-30 8:24 ` Xinglu Chen
2021-05-03 2:10 ` raingloom
2021-05-04 17:12 ` Xinglu Chen
2021-05-11 21:47 ` raingloom
2021-05-14 12:08 ` Xinglu Chen
2021-04-30 8:50 ` Maxime Devos
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=20210426172240.683c4c2b@riseup.net \
--to=raingloom@riseup.net \
--cc=46124@debbugs.gnu.org \
--cc=public@yoctocell.xyz \
/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).