From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp0 ([2001:41d0:2:4a6f::]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) by ms0.migadu.com with LMTPS id 4F+aIPAmh2AplAAAgWs5BA (envelope-from ) for ; Mon, 26 Apr 2021 22:47:44 +0200 Received: from aspmx1.migadu.com ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp0 with LMTPS id II9cHPAmh2BSFwAA1q6Kng (envelope-from ) for ; Mon, 26 Apr 2021 20:47:44 +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 329A0175DA for ; Mon, 26 Apr 2021 22:47:44 +0200 (CEST) Received: from localhost ([::1]:39730 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1lb88t-0003Pz-BF for larch@yhetil.org; Mon, 26 Apr 2021 16:47:43 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:40020) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1lb88F-00032U-L7 for guix-patches@gnu.org; Mon, 26 Apr 2021 16:47:03 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:35791) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1lb88F-0001Aj-Di for guix-patches@gnu.org; Mon, 26 Apr 2021 16:47:03 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1lb88F-0005v6-CG for guix-patches@gnu.org; Mon, 26 Apr 2021 16:47:03 -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: Mon, 26 Apr 2021 20:47:03 +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: Xinglu Chen Cc: 46124@debbugs.gnu.org Received: via spool by 46124-submit@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 ) id 1lb87R-0005tU-QV for submit@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 ) id 1lb87H-0005sC-6i for 46124@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 Message-ID: <20210426172240.683c4c2b@riseup.net> In-Reply-To: <87r1j267c6.fsf@yoctocell.xyz> References: <20210127064337.6a226301@riseup.net> <87r1j267c6.fsf@yoctocell.xyz> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="MP_/=J6D/.pR/cuCeavvn7rp8qV" 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=1619470064; 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=p8QQGYfkCofuLbcj1NCtXcMEiMeipPkMLZZ6wsyEuco=; b=hhG1/Nqy/m9mZPMeU4dChBJpCLZSsNOpwCjC0U7mlD0y8iiLhFWOJ8/9DS6DwKX9In5Swt qyWgfzXbW/LH1qPMe3vCDh8cjlYZJvvHYA2zH+nuISYDHigDamPI2mbxKlavoTcJ9Nwfjl S0oWjqil4jp6oXrVfm8J6JKSXTAkW/4QK3z+fjA79cdrcVLWcwe5iIKAohZOXAJa6wvvDI Ca4lvBO9ufwKe5TZwRIgtOIliuSkKIsTj2M4g2GAcBhKmSs4+O+pQrrV9qDW/8tcKg3yP2 euH5UeWcYIk7nSm8wwCcEbnCoptaufg58G/yw2NU1yWP5vBl4uJa2dOVNlnf5A== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1619470064; a=rsa-sha256; cv=none; b=i02dzPMBAfzPadeXHzWwPBmJAW28LczuZQXxG2+ZtpHE/jQZ51p1t7+6nM4OWc5k969Po0 Bth3wjHHvQtp1tPG1IZ1/hs6IYSDc+xNvBdV1a8NIdzhWZxMkfJZJKvuYw0yluWFFPTbrw Afq/vaqBno2+wyCjATEcDINbGsvoAWcnQnAeoAwpOYYPQ64gYeCqpyzrCUPwlWRbqAfHef F0/M9lZewFnFzB9O9vxHfG2mxWRj2vEEHaT4izLFNLzMZcssTjyJD6DvtZea737YjFJx4+ DDeqqIYSL6+NmXdV3/Az5LOBczK9p663uPk/U6/VmJHBd/2Vj5XE1j9h56yaCA== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=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.35 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: 329A0175DA X-Spam-Score: -2.35 X-Migadu-Scanner: scn0.migadu.com X-TUID: paYAHwxceHLL --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 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 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--