From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp2 ([2001:41d0:8:6d80::]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) by ms0.migadu.com with LMTPS id uHfaLG8/i2CCygAAgWs5BA (envelope-from ) for ; Fri, 30 Apr 2021 01:21:19 +0200 Received: from aspmx1.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp2 with LMTPS id M/plKG8/i2AIXwAAB5/wlQ (envelope-from ) for ; Thu, 29 Apr 2021 23:21:19 +0000 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id 244D815B20 for ; Fri, 30 Apr 2021 01:21:19 +0200 (CEST) Received: from localhost ([::1]:60116 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1lcFyA-00062G-BI for larch@yhetil.org; Thu, 29 Apr 2021 19:21:18 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:47164) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1lcFxv-00060o-Ts for guix-patches@gnu.org; Thu, 29 Apr 2021 19:21:05 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:45521) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1lcFxu-0001LW-FG for guix-patches@gnu.org; Thu, 29 Apr 2021 19:21:03 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1lcFxu-000729-Al for guix-patches@gnu.org; Thu, 29 Apr 2021 19:21:02 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#46124] [PATCH] Idris 2 Resent-From: raingloom Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Thu, 29 Apr 2021 23:21:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 46124 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Maxime Devos Cc: Xinglu Chen , 46124@debbugs.gnu.org Received: via spool by 46124-submit@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 ) id 1lcFxn-00071H-Tc for submit@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 ) id 1lcFxi-00070o-8d for 46124@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 Message-ID: <20210429204317.7e3a707c@riseup.net> In-Reply-To: <5003aa160dc82b35b06e60d425a09309199e1670.camel@telenet.be> References: <20210127064337.6a226301@riseup.net> <87r1j267c6.fsf@yoctocell.xyz> <20210426172240.683c4c2b@riseup.net> <5003aa160dc82b35b06e60d425a09309199e1670.camel@telenet.be> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="MP_/X7RxX_rpJMU.w8Ngt.a7fAX" X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org Sender: "Guix-patches" X-Migadu-Flow: FLOW_IN ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1619738479; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:cc:mime-version:mime-version: content-type:content-type:resent-cc:resent-from:resent-sender: resent-message-id:in-reply-to:in-reply-to:references:references: list-id:list-help:list-unsubscribe:list-subscribe:list-post; bh=aY8+exXLrXdsFjoAX5EkdoU6dkHqayN6CXo/fdDAcJ8=; b=TnbX+qOUkDXElZsEi1cFCJpAuE1VH87li4ENoOws56DHxwzh6tl6ZEJ1C6GzAL3rLYqavM WR1dhzXgYhhnHeKyvIjtkvVJBrf2ox4bd6DmjYvo5yUFFAO9xOEvzJ0gcvyIvScuNvHJu3 r7cbyW1Jqb8pDy9pi02p/BFrnOFbnwdckEs3rR0U2+Pn35/t56zNm2fKsCFcjya2SblBXm 88Ax0eaybQ5IlnKXyjMf9bwb+LtDwVNR1LdXarFWxGa9e2gfx3CdODssOpejKd6xVUHaPP qMhLmsX60Osn2rPBWVnZ1GA3c7bH9V7SesRpv4EUzH5XGEKtN6epM1X6kpqSfQ== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1619738479; a=rsa-sha256; cv=none; b=NorhG0dI93GuZx3Q1xyte0247YuN3Dez0Sn0eUYi5BqGWw10fNpBj8tB2HldCxtY2IaUV7 RASzpYKJhFAJeUdCUx3WFIsaIKQNOpvzEBtKLaYmKFbAfT7R1Dv5YTy6BD4q9Gy9GyeJ4F /YrQnlUzpI0t6Fx/p7m9k+Wc4Vr0ijbmfu2asYVirboVA3MboQ29u98vMCj9zogYbPOkWZ KmQ6eYVKN0kBUqlJkURcbb9rYkzIKHLB8RarDhg8rvaCQhqAwlT6cYwhhN7+mamH5ALv9q SstNmcZqfagZtVQt1lO6MgC1eZ7Xhtb4fkHXjqnjscNCbd1mIikolS/0rIcEAQ== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=none; dmarc=fail reason="SPF not aligned (relaxed), No valid DKIM" header.from=riseup.net (policy=none); spf=pass (aspmx1.migadu.com: domain of guix-patches-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=guix-patches-bounces@gnu.org X-Migadu-Spam-Score: -2.36 Authentication-Results: aspmx1.migadu.com; dkim=none; dmarc=fail reason="SPF not aligned (relaxed), No valid DKIM" header.from=riseup.net (policy=none); spf=pass (aspmx1.migadu.com: domain of guix-patches-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=guix-patches-bounces@gnu.org X-Migadu-Queue-Id: 244D815B20 X-Spam-Score: -2.36 X-Migadu-Scanner: scn0.migadu.com X-TUID: Wi+9qtQLfHux --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 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 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--