From patchwork Mon Apr 26 15:22:40 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Csepp X-Patchwork-Id: 28924 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 4549827BC7D; Mon, 26 Apr 2021 21:47:51 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-2.9 required=5.0 tests=BAYES_00,MAILING_LIST_MULTI, RCVD_IN_MSPIKE_H4,RCVD_IN_MSPIKE_WL,SPF_HELO_PASS,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.2 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id D251C27BC7C for ; Mon, 26 Apr 2021 21:47:50 +0100 (BST) Received: from localhost ([::1]:39730 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1lb890-0003Pz-1w for patchwork@mira.cbaines.net; Mon, 26 Apr 2021 16:47:50 -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 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+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches 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. 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