From patchwork Thu Apr 29 18:43:17 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Csepp X-Patchwork-Id: 28990 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 8168927BC7D; Fri, 30 Apr 2021 00:21:37 +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 EE34A27BC7C for ; Fri, 30 Apr 2021 00:21:36 +0100 (BST) Received: from localhost ([::1]:60116 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1lcFyS-00062G-1x for patchwork@mira.cbaines.net; Thu, 29 Apr 2021 19:21:36 -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 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 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. 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