X-Loop: help-debbugs@HIDDEN
Subject: [bug#46124] [PATCH] Idris 2
Resent-From: raingloom <raingloom@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Wed, 27 Jan 2021 06:32:02 +0000
Resent-Message-ID: <handler.46124.B.161172911723314 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: report 46124
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: 46124 <at> debbugs.gnu.org
X-Debbugs-Original-To: Guix Patches <guix-patches@HIDDEN>
Received: via spool by submit <at> debbugs.gnu.org id=B.161172911723314
(code B ref -1); Wed, 27 Jan 2021 06:32:02 +0000
Received: (at submit) by debbugs.gnu.org; 27 Jan 2021 06:31:57 +0000
Received: from localhost ([127.0.0.1]:43468 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1l4eMu-00063j-OD
for submit <at> debbugs.gnu.org; Wed, 27 Jan 2021 01:31:57 -0500
Received: from lists.gnu.org ([209.51.188.17]:53426)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <raingloom@HIDDEN>) id 1l4eMr-000615-Mf
for submit <at> debbugs.gnu.org; Wed, 27 Jan 2021 01:31:54 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10]:46082)
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from <raingloom@HIDDEN>)
id 1l4eMq-0005oT-RI
for guix-patches@HIDDEN; Wed, 27 Jan 2021 01:31:53 -0500
Received: from mx1.riseup.net ([198.252.153.129]:42308)
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from <raingloom@HIDDEN>)
id 1l4eMo-0007Fk-B7
for guix-patches@HIDDEN; Wed, 27 Jan 2021 01:31:52 -0500
Received: from fews1.riseup.net (unknown [10.0.1.83])
(using TLSv1 with cipher ECDHE-RSA-AES256-SHA (256/256 bits))
(Client CN "*.riseup.net",
Issuer "Sectigo RSA Domain Validation Secure Server CA" (not verified))
by mx1.riseup.net (Postfix) with ESMTPS id 4DQYfV0lh9zFdtV
for <guix-patches@HIDDEN>; Tue, 26 Jan 2021 22:31:46 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=riseup.net; s=squak;
t=1611729106; bh=7zdSXsWWuB7e3t41wohuMyt05BMJmiaORR3SannEAEI=;
h=Date:From:To:Subject:From;
b=RytrKUKmhd25vrYExuSpWwTCCXp6/oOW+ah30ESulYLrbonWy9B5ZdZHrG+Ek5IzU
5cldwzbV1NqHH51HcG3/HaMYrzUrk9Z5F3H218LQ3TARvFveZApBwNZQPmTotJNt+K
U7j7qQymALQLPgJ90mKncV5Fw3p+UbcuNgR+iJbw=
X-Riseup-User-ID: 1C9A1DACFC11D9DEDC54C2F630DC1A35FF850E777CA9251D062000E093E4723A
Received: from [127.0.0.1] (localhost [127.0.0.1])
by fews1.riseup.net (Postfix) with ESMTPSA id 4DQYfT2sYMz5wFM
for <guix-patches@HIDDEN>; Tue, 26 Jan 2021 22:31:45 -0800 (PST)
Date: Wed, 27 Jan 2021 06:43:37 +0100
From: raingloom <raingloom@HIDDEN>
Message-ID: <20210127064337.6a226301@HIDDEN>
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Received-SPF: pass client-ip=198.252.153.129;
envelope-from=raingloom@HIDDEN; helo=mx1.riseup.net
X-Spam_score_int: -27
X-Spam_score: -2.8
X-Spam_bar: --
X-Spam_report: (-2.8 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1,
RCVD_IN_DNSWL_LOW=-0.7, RCVD_IN_MSPIKE_H3=0.001, RCVD_IN_MSPIKE_WL=0.001,
SPF_HELO_PASS=-0.001, SPF_PASS=-0.001 autolearn=ham autolearn_force=no
X-Spam_action: no action
X-Spam-Score: -1.4 (-)
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -2.4 (--)
Now that Idris 2 has had some proper tagged releases, I thought I'd
move it from my channel to Guix proper.
I've been using this package for quite a few months now and it pretty
much works. REPL works, building things works. Couldn't try IDE
functionality but I suppose it probably works if you can set it up in
Vim. That reminds me, I still haven't packaged the Vim mode, but I
don't use Vim so I don't really know its module system.
## Still TODO for the package:
search paths: There are no 3rd party Idris 2 modules yet, but it should
be done soon.
output prefix weirdness: Output is a bit odd, having an idris2-0.3.0
directory in its root, but since this is Guix, I suppose that's not
really a problem. Everything else is in its proper place, in bin, lib,
and share.
clang-toolchain support: Right now CC=gcc is hardcoded. Auto detection
would be preferable.
bootstrap: Right now it's bootstrapped from auto-generated Chez or
Racket. It **can** be built with Idris 1, but it uses such on obscene
amount of RAM that I refuse to consider building it that way ever
again. If someone wants to incorporate that step into Guix, they are
free to do so. Or we could generate it once and then freeze it and use
it as an input. Just leave my poor laptop out of it, it already
suffered enough. And probably leave the CI infrastructure out of it too.
## Bigger TODO:
Build system. Eventually it will need one.
Considering that it has multiple code generation backends, this is not
trivial, as each backend uses a different existing language, the
official ones (that I can remember right now) being:
* Chez
* Racket
* Gambit
* Chicken
* JavaScript/Node
* C
It might also make sense to compile Idris 2 itself with different
backends. It "officially" supports bootstrapping with Chez and Racket,
but others might be possible too.
Anyways, here's the patch, have fun with it, and/or suggest changes,
etc!
Content-Disposition: inline Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Mailer: MIME-tools 5.505 (Entity 5.505) Content-Type: text/plain; charset=utf-8 X-Loop: help-debbugs@HIDDEN From: help-debbugs@HIDDEN (GNU bug Tracking System) To: raingloom <raingloom@HIDDEN> Subject: bug#46124: Acknowledgement ([PATCH] Idris 2) Message-ID: <handler.46124.B.161172911723314.ack <at> debbugs.gnu.org> References: <20210127064337.6a226301@HIDDEN> X-Gnu-PR-Message: ack 46124 X-Gnu-PR-Package: guix-patches X-Gnu-PR-Keywords: patch Reply-To: 46124 <at> debbugs.gnu.org Date: Wed, 27 Jan 2021 06:32:02 +0000 Thank you for filing a new bug report with debbugs.gnu.org. This is an automatically generated reply to let you know your message has been received. Your message is being forwarded to the package maintainers and other interested parties for their attention; they will reply in due course. Your message has been sent to the package maintainer(s): guix-patches@HIDDEN If you wish to submit further information on this problem, please send it to 46124 <at> debbugs.gnu.org. Please do not send mail to help-debbugs@HIDDEN unless you wish to report a problem with the Bug-tracking system. --=20 46124: http://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D46124 GNU Bug Tracking System Contact help-debbugs@HIDDEN with problems
X-Loop: help-debbugs@HIDDEN
Subject: [bug#46124] [PATCH] Idris 2
Resent-From: raingloom <raingloom@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Mon, 26 Apr 2021 20:47:03 +0000
Resent-Message-ID: <handler.46124.B46124.161946997422669 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: followup 46124
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: Xinglu Chen <public@HIDDEN>
Cc: 46124 <at> debbugs.gnu.org
Received: via spool by 46124-submit <at> debbugs.gnu.org id=B46124.161946997422669
(code B ref 46124); Mon, 26 Apr 2021 20:47:03 +0000
Received: (at 46124) by debbugs.gnu.org; 26 Apr 2021 20:46:14 +0000
Received: from localhost ([127.0.0.1]:47333 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1lb87R-0005tU-QV
for submit <at> debbugs.gnu.org; Mon, 26 Apr 2021 16:46:14 -0400
Received: from mx1.riseup.net ([198.252.153.129]:39342)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <raingloom@HIDDEN>) id 1lb87H-0005sC-6i
for 46124 <at> debbugs.gnu.org; Mon, 26 Apr 2021 16:46:06 -0400
Received: from fews1.riseup.net (fews1-pn.riseup.net [10.0.1.83])
(using TLSv1 with cipher ECDHE-RSA-AES256-SHA (256/256 bits))
(Client CN "*.riseup.net",
Issuer "Sectigo RSA Domain Validation Secure Server CA" (not verified))
by mx1.riseup.net (Postfix) with ESMTPS id 4FTcP64W7lzDqgQ;
Mon, 26 Apr 2021 13:46:02 -0700 (PDT)
X-Riseup-User-ID: 67A3C5CC5B40807FD571DE8A7D773202A220DF8DD7985CD49E850154237E3F10
Received: from [127.0.0.1] (localhost [127.0.0.1])
by fews1.riseup.net (Postfix) with ESMTPSA id 4FTcP56fRTz5w4h;
Mon, 26 Apr 2021 13:46:01 -0700 (PDT)
Date: Mon, 26 Apr 2021 17:22:40 +0200
From: raingloom <raingloom@HIDDEN>
Message-ID: <20210426172240.683c4c2b@HIDDEN>
In-Reply-To: <87r1j267c6.fsf@HIDDEN>
References: <20210127064337.6a226301@HIDDEN> <87r1j267c6.fsf@HIDDEN>
MIME-Version: 1.0
Content-Type: multipart/mixed; boundary="MP_/=J6D/.pR/cuCeavvn7rp8qV"
X-Spam-Score: 2.4 (++)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
has NOT identified this incoming email as spam. The original
message has been attached to this so you can view it or label
similar future email. If you have any questions, see
the administrator of that system for details.
Content preview: On Thu,
22 Apr 2021 10:39:53 +0200 Xinglu Chen <public@HIDDEN>
wrote: > I think you forgot the attach the patch. ;) > Ah heck. That might
have been the case. Here it is.
Content analysis details: (2.4 points, 10.0 required)
pts rule name description
---- ---------------------- --------------------------------------------------
0.0 RCVD_IN_MSPIKE_H3 RBL: Good reputation (+3)
[198.252.153.129 listed in wl.mailspike.net]
-0.7 RCVD_IN_DNSWL_LOW RBL: Sender listed at https://www.dnswl.org/,
low trust [198.252.153.129 listed in list.dnswl.org]
2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs
[URI: yoctocell.xyz (xyz)]
1.1 DATE_IN_PAST_03_06 Date: is 3 to 6 hours before Received: date
-0.0 SPF_HELO_PASS SPF: HELO matches SPF record
-0.0 SPF_PASS SPF: sender matches SPF record
0.0 RCVD_IN_MSPIKE_WL Mailspike good senders
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: 1.4 (+)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
has NOT identified this incoming email as spam. The original
message has been attached to this so you can view it or label
similar future email. If you have any questions, see
the administrator of that system for details.
Content preview: On Thu, 22 Apr 2021 10:39:53 +0200 Xinglu Chen <public@HIDDEN>
wrote: > I think you forgot the attach the patch. ;) > Ah heck. That might
have been the case. Here it is.
Content analysis details: (1.4 points, 10.0 required)
pts rule name description
---- ---------------------- --------------------------------------------------
0.0 RCVD_IN_MSPIKE_H3 RBL: Good reputation (+3)
[198.252.153.129 listed in wl.mailspike.net]
-0.7 RCVD_IN_DNSWL_LOW RBL: Sender listed at https://www.dnswl.org/,
low trust
[198.252.153.129 listed in list.dnswl.org]
2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs
[URI: yoctocell.xyz (xyz)]
1.1 DATE_IN_PAST_03_06 Date: is 3 to 6 hours before Received: date
-0.0 SPF_HELO_PASS SPF: HELO matches SPF record
-0.0 SPF_PASS SPF: sender matches SPF record
0.0 RCVD_IN_MSPIKE_WL Mailspike good senders
-1.0 MAILING_LIST_MULTI Multiple indicators imply a widely-seen list
manager
--MP_/=J6D/.pR/cuCeavvn7rp8qV
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Disposition: inline
On Thu, 22 Apr 2021 10:39:53 +0200
Xinglu Chen <public@HIDDEN> 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.
--MP_/=J6D/.pR/cuCeavvn7rp8qV
Content-Type: text/x-patch
Content-Transfer-Encoding: 7bit
Content-Disposition: attachment; filename=0001-gnu-Added-Idris-2.patch
From 7554e53ad682e5baa40fee0776ab88cffc1a7772 Mon Sep 17 00:00:00 2001
From: raingloom <raingloom@HIDDEN>
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
--MP_/=J6D/.pR/cuCeavvn7rp8qV--
X-Loop: help-debbugs@HIDDEN
Subject: [bug#46124] [PATCH] Idris 2
Resent-From: Maxime Devos <maximedevos@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Mon, 26 Apr 2021 21:28:02 +0000
Resent-Message-ID: <handler.46124.B46124.161947247026596 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: followup 46124
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: raingloom <raingloom@HIDDEN>, Xinglu Chen <public@HIDDEN>
Cc: 46124 <at> debbugs.gnu.org
Received: via spool by 46124-submit <at> debbugs.gnu.org id=B46124.161947247026596
(code B ref 46124); Mon, 26 Apr 2021 21:28:02 +0000
Received: (at 46124) by debbugs.gnu.org; 26 Apr 2021 21:27:50 +0000
Received: from localhost ([127.0.0.1]:47412 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1lb8lh-0006ut-M4
for submit <at> debbugs.gnu.org; Mon, 26 Apr 2021 17:27:49 -0400
Received: from baptiste.telenet-ops.be ([195.130.132.51]:52926)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <maximedevos@HIDDEN>) id 1lb8le-0006ui-CT
for 46124 <at> debbugs.gnu.org; Mon, 26 Apr 2021 17:27:47 -0400
Received: from ptr-bvsjgyjmffd7q9timvx.18120a2.ip6.access.telenet.be
([IPv6:2a02:1811:8c09:9d00:aaf1:9810:a0b8:a55d])
by baptiste.telenet-ops.be with bizsmtp
id xZTk240070mfAB401ZTksh; Mon, 26 Apr 2021 23:27:44 +0200
Message-ID: <5003aa160dc82b35b06e60d425a09309199e1670.camel@HIDDEN>
From: Maxime Devos <maximedevos@HIDDEN>
Date: Mon, 26 Apr 2021 23:27:39 +0200
In-Reply-To: <20210426172240.683c4c2b@HIDDEN>
References: <20210127064337.6a226301@HIDDEN>
<87r1j267c6.fsf@HIDDEN> <20210426172240.683c4c2b@HIDDEN>
Content-Type: multipart/signed; micalg="pgp-sha512";
protocol="application/pgp-signature"; boundary="=-+ECGZ9mk7Seq81Ss302w"
User-Agent: Evolution 3.34.2
MIME-Version: 1.0
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=telenet.be; s=r21;
t=1619472464; bh=C0ZabV06I83s7HJGWgfesFuW2VWAR1Pk6c+bAL2eKrA=;
h=Subject:From:To:Cc:Date:In-Reply-To:References;
b=aYTN0MNhNvFcTJGJdfOGqzGEMu42V0tQuJLwatUrGf9bw3lYg4PE2FZjW4p+lQv9S
R6XVWHXwKLMavlMucpG9geoFtH7W3LxujzUV/XbqSEe9dCEO4XhfS5VGIbyF+A8MVn
XWs2bL4eWa3iGDkiPC7qo4/vTr2fEQmP995TzUluyufF2qTrSlFYxPQpR/MsZeMA3G
/6T/SY1QzArb0W/kEkCDgRdzN5Jbped5apdpdWnZla7eivveWG5Otm5gDRbFZmpM+s
KC2LhTwpe6WZBC324wh3x/HYJc6CQmVCsntXBiPfUVdZnbl76mePRFDKGk8zSLE2h7
iZdIGhcuj1e/w==
X-Spam-Score: -0.7 (/)
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.7 (-)
--=-+ECGZ9mk7Seq81Ss302w
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
raingloom schreef op ma 26-04-2021 om 17:22 [+0200]:
> 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.
>=20
> + ;; TODO detect toolchain
> + "CC=3Dgcc")))
Unless idris has a compiler built in that uses gcc for compiling
idris to machine code, this should likely be
,(string-append "CC=3D" (cc-for-target)) instead, such that the
cross-compiler is used when cross-compiling.
Teaching (cc-for-target) to detect which toolchain should be used
is a separate matter. Maybe it could be a macro that looks at
(package-native-inputs this-package) or something.
Greetings,
Maxime.
--=-+ECGZ9mk7Seq81Ss302w
Content-Type: application/pgp-signature; name="signature.asc"
Content-Description: This is a digitally signed message part
Content-Transfer-Encoding: 7bit
-----BEGIN PGP SIGNATURE-----
iI0EABYKADUWIQTB8z7iDFKP233XAR9J4+4iGRcl7gUCYIcwSxccbWF4aW1lZGV2
b3NAdGVsZW5ldC5iZQAKCRBJ4+4iGRcl7ou8AP9bagGIjCuIbHAiN1XmNgTMzlXr
ix9XJKe7v5D9uIVqFwEA95EeNJSEiX9jM8QBH4KAsrvNtbh+rQYznhbxAG1MeAo=
=qTHC
-----END PGP SIGNATURE-----
--=-+ECGZ9mk7Seq81Ss302w--
X-Loop: help-debbugs@HIDDEN
Subject: [bug#46124] [PATCH] Idris 2
Resent-From: raingloom <raingloom@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Thu, 29 Apr 2021 23:21:02 +0000
Resent-Message-ID: <handler.46124.B46124.161973845626992 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: followup 46124
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: Maxime Devos <maximedevos@HIDDEN>
Cc: Xinglu Chen <public@HIDDEN>, 46124 <at> debbugs.gnu.org
Received: via spool by 46124-submit <at> debbugs.gnu.org id=B46124.161973845626992
(code B ref 46124); Thu, 29 Apr 2021 23:21:02 +0000
Received: (at 46124) by debbugs.gnu.org; 29 Apr 2021 23:20:56 +0000
Received: from localhost ([127.0.0.1]:57065 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1lcFxn-00071H-Tc
for submit <at> debbugs.gnu.org; Thu, 29 Apr 2021 19:20:56 -0400
Received: from mx1.riseup.net ([198.252.153.129]:49854)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <raingloom@HIDDEN>) id 1lcFxi-00070o-8d
for 46124 <at> debbugs.gnu.org; Thu, 29 Apr 2021 19:20:53 -0400
Received: from fews2.riseup.net (fews2-pn.riseup.net [10.0.1.84])
(using TLSv1 with cipher ECDHE-RSA-AES256-SHA (256/256 bits))
(Client CN "*.riseup.net",
Issuer "Sectigo RSA Domain Validation Secure Server CA" (not verified))
by mx1.riseup.net (Postfix) with ESMTPS id 4FWWhD5djYzF2pM;
Thu, 29 Apr 2021 16:20:44 -0700 (PDT)
X-Riseup-User-ID: A85BAEA94A02D06A71FF8650C4D829F7C74316CA3801AADC06C1C60B29709618
Received: from [127.0.0.1] (localhost [127.0.0.1])
by fews2.riseup.net (Postfix) with ESMTPSA id 4FWWhC3Zy6z1yS8;
Thu, 29 Apr 2021 16:20:43 -0700 (PDT)
Date: Thu, 29 Apr 2021 20:43:17 +0200
From: raingloom <raingloom@HIDDEN>
Message-ID: <20210429204317.7e3a707c@HIDDEN>
In-Reply-To: <5003aa160dc82b35b06e60d425a09309199e1670.camel@HIDDEN>
References: <20210127064337.6a226301@HIDDEN> <87r1j267c6.fsf@HIDDEN>
<20210426172240.683c4c2b@HIDDEN>
<5003aa160dc82b35b06e60d425a09309199e1670.camel@HIDDEN>
MIME-Version: 1.0
Content-Type: multipart/mixed; boundary="MP_/X7RxX_rpJMU.w8Ngt.a7fAX"
X-Spam-Score: 0.4 (/)
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -0.6 (/)
--MP_/X7RxX_rpJMU.w8Ngt.a7fAX
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Disposition: inline
On Mon, 26 Apr 2021 23:27:39 +0200
Maxime Devos <maximedevos@HIDDEN> wrote:
> raingloom schreef op ma 26-04-2021 om 17:22 [+0200]:
> > 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.
> >
> > + ;; TODO detect toolchain
> > + "CC=gcc")))
>
> Unless idris has a compiler built in that uses gcc for compiling
> idris to machine code, this should likely be
> ,(string-append "CC=" (cc-for-target)) instead, such that the
> cross-compiler is used when cross-compiling.
>
> Teaching (cc-for-target) to detect which toolchain should be used
> is a separate matter. Maybe it could be a macro that looks at
> (package-native-inputs this-package) or something.
>
> Greetings,
> Maxime.
Oh, that's a leftover, I was using clang for a while, since it's
said to use less RAM. I switched back to gcc and left that in.
Here is the updated patch. No idea if this actually works cross
compiled, but I don't have much time to test it. My suspicion is that
it's likely broken and requires changes to Idris 2's code generators,
because they almost definitely call Chez, GCC, etc, with the wrong
arguments.
--MP_/X7RxX_rpJMU.w8Ngt.a7fAX
Content-Type: text/x-patch
Content-Transfer-Encoding: 7bit
Content-Disposition: attachment; filename=0001-gnu-Added-Idris-2.patch
From e3c942454af34879393d073be755fa53390891bc Mon Sep 17 00:00:00 2001
From: raingloom <raingloom@HIDDEN>
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..da66f7b0d8 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
+ ,(string-append "CC=" (cc-for-target)))))
+ (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
--MP_/X7RxX_rpJMU.w8Ngt.a7fAX--
X-Loop: help-debbugs@HIDDEN
Subject: [bug#46124] [PATCH] Idris 2
Resent-From: Xinglu Chen <public@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Fri, 30 Apr 2021 08:25:01 +0000
Resent-Message-ID: <handler.46124.B46124.161977109520241 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: followup 46124
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: raingloom <raingloom@HIDDEN>, Maxime Devos <maximedevos@HIDDEN>
Cc: 46124 <at> debbugs.gnu.org
Received: via spool by 46124-submit <at> debbugs.gnu.org id=B46124.161977109520241
(code B ref 46124); Fri, 30 Apr 2021 08:25:01 +0000
Received: (at 46124) by debbugs.gnu.org; 30 Apr 2021 08:24:55 +0000
Received: from localhost ([127.0.0.1]:57429 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1lcOSF-0005GP-MS
for submit <at> debbugs.gnu.org; Fri, 30 Apr 2021 04:24:55 -0400
Received: from h87-96-130-155.cust.a3fiber.se ([87.96.130.155]:38208
helo=mail.yoctocell.xyz) by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <public@HIDDEN>) id 1lcOSD-0005G7-GL
for 46124 <at> debbugs.gnu.org; Fri, 30 Apr 2021 04:24:54 -0400
From: Xinglu Chen <public@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=yoctocell.xyz;
s=mail; t=1619771084;
bh=HuLMjJSAHea+ZMyVTFbLBptJSvzsOcE8sraxUKPXLgE=;
h=From:To:Cc:Subject:In-Reply-To:References:Date;
b=OK/O/Cqh62+VdV3REVBMlzllGzR3L0NQabYQJpDuZvHGGChhh6S9ic1a7kaYrBJLN
ZhY1VmWeX9mfRdejeESfRHskmlwjRQjEQdjRq3UpD/M884c045ST6/SXqYKd87buWk
BSTz5/lB7OLXCwS/WU7yNcNrT08l7o9bhHLzR1yQ=
In-Reply-To: <20210429204317.7e3a707c@HIDDEN>
References: <20210127064337.6a226301@HIDDEN>
<87r1j267c6.fsf@HIDDEN> <20210426172240.683c4c2b@HIDDEN>
<5003aa160dc82b35b06e60d425a09309199e1670.camel@HIDDEN>
<20210429204317.7e3a707c@HIDDEN>
Date: Fri, 30 Apr 2021 10:24:42 +0200
Message-ID: <87im44nprp.fsf@HIDDEN>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
X-Spam-Score: 2.9 (++)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
has NOT identified this incoming email as spam. The original
message has been attached to this so you can view it or label
similar future email. If you have any questions, see
the administrator of that system for details.
Content preview: On Thu, Apr 29 2021, raingloom wrote: > Here is the updated
patch. No idea if this actually works cross > compiled, but I don't have
much time to test it. My suspicion is that > it's likely broken and requires
changes to Idris 2's code ge [...]
Content analysis details: (2.9 points, 10.0 required)
pts rule name description
---- ---------------------- --------------------------------------------------
2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs
[URI: yoctocell.xyz (xyz)]
-0.0 SPF_PASS SPF: sender matches SPF record
0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record
0.4 RDNS_DYNAMIC Delivered to internal network by host with
dynamic-looking rDNS 0.5 FROM_SUSPICIOUS_NTLD From abused NTLD
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: 2.9 (++)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
has NOT identified this incoming email as spam. The original
message has been attached to this so you can view it or label
similar future email. If you have any questions, see
the administrator of that system for details.
Content preview: On Thu, Apr 29 2021, raingloom wrote: > Here is the updated
patch. No idea if this actually works cross > compiled, but I don't have
much time to test it. My suspicion is that > it's likely broken and requires
changes to Idris 2's code ge [...]
Content analysis details: (2.9 points, 10.0 required)
pts rule name description
---- ---------------------- --------------------------------------------------
2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs
[URI: yoctocell.xyz (xyz)]
-0.0 SPF_PASS SPF: sender matches SPF record
0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record
1.0 BULK_RE_SUSP_NTLD Precedence bulk and RE: from a suspicious TLD
0.4 RDNS_DYNAMIC Delivered to internal network by host with
dynamic-looking rDNS
0.5 FROM_SUSPICIOUS_NTLD From abused NTLD
-1.0 MAILING_LIST_MULTI Multiple indicators imply a widely-seen list
manager
On Thu, Apr 29 2021, raingloom wrote:
> Here is the updated patch. No idea if this actually works cross
> compiled, but I don't have much time to test it. My suspicion is that
> it's likely broken and requires changes to Idris 2's code generators,
> because they almost definitely call Chez, GCC, etc, with the wrong
> arguments.
I noticed that there is an =E2=80=98idris2_app=E2=80=99 directory in the =
=E2=80=98bin=E2=80=99 directory
$ ls /gnu/store/va62hzp46c3dp2vlcnqc7fg109axj8rq-idris2-0.3.0/bin
idris2* idris2_app/
What is this used for?
X-Loop: help-debbugs@HIDDEN
Subject: [bug#46124] [PATCH] Idris 2
Resent-From: Maxime Devos <maximedevos@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Fri, 30 Apr 2021 08:52:01 +0000
Resent-Message-ID: <handler.46124.B46124.161977266522679 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: followup 46124
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: raingloom <raingloom@HIDDEN>
Cc: Xinglu Chen <public@HIDDEN>, 46124 <at> debbugs.gnu.org
Received: via spool by 46124-submit <at> debbugs.gnu.org id=B46124.161977266522679
(code B ref 46124); Fri, 30 Apr 2021 08:52:01 +0000
Received: (at 46124) by debbugs.gnu.org; 30 Apr 2021 08:51:05 +0000
Received: from localhost ([127.0.0.1]:57455 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1lcOrZ-0005tj-C0
for submit <at> debbugs.gnu.org; Fri, 30 Apr 2021 04:51:05 -0400
Received: from laurent.telenet-ops.be ([195.130.137.89]:53396)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <maximedevos@HIDDEN>) id 1lcOrV-0005tH-Hc
for 46124 <at> debbugs.gnu.org; Fri, 30 Apr 2021 04:51:04 -0400
Received: from ptr-bvsjgyjmffd7q9timvx.18120a2.ip6.access.telenet.be
([IPv6:2a02:1811:8c09:9d00:aaf1:9810:a0b8:a55d])
by laurent.telenet-ops.be with bizsmtp
id ywqz2400H0mfAB401wqzyk; Fri, 30 Apr 2021 10:50:59 +0200
Message-ID: <f6728a87fd3de484c16935273bb7ddf5ec656636.camel@HIDDEN>
From: Maxime Devos <maximedevos@HIDDEN>
Date: Fri, 30 Apr 2021 10:50:51 +0200
In-Reply-To: <20210429204317.7e3a707c@HIDDEN>
References: <20210127064337.6a226301@HIDDEN>
<87r1j267c6.fsf@HIDDEN> <20210426172240.683c4c2b@HIDDEN>
<5003aa160dc82b35b06e60d425a09309199e1670.camel@HIDDEN>
<20210429204317.7e3a707c@HIDDEN>
Content-Type: multipart/signed; micalg="pgp-sha512";
protocol="application/pgp-signature"; boundary="=-eegqEHnuNfQ5EQVOsGsM"
User-Agent: Evolution 3.34.2
MIME-Version: 1.0
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=telenet.be; s=r21;
t=1619772659; bh=wByehzKXMQo/tsneKo60ycPEXln53M5SSIbsK2ZUuIA=;
h=Subject:From:To:Cc:Date:In-Reply-To:References;
b=kfl0U68WUKC2SQ3g3hWGphwCym8l7iiEDxAdAgdTn23q1fEyNekPkzPX7SWqks6kB
J6dp62u2kXiCzZrTKKM9J7sT+oGX4s7wV6zEKhXpwvW2R0Ue7EozxivULTT+vC8Vvx
K2nmszy/iYvV9LVJ1MO1HMBrKjHcGJDllbc+nLSnIwA0tRnvCatIYS1hFUdpKMIdbR
HpZfYG94F0tCqnuMvO4ROlckN7fSnU1Wp8fm+sBbRnkUTMm3yrp2h2dXDHNy3irm9W
L9PKeLuYT/D8yoOk/ItFmdZDpkKXCIVRlF6ztwQJi2YCeyZBeLWT2BHEU/CmblLer0
6hwsyG3qTVrOA==
X-Spam-Score: -0.7 (/)
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.7 (-)
--=-eegqEHnuNfQ5EQVOsGsM
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
raingloom schreef op do 29-04-2021 om 20:43 [+0200]:
> On Mon, 26 Apr 2021 23:27:39 +0200
> Maxime Devos <maximedevos@HIDDEN> wrote:
>=20
> > raingloom schreef op ma 26-04-2021 om 17:22 [+0200]:
> > > [...]
> > >=20
> > > + ;; TODO detect toolchain
> > > + "CC=3Dgcc"))) =20
> >=20
> > Unless idris has a compiler built in that uses gcc for compiling
> > idris to machine code, this should likely be
> > ,(string-append "CC=3D" (cc-for-target)) instead, such that the
> > cross-compiler is used when cross-compiling.
> >=20
> > [...]
> Oh, that's a leftover, I was using clang for a while, since it's
> said to use less RAM. I switched back to gcc and left that in.
>=20
> Here is the updated patch. No idea if this actually works cross
> compiled, but I don't have much time to test it.
IIUC, cross-compilation is not required to be supported by each
package in guix. It is something nice-to-have, but not strictly
required.
Greetings,
Maxime.
--=-eegqEHnuNfQ5EQVOsGsM
Content-Type: application/pgp-signature; name="signature.asc"
Content-Description: This is a digitally signed message part
Content-Transfer-Encoding: 7bit
-----BEGIN PGP SIGNATURE-----
iI0EABYKADUWIQTB8z7iDFKP233XAR9J4+4iGRcl7gUCYIvE6xccbWF4aW1lZGV2
b3NAdGVsZW5ldC5iZQAKCRBJ4+4iGRcl7lbgAP9K3rd7WywkbN9sXQRo5g133gvs
wB/gM4kgG1twdqJWLwEAzvg8wNd2oAlo8Hw/jmbS8mJJfvAQFydiM5V5c9PpLAI=
=O2R1
-----END PGP SIGNATURE-----
--=-eegqEHnuNfQ5EQVOsGsM--
X-Loop: help-debbugs@HIDDEN
Subject: [bug#46124] [PATCH] Idris 2
Resent-From: raingloom <raingloom@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Mon, 03 May 2021 09:08:01 +0000
Resent-Message-ID: <handler.46124.B46124.16200328235870 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: followup 46124
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: Xinglu Chen <public@HIDDEN>
Cc: Maxime Devos <maximedevos@HIDDEN>, 46124 <at> debbugs.gnu.org
Received: via spool by 46124-submit <at> debbugs.gnu.org id=B46124.16200328235870
(code B ref 46124); Mon, 03 May 2021 09:08:01 +0000
Received: (at 46124) by debbugs.gnu.org; 3 May 2021 09:07:03 +0000
Received: from localhost ([127.0.0.1]:46209 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1ldUXe-0001WT-3X
for submit <at> debbugs.gnu.org; Mon, 03 May 2021 05:07:02 -0400
Received: from mx1.riseup.net ([198.252.153.129]:55938)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <raingloom@HIDDEN>) id 1ldUXZ-0001Vx-K8
for 46124 <at> debbugs.gnu.org; Mon, 03 May 2021 05:07:00 -0400
Received: from fews1.riseup.net (fews1-pn.riseup.net [10.0.1.83])
(using TLSv1 with cipher ECDHE-RSA-AES256-SHA (256/256 bits))
(Client CN "*.riseup.net",
Issuer "Sectigo RSA Domain Validation Secure Server CA" (not verified))
by mx1.riseup.net (Postfix) with ESMTPS id 4FYcY80x9VzDqCq;
Mon, 3 May 2021 02:06:52 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=riseup.net; s=squak;
t=1620032812; bh=Xj0mXdlPCpBF/jE2mnzQ9pRHhGtssEH+L01pUTYHg+4=;
h=Date:From:To:Cc:Subject:In-Reply-To:References:From;
b=jmgMcmiXQvKlcW9gSZs6QrTMKqUAmWi2kRRP2AX/4CE4l/cwOWxJ/h/mhz0CycIOW
4SgQgdSyl9t1ulrABPM5H/Ysj407fSqYSkcRn03A/nNS3PcEO/iXJUEQnSQQQ+vVR8
xPKfLnvG3auo3YFGMokb0Zh0+RC4PivfvE5Wu1RM=
X-Riseup-User-ID: 41ADFC538ACE53CC682C99CD2FCB2A9AD5CEBB8F6D0E115F355DD9B6E04CAD90
Received: from [127.0.0.1] (localhost [127.0.0.1])
by fews1.riseup.net (Postfix) with ESMTPSA id 4FYcY66Mxdz5vRy;
Mon, 3 May 2021 02:06:50 -0700 (PDT)
Date: Mon, 3 May 2021 04:10:44 +0200
From: raingloom <raingloom@HIDDEN>
Message-ID: <20210503041044.13358182@HIDDEN>
In-Reply-To: <87im44nprp.fsf@HIDDEN>
References: <20210127064337.6a226301@HIDDEN> <87r1j267c6.fsf@HIDDEN>
<20210426172240.683c4c2b@HIDDEN>
<5003aa160dc82b35b06e60d425a09309199e1670.camel@HIDDEN>
<20210429204317.7e3a707c@HIDDEN> <87im44nprp.fsf@HIDDEN>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
X-Spam-Score: 2.4 (++)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
has NOT identified this incoming email as spam. The original
message has been attached to this so you can view it or label
similar future email. If you have any questions, see
the administrator of that system for details.
Content preview: On Fri,
30 Apr 2021 10:24:42 +0200 Xinglu Chen <public@HIDDEN>
wrote: > On Thu, Apr 29 2021, raingloom wrote: > > > Here is the updated
patch. No idea if this actually works cross > > compiled, but I don't have
much time to test it. My suspicion is > > that it's likely [...]
Content analysis details: (2.4 points, 10.0 required)
pts rule name description
---- ---------------------- --------------------------------------------------
-0.7 RCVD_IN_DNSWL_LOW RBL: Sender listed at https://www.dnswl.org/,
low trust [198.252.153.129 listed in list.dnswl.org]
-0.0 SPF_PASS SPF: sender matches SPF record
-0.0 SPF_HELO_PASS SPF: HELO matches SPF record
2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs
[URI: yoctocell.xyz (xyz)]
1.1 DATE_IN_PAST_06_12 Date: is 6 to 12 hours before Received: date
-0.0 RCVD_IN_MSPIKE_H3 RBL: Good reputation (+3)
[198.252.153.129 listed in wl.mailspike.net]
-0.0 RCVD_IN_MSPIKE_WL Mailspike good senders
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: 1.4 (+)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
has NOT identified this incoming email as spam. The original
message has been attached to this so you can view it or label
similar future email. If you have any questions, see
the administrator of that system for details.
Content preview: On Fri, 30 Apr 2021 10:24:42 +0200 Xinglu Chen <public@HIDDEN>
wrote: > On Thu, Apr 29 2021, raingloom wrote: > > > Here is the updated
patch. No idea if this actually works cross > > compiled, but I don't have
much time to test it. My suspicion is > > that it's likely [...]
Content analysis details: (1.4 points, 10.0 required)
pts rule name description
---- ---------------------- --------------------------------------------------
-0.7 RCVD_IN_DNSWL_LOW RBL: Sender listed at https://www.dnswl.org/,
low trust
[198.252.153.129 listed in list.dnswl.org]
-0.0 RCVD_IN_MSPIKE_H3 RBL: Good reputation (+3)
[198.252.153.129 listed in wl.mailspike.net]
-0.0 SPF_PASS SPF: sender matches SPF record
-0.0 SPF_HELO_PASS SPF: HELO matches SPF record
2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs
[URI: yoctocell.xyz (xyz)]
1.1 DATE_IN_PAST_06_12 Date: is 6 to 12 hours before Received: date
-0.0 RCVD_IN_MSPIKE_WL Mailspike good senders
-1.0 MAILING_LIST_MULTI Multiple indicators imply a widely-seen list
manager
On Fri, 30 Apr 2021 10:24:42 +0200
Xinglu Chen <public@HIDDEN> wrote:
> On Thu, Apr 29 2021, raingloom wrote:
>=20
> > Here is the updated patch. No idea if this actually works cross
> > compiled, but I don't have much time to test it. My suspicion is
> > that it's likely broken and requires changes to Idris 2's code
> > generators, because they almost definitely call Chez, GCC, etc,
> > with the wrong arguments. =20
>=20
> I noticed that there is an =E2=80=98idris2_app=E2=80=99 directory in the =
=E2=80=98bin=E2=80=99
> directory
>=20
> $ ls /gnu/store/va62hzp46c3dp2vlcnqc7fg109axj8rq-idris2-0.3.0/bin
> idris2* idris2_app/
>=20
> What is this used for?
>=20
If you take a look at $(guix build idris2)/bin/idris2, it's actually
just a wrapper. It contains the supporting dynamically linked shared
objects and the executable itself.
I don't know the details of what each file does or why it's like this,
the codegen seems to use a similar structure for all backends. The
scheme files are probably all for the Chez backend, the shared objects
are either C libraries (for socket support and stuff), or compiled Chez
code. I just noticed the Racket script, that I have no idea about.
Idris 2's build system makes some... uhm... interesting choices, so
it's entirely possible that not all of those are necessary, or could be
moved somewhere more sensible.
X-Loop: help-debbugs@HIDDEN
Subject: [bug#46124] [PATCH] Idris 2
Resent-From: Xinglu Chen <public@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Tue, 04 May 2021 17:13:02 +0000
Resent-Message-ID: <handler.46124.B46124.162014835013858 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: followup 46124
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: raingloom <raingloom@HIDDEN>
Cc: Maxime Devos <maximedevos@HIDDEN>, 46124 <at> debbugs.gnu.org
Received: via spool by 46124-submit <at> debbugs.gnu.org id=B46124.162014835013858
(code B ref 46124); Tue, 04 May 2021 17:13:02 +0000
Received: (at 46124) by debbugs.gnu.org; 4 May 2021 17:12:30 +0000
Received: from localhost ([127.0.0.1]:54364 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1ldyb0-0003bS-8E
for submit <at> debbugs.gnu.org; Tue, 04 May 2021 13:12:30 -0400
Received: from h87-96-130-155.cust.a3fiber.se ([87.96.130.155]:54754
helo=mail.yoctocell.xyz) by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <public@HIDDEN>) id 1ldyaw-0003bL-T4
for 46124 <at> debbugs.gnu.org; Tue, 04 May 2021 13:12:29 -0400
From: Xinglu Chen <public@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=yoctocell.xyz;
s=mail; t=1620148339;
bh=z4tAIrwX1y2UAWOSinUVmGptDet1iJxgtBtTWEGfbyM=;
h=From:To:Cc:Subject:In-Reply-To:References:Date;
b=GP9k01kn7lMU8yApUNRQaiTRDXTW5n1KodSJFUoArGJP7zL/aTMoxTI0B32rkLYyC
TQS4RJnA9TkkRw8HaoasxSfWlxNq0ROYukjrO04N373Qpja7ccDNO9XTb7GhcyXvkL
qyJHz8CHXd+sjzmtgGpTubZOj4HOjda3wzXUNwGk=
In-Reply-To: <20210503041044.13358182@HIDDEN>
References: <20210127064337.6a226301@HIDDEN>
<87r1j267c6.fsf@HIDDEN> <20210426172240.683c4c2b@HIDDEN>
<5003aa160dc82b35b06e60d425a09309199e1670.camel@HIDDEN>
<20210429204317.7e3a707c@HIDDEN> <87im44nprp.fsf@HIDDEN>
<20210503041044.13358182@HIDDEN>
Date: Tue, 04 May 2021 19:12:18 +0200
Message-ID: <87mttae83x.fsf@HIDDEN>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
X-Spam-Score: 2.9 (++)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
has NOT identified this incoming email as spam. The original
message has been attached to this so you can view it or label
similar future email. If you have any questions, see
the administrator of that system for details.
Content preview: On Mon, May 03 2021, raingloom wrote: > On Fri, 30 Apr 2021
10:24:42 +0200 > Xinglu Chen <public@HIDDEN> wrote: > >> On Thu, Apr
29 2021, raingloom wrote: >> >> > Here is the updated patch. No idea if this
actually works cross >> > [...]
Content analysis details: (2.9 points, 10.0 required)
pts rule name description
---- ---------------------- --------------------------------------------------
2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs
[URI: yoctocell.xyz (xyz)]
0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record
-0.0 SPF_PASS SPF: sender matches SPF record
0.4 RDNS_DYNAMIC Delivered to internal network by host with
dynamic-looking rDNS 0.5 FROM_SUSPICIOUS_NTLD From abused NTLD
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: 2.9 (++)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
has NOT identified this incoming email as spam. The original
message has been attached to this so you can view it or label
similar future email. If you have any questions, see
the administrator of that system for details.
Content preview: On Mon, May 03 2021, raingloom wrote: > On Fri, 30 Apr 2021
10:24:42 +0200 > Xinglu Chen <public@HIDDEN> wrote: > >> On Thu, Apr
29 2021, raingloom wrote: >> >> > Here is the updated patch. No idea if this
actually works cross >> > [...]
Content analysis details: (2.9 points, 10.0 required)
pts rule name description
---- ---------------------- --------------------------------------------------
2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs
[URI: yoctocell.xyz (xyz)]
0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record
-0.0 SPF_PASS SPF: sender matches SPF record
0.4 RDNS_DYNAMIC Delivered to internal network by host with
dynamic-looking rDNS
0.5 FROM_SUSPICIOUS_NTLD From abused NTLD
1.0 BULK_RE_SUSP_NTLD Precedence bulk and RE: from a suspicious TLD
-1.0 MAILING_LIST_MULTI Multiple indicators imply a widely-seen list
manager
On Mon, May 03 2021, raingloom wrote:
> On Fri, 30 Apr 2021 10:24:42 +0200
> Xinglu Chen <public@HIDDEN> wrote:
>
>> On Thu, Apr 29 2021, raingloom wrote:
>>=20
>> > Here is the updated patch. No idea if this actually works cross
>> > compiled, but I don't have much time to test it. My suspicion is
>> > that it's likely broken and requires changes to Idris 2's code
>> > generators, because they almost definitely call Chez, GCC, etc,
>> > with the wrong arguments.=20=20
>>=20
>> I noticed that there is an =E2=80=98idris2_app=E2=80=99 directory in the=
=E2=80=98bin=E2=80=99
>> directory
>>=20
>> $ ls /gnu/store/va62hzp46c3dp2vlcnqc7fg109axj8rq-idris2-0.3.0/bin
>> idris2* idris2_app/
>>=20
>> What is this used for?
>
> If you take a look at $(guix build idris2)/bin/idris2, it's actually
> just a wrapper. It contains the supporting dynamically linked shared
> objects and the executable itself.
>
> I don't know the details of what each file does or why it's like this,
> the codegen seems to use a similar structure for all backends. The
> scheme files are probably all for the Chez backend, the shared objects
> are either C libraries (for socket support and stuff), or compiled Chez
> code. I just noticed the Racket script, that I have no idea about.
>
> Idris 2's build system makes some... uhm... interesting choices, so
> it's entirely possible that not all of those are necessary, or could be
> moved somewhere more sensible.
Looking at the Nix package, they remove the wrapper and instead move
bin/idris2_app/idris2.so to bin/idris2 and wraps that executable[1].
Perhaps we could do the same thing? I am not familiar with Idris,
though.
[1]: https://github.com/nixos/nixpkgs/blob//pkgs/development/compilers/idri=
s2/default.nix#L41
X-Loop: help-debbugs@HIDDEN
Subject: [bug#46124] [PATCH] Idris 2
Resent-From: raingloom <raingloom@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Wed, 12 May 2021 14:54:01 +0000
Resent-Message-ID: <handler.46124.B46124.16208311948870 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: followup 46124
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: Xinglu Chen <public@HIDDEN>
Cc: Maxime Devos <maximedevos@HIDDEN>, 46124 <at> debbugs.gnu.org
Received: via spool by 46124-submit <at> debbugs.gnu.org id=B46124.16208311948870
(code B ref 46124); Wed, 12 May 2021 14:54:01 +0000
Received: (at 46124) by debbugs.gnu.org; 12 May 2021 14:53:14 +0000
Received: from localhost ([127.0.0.1]:40042 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1lgqEb-0002J0-Nj
for submit <at> debbugs.gnu.org; Wed, 12 May 2021 10:53:13 -0400
Received: from mx1.riseup.net ([198.252.153.129]:37056)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <raingloom@HIDDEN>) id 1lgqEZ-0002Il-9M
for 46124 <at> debbugs.gnu.org; Wed, 12 May 2021 10:53:13 -0400
Received: from fews1.riseup.net (fews1-pn.riseup.net [10.0.1.83])
(using TLSv1 with cipher ECDHE-RSA-AES256-SHA (256/256 bits))
(Client CN "*.riseup.net",
Issuer "Sectigo RSA Domain Validation Secure Server CA" (not verified))
by mx1.riseup.net (Postfix) with ESMTPS id 4FgHpT4m5VzF24f;
Wed, 12 May 2021 07:53:05 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=riseup.net; s=squak;
t=1620831185; bh=KwjS3xLJujLLGLf/4PiCf504b242XAGZubNshuhA/Ck=;
h=Date:From:To:Cc:Subject:In-Reply-To:References:From;
b=pMiKYbgMS6zpWcvMUZyl3cbXDYC5F80NavP418bcKLEmx6eFbwKwqdpFeaprdmItQ
eUZMtpm5gYkNlULrY2evJ/CkfdArF8h1PxMjzBV1AChCYAhCoWZesUmQ4ZKp96vbDg
LoiwasTl60KYe44lPOkL/K6MLMblnAH97fJ/h1fI=
X-Riseup-User-ID: F833FE360E2DD37859E1CAF8B482937B694DAEE1B8894AF35D7DBFEA25DCF19B
Received: from [127.0.0.1] (localhost [127.0.0.1])
by fews1.riseup.net (Postfix) with ESMTPSA id 4FgHpS4Vcsz5vcH;
Wed, 12 May 2021 07:53:04 -0700 (PDT)
Date: Tue, 11 May 2021 23:47:34 +0200
From: raingloom <raingloom@HIDDEN>
Message-ID: <20210511234734.5cf190af@HIDDEN>
In-Reply-To: <87mttae83x.fsf@HIDDEN>
References: <20210127064337.6a226301@HIDDEN> <87r1j267c6.fsf@HIDDEN>
<20210426172240.683c4c2b@HIDDEN>
<5003aa160dc82b35b06e60d425a09309199e1670.camel@HIDDEN>
<20210429204317.7e3a707c@HIDDEN> <87im44nprp.fsf@HIDDEN>
<20210503041044.13358182@HIDDEN> <87mttae83x.fsf@HIDDEN>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
X-Spam-Score: 2.1 (++)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
has NOT identified this incoming email as spam. The original
message has been attached to this so you can view it or label
similar future email. If you have any questions, see
the administrator of that system for details.
Content preview: On Tue,
04 May 2021 19:12:18 +0200 Xinglu Chen <public@HIDDEN>
wrote: > On Mon, May 03 2021, raingloom wrote: > > > On Fri, 30 Apr 2021
10:24:42 +0200 > > Xinglu Chen <public@HIDDEN> wrote: > > > >> On Thu,
Apr 29 2021, raingloom wrote: > >> > >> > Here is the up [...]
Content analysis details: (2.1 points, 10.0 required)
pts rule name description
---- ---------------------- --------------------------------------------------
0.8 DATE_IN_PAST_12_24 Date: is 12 to 24 hours before Received: date
2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs
[URI: yoctocell.xyz (xyz)]
-0.0 SPF_PASS SPF: sender matches SPF record
-0.0 SPF_HELO_PASS SPF: HELO matches SPF record
-0.7 RCVD_IN_DNSWL_LOW RBL: Sender listed at https://www.dnswl.org/,
low trust [198.252.153.129 listed in list.dnswl.org]
0.0 RCVD_IN_MSPIKE_H3 RBL: Good reputation (+3)
[198.252.153.129 listed in wl.mailspike.net]
0.0 RCVD_IN_MSPIKE_WL Mailspike good senders
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: 1.1 (+)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
has NOT identified this incoming email as spam. The original
message has been attached to this so you can view it or label
similar future email. If you have any questions, see
the administrator of that system for details.
Content preview: On Tue, 04 May 2021 19:12:18 +0200 Xinglu Chen <public@HIDDEN>
wrote: > On Mon, May 03 2021, raingloom wrote: > > > On Fri, 30 Apr 2021
10:24:42 +0200 > > Xinglu Chen <public@HIDDEN> wrote: > > > >> On Thu,
Apr 29 2021, raingloom wrote: > >> > >> > Here is the up [...]
Content analysis details: (1.1 points, 10.0 required)
pts rule name description
---- ---------------------- --------------------------------------------------
-0.7 RCVD_IN_DNSWL_LOW RBL: Sender listed at https://www.dnswl.org/,
low trust
[198.252.153.129 listed in list.dnswl.org]
0.0 RCVD_IN_MSPIKE_H3 RBL: Good reputation (+3)
[198.252.153.129 listed in wl.mailspike.net]
0.8 DATE_IN_PAST_12_24 Date: is 12 to 24 hours before Received: date
2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs
[URI: yoctocell.xyz (xyz)]
-0.0 SPF_PASS SPF: sender matches SPF record
-0.0 SPF_HELO_PASS SPF: HELO matches SPF record
0.0 RCVD_IN_MSPIKE_WL Mailspike good senders
-1.0 MAILING_LIST_MULTI Multiple indicators imply a widely-seen list
manager
On Tue, 04 May 2021 19:12:18 +0200
Xinglu Chen <public@HIDDEN> wrote:
> On Mon, May 03 2021, raingloom wrote:
>=20
> > On Fri, 30 Apr 2021 10:24:42 +0200
> > Xinglu Chen <public@HIDDEN> wrote:
> > =20
> >> On Thu, Apr 29 2021, raingloom wrote:
> >> =20
> >> > Here is the updated patch. No idea if this actually works cross
> >> > compiled, but I don't have much time to test it. My suspicion is
> >> > that it's likely broken and requires changes to Idris 2's code
> >> > generators, because they almost definitely call Chez, GCC, etc,
> >> > with the wrong arguments. =20
> >>=20
> >> I noticed that there is an =E2=80=98idris2_app=E2=80=99 directory in t=
he =E2=80=98bin=E2=80=99
> >> directory
> >>=20
> >> $ ls /gnu/store/va62hzp46c3dp2vlcnqc7fg109axj8rq-idris2-0.3.0/bin
> >> idris2* idris2_app/
> >>=20
> >> What is this used for? =20
> >
> > If you take a look at $(guix build idris2)/bin/idris2, it's actually
> > just a wrapper. It contains the supporting dynamically linked shared
> > objects and the executable itself.
> >
> > I don't know the details of what each file does or why it's like
> > this, the codegen seems to use a similar structure for all
> > backends. The scheme files are probably all for the Chez backend,
> > the shared objects are either C libraries (for socket support and
> > stuff), or compiled Chez code. I just noticed the Racket script,
> > that I have no idea about.
> >
> > Idris 2's build system makes some... uhm... interesting choices, so
> > it's entirely possible that not all of those are necessary, or
> > could be moved somewhere more sensible. =20
>=20
> Looking at the Nix package, they remove the wrapper and instead move
> bin/idris2_app/idris2.so to bin/idris2 and wraps that executable[1].
> Perhaps we could do the same thing? I am not familiar with Idris,
> though.
>=20
> [1]:
> https://github.com/nixos/nixpkgs/blob//pkgs/development/compilers/idris2/=
default.nix#L41
That link doesn't work.
I have some more pressing projects to work on, but I'll look into it.
X-Loop: help-debbugs@HIDDEN
Subject: [bug#46124] [PATCH] Idris 2
Resent-From: Xinglu Chen <public@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Fri, 14 May 2021 12:09:02 +0000
Resent-Message-ID: <handler.46124.B46124.162099412416618 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: followup 46124
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: raingloom <raingloom@HIDDEN>
Cc: Maxime Devos <maximedevos@HIDDEN>, 46124 <at> debbugs.gnu.org
Received: via spool by 46124-submit <at> debbugs.gnu.org id=B46124.162099412416618
(code B ref 46124); Fri, 14 May 2021 12:09:02 +0000
Received: (at 46124) by debbugs.gnu.org; 14 May 2021 12:08:44 +0000
Received: from localhost ([127.0.0.1]:45228 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1lhWcW-0004Jy-69
for submit <at> debbugs.gnu.org; Fri, 14 May 2021 08:08:44 -0400
Received: from h87-96-130-155.cust.a3fiber.se ([87.96.130.155]:33804
helo=mail.yoctocell.xyz) by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <public@HIDDEN>) id 1lhWcU-0004Jd-B5
for 46124 <at> debbugs.gnu.org; Fri, 14 May 2021 08:08:43 -0400
From: Xinglu Chen <public@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=yoctocell.xyz;
s=mail; t=1620994114;
bh=dhZmUesfwQf7d8SOkpHCERxwBqRNtNJYDTp4MgcJNXE=;
h=From:To:Cc:Subject:In-Reply-To:References:Date;
b=KsLSQ5pW3mxw4//cMtrCybPw9wIb1nZLJmPVIJMg2YG3PnrkzinzzS4dJXiGKRF1s
oPJWvV7t5JuXNZi+cnRnlymyylgIoB59R2IwS1Dyxn0sO7AAqL59uFUpcyX74AFsaq
fGlBDjHlJx7zTX+Liimz6ll09TxT3HgKlVAWPk+E=
In-Reply-To: <20210511234734.5cf190af@HIDDEN>
References: <20210127064337.6a226301@HIDDEN>
<87r1j267c6.fsf@HIDDEN> <20210426172240.683c4c2b@HIDDEN>
<5003aa160dc82b35b06e60d425a09309199e1670.camel@HIDDEN>
<20210429204317.7e3a707c@HIDDEN> <87im44nprp.fsf@HIDDEN>
<20210503041044.13358182@HIDDEN> <87mttae83x.fsf@HIDDEN>
<20210511234734.5cf190af@HIDDEN>
Date: Fri, 14 May 2021 14:08:33 +0200
Message-ID: <87o8ddjz5q.fsf@HIDDEN>
MIME-Version: 1.0
Content-Type: multipart/signed; boundary="=-=-=";
micalg=pgp-sha256; protocol="application/pgp-signature"
X-Spam-Score: 2.9 (++)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
has NOT identified this incoming email as spam. The original
message has been attached to this so you can view it or label
similar future email. If you have any questions, see
the administrator of that system for details.
Content preview: On Tue, May 11 2021,
raingloom wrote: >> >> [1]: >>
https://github.com/nixos/nixpkgs/blob//pkgs/development/compilers/idris2/default.nix#L41
> > That link doesn't work. Sorry, this one should work
Content analysis details: (2.9 points, 10.0 required)
pts rule name description
---- ---------------------- --------------------------------------------------
2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs
[URI: yoctocell.xyz (xyz)]
0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record
-0.0 SPF_PASS SPF: sender matches SPF record
0.5 FROM_SUSPICIOUS_NTLD From abused NTLD
0.4 RDNS_DYNAMIC Delivered to internal network by host with
dynamic-looking rDNS
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: 2.9 (++)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
has NOT identified this incoming email as spam. The original
message has been attached to this so you can view it or label
similar future email. If you have any questions, see
the administrator of that system for details.
Content preview: On Tue, May 11 2021, raingloom wrote: >> >> [1]: >> https://github.com/nixos/nixpkgs/blob//pkgs/development/compilers/idris2/default.nix#L41
> > That link doesn't work. Sorry, this one should work
Content analysis details: (2.9 points, 10.0 required)
pts rule name description
---- ---------------------- --------------------------------------------------
2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs
[URI: yoctocell.xyz (xyz)]
0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record
-0.0 SPF_PASS SPF: sender matches SPF record
0.5 FROM_SUSPICIOUS_NTLD From abused NTLD
1.0 BULK_RE_SUSP_NTLD Precedence bulk and RE: from a suspicious TLD
0.4 RDNS_DYNAMIC Delivered to internal network by host with
dynamic-looking rDNS
-1.0 MAILING_LIST_MULTI Multiple indicators imply a widely-seen list
manager
--=-=-=
Content-Type: text/plain
Content-Transfer-Encoding: quoted-printable
On Tue, May 11 2021, raingloom wrote:
>>=20
>> [1]:
>> https://github.com/nixos/nixpkgs/blob//pkgs/development/compilers/idris2=
/default.nix#L41
>
> That link doesn't work.
Sorry, this one should work=20
https://github.com/NixOS/nixpkgs/blob/8284fc30c84ea47e63209d1a892aca1dfcd=
6bdf3/pkgs/development/compilers/idris2/default.nix#L35
=20=20
--=-=-=
Content-Type: application/pgp-signature; name="signature.asc"
-----BEGIN PGP SIGNATURE-----
iQJJBAEBCAAzFiEEAVhh4yyK5+SEykIzrPUJmaL7XHkFAmCeaEEVHHB1YmxpY0B5
b2N0b2NlbGwueHl6AAoJEKz1CZmi+1x5w44P/AoVY/C8RAX8irx/ugyxu2tQcYwt
QZdVOsZG4Ek/v0ooT3FX9kkvwZ99MF4RuIv20P/02bnkreylC+yhsa8scF4yDXvh
TeY4X/OIzH7ge0FTe1I7XBCO/5acQ4ZTznIBE4/1VmYXOyikmTd5tpRYfrANFB8k
5oadiNNXddsUZ3YpQc30/83svrcPJ78dqAQATFQO05MahY/CV/XY7XPZKDhd830R
vsfo9M8xloJ3olqt6cazPbYiOdZNKtWYuJ4nEgNbYOPQztn/BC2umKP3aKPQy16p
bHqi1GBXj0GmBZk+G5zdW5MeSFGbD+xQQGteozRkcj63EWWKLjRaBzemyXBJ5RAq
hFE+FAeZBOpZmagwEx9ns5PYzLKblVFZGafGnSmX37WxhRQN7e5IdBaGTphxIS0b
+/rzoS+VT2VI27ivH/9oICzLcvv9l6ao7Gydb/3y3BCrxuPObR1LFs5i5Pl6Xejq
OjBuSH1eiM2ExMlBO0z94puM6Mb0JbOQh/MzRKfDyGx+u6eYnU8IMQTJaXaLprtd
/xcDGw0Z/G1dtM0VyAdwVbj9YplxdCJUGZOJwhF/SqOGS865HsaiOAkHOrcm3Fs0
6cCwiwLNKW6MMMpi3WWWq3lxqgpxidJ237oIU47F6Z5dPV+8fDYyNr5KjJjS8AGE
J5WkuJQKduZEmK+F
=ZkQf
-----END PGP SIGNATURE-----
--=-=-=--
Received: (at control) by debbugs.gnu.org; 11 May 2022 12:58:57 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed May 11 08:58:57 2022
Received: from localhost ([127.0.0.1]:36455 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1nolvd-0007PS-OF
for submit <at> debbugs.gnu.org; Wed, 11 May 2022 08:58:57 -0400
Received: from tobias.gr ([80.241.217.52]:41808)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <me@HIDDEN>) id 1nolva-0007PH-IT
for control <at> debbugs.gnu.org; Wed, 11 May 2022 08:58:56 -0400
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; s=2018; bh=SOHFqrqMElkT0
3BNSM5gSd/T5AmMJb+j4Rb+G6P8ZPE=; h=to:from:date; d=tobias.gr;
b=aFa4cr
JKNfAsHcyl5k3QTtKmXZ2j9V3F6m6lc4P1TyJSxSWY2xHvIjqR0wwKg+LLtadHWbI3ZEfW
suDLip4xED4a8T1arpbuccV181om+NZNNJvA4WoUsB/Upl6Lhw2sJzzNqnSokQI1aAyigT
uquwwf66WwLCIS0KMfiwb7SEBm7og9+HwrcRaJuJKqLXEIpERL95G4IdE1UglscYCTpOWW
Mf87jVkQxu9ju7J9wh09k6hwEbELBl9vcwXJ7mhC8Ql1XdrwUGCIvQXRVz9HUyA6Ubc2E+
FEXHYy69FZbQHn8z1oY90KRTFD9pPlc4QKWHRQfDvIx2T+KKD8Dvo4Sw==
Received: by submission.tobias.gr (OpenSMTPD) with ESMTP id b126e7a8
for <control <at> debbugs.gnu.org>; Wed, 11 May 2022 12:58:48 +0000 (UTC)
MIME-Version: 1.0
Date: Wed, 11 May 2022 14:58:48 +0200
From: Tobias Geerinckx-Rice <me@HIDDEN>
To: control <at> debbugs.gnu.org
Message-ID: <63d7377afc5e206fc2485052563cb927@HIDDEN>
Content-Type: text/plain; charset=US-ASCII;
format=flowed
Content-Transfer-Encoding: 7bit
X-Spam-Score: 3.7 (+++)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
has NOT identified this incoming email as spam. The original
message has been attached to this so you can view it or label
similar future email. If you have any questions, see
the administrator of that system for details.
Content preview: merge 49607 46124
Content analysis details: (3.7 points, 10.0 required)
pts rule name description
---- ---------------------- --------------------------------------------------
-0.0 SPF_HELO_PASS SPF: HELO matches SPF record
-0.0 SPF_PASS SPF: sender matches SPF record
1.8 MISSING_SUBJECT Missing Subject: header
0.2 NO_SUBJECT Extra score for no subject
-0.0 T_SCC_BODY_TEXT_LINE No description available.
1.7 BODY_EMPTY No body text in message
X-Debbugs-Envelope-To: control
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: 2.7 (++)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
has NOT identified this incoming email as spam. The original
message has been attached to this so you can view it or label
similar future email. If you have any questions, see
the administrator of that system for details.
Content preview: merge 49607 46124
Content analysis details: (2.7 points, 10.0 required)
pts rule name description
---- ---------------------- --------------------------------------------------
-0.0 SPF_HELO_PASS SPF: HELO matches SPF record
-0.0 SPF_PASS SPF: sender matches SPF record
1.8 MISSING_SUBJECT Missing Subject: header
0.2 NO_SUBJECT Extra score for no subject
-0.0 T_SCC_BODY_TEXT_LINE No description available.
-1.0 MAILING_LIST_MULTI Multiple indicators imply a widely-seen list
manager
1.7 BODY_EMPTY No body text in message
merge 49607 46124
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997 nCipher Corporation Ltd,
1994-97 Ian Jackson.