From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp0 ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms0.migadu.com with LMTPS id kPG9KQOYXGE1zgAAgWs5BA (envelope-from ) for ; Tue, 05 Oct 2021 20:22:59 +0200 Received: from aspmx1.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp0 with LMTPS id MOJyJQOYXGHmQAAA1q6Kng (envelope-from ) for ; Tue, 05 Oct 2021 18:22:59 +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 549CE26BCD for ; Tue, 5 Oct 2021 20:22:59 +0200 (CEST) Received: from localhost ([::1]:52638 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1mXp5e-0001Wi-Ca for larch@yhetil.org; Tue, 05 Oct 2021 14:22:58 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:46236) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1mXnbm-0005IJ-Tq for guix-patches@gnu.org; Tue, 05 Oct 2021 12:48:06 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:58433) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1mXnbm-0006VK-4D for guix-patches@gnu.org; Tue, 05 Oct 2021 12:48:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1mXnbm-00020x-38 for guix-patches@gnu.org; Tue, 05 Oct 2021 12:48:02 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#49607] [PATCH 3/3] gnu: idris: Add idris2 0.5.1, and 1.3.3-1.5545986. Resent-From: Attila Lendvai Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Tue, 05 Oct 2021 16:48:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 49607 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 49607@debbugs.gnu.org Cc: Attila Lendvai Received: via spool by 49607-submit@debbugs.gnu.org id=B49607.16334524797726 (code B ref 49607); Tue, 05 Oct 2021 16:48:02 +0000 Received: (at 49607) by debbugs.gnu.org; 5 Oct 2021 16:47:59 +0000 Received: from localhost ([127.0.0.1]:41745 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mXnbi-00020X-E1 for submit@debbugs.gnu.org; Tue, 05 Oct 2021 12:47:58 -0400 Received: from mail-ed1-f46.google.com ([209.85.208.46]:35378) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mXnbc-0001zx-Cb for 49607@debbugs.gnu.org; Tue, 05 Oct 2021 12:47:56 -0400 Received: by mail-ed1-f46.google.com with SMTP id b8so1259276edk.2 for <49607@debbugs.gnu.org>; Tue, 05 Oct 2021 09:47:52 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=sender:from:to:cc:subject:date:message-id:in-reply-to:references :mime-version:content-transfer-encoding; bh=3iHNUeVDPh33Vb+Y9J04Uen/qwU4czBRZ9FMfloTa50=; b=bIc+xH2plV/N7wwJPBgC88HUUzOBHOl2+mhnclwunhTSNXPpopGuZdI739xKvda0pi CKcyUuJfGVlaF5KUDW7zfeQ6R65ehN5+A/B2esPnuAeW1Qj7XjScKVWB0x8geZnz2t4k ihgJTOWC5QZsfwJ6M+rEELK+dL6fFoTDr/evo37MkpecJZjQzZ67+pNRk8uA41h7DvoD +JjbDn+pEwj15ifYawtO6/baVNVmO6fPSdzUa2Ol1rXAMdgIaxQ0xhZZlX/M+8cDXBo7 poxcBBMdQ+hcPYTshGiK2dQwD8vhUT5jHAmwIuuG2nXXf0OU+le1TJpiPSoXVqug+Cm2 SXjA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:sender:from:to:cc:subject:date:message-id :in-reply-to:references:mime-version:content-transfer-encoding; bh=3iHNUeVDPh33Vb+Y9J04Uen/qwU4czBRZ9FMfloTa50=; b=XZh+fD2nZX16dbDlLFC79Fy2d24mAv6R1sk1hVd+m926G30FIYxIUK1DYHHOUgEXt9 SmlahbREQiMM0n0Qf8mP7lc/HXULfrt9zT4JQNI6VyluKSApprSCJ9xXFzsN3m6SnvlM YeqRvUas5/YYQgXwk/X0EMphR1Uft/TAFZLpHzMeJgJKPYUGYT96wo7DopDtNlPMPBHF 3KnNR6Jcsk5sPHiDLXIyX2zT00gdeGOZpX76XZGijEcIOQi5hpaooT87hudIT3q/TVLQ 7UVW+2XX+U2EtmHCEzS27SLza2dkTOsL+Vr5tJocpI/OHQvlp5aIM/g6jrT/CJutlE+N tjkg== X-Gm-Message-State: AOAM533BknAKPI6bAnpbPWA0JwbWz7qqIJPo5yT0IBsVtJKzQD7sdaR3 7Urqh/eYL8vmz4qljCcnIUJ92ssIav8= X-Google-Smtp-Source: ABdhPJzjqIxrEzi49YptjrbxDCDhFcVxKGmoQx0T0Pvoo982tGfi1BzKlYiqiqcnlp1gUGeiOPy+Ug== X-Received: by 2002:a17:907:9604:: with SMTP id gb4mr26423866ejc.142.1633452466496; Tue, 05 Oct 2021 09:47:46 -0700 (PDT) Received: from lelap.lan (catv-213-222-131-28.catv.broadband.hu. [213.222.131.28]) by smtp.gmail.com with ESMTPSA id n6sm8999335eds.10.2021.10.05.09.47.45 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 05 Oct 2021 09:47:46 -0700 (PDT) From: Attila Lendvai Date: Tue, 5 Oct 2021 18:37:58 +0200 Message-Id: <20211005163757.29637-3-attila@lendvai.name> X-Mailer: git-send-email 2.33.0 In-Reply-To: <20211005163757.29637-1-attila@lendvai.name> References: <20211005163757.29637-1-attila@lendvai.name> MIME-Version: 1.0 Content-Transfer-Encoding: 8bit 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=1633458179; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: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:dkim-signature; bh=3iHNUeVDPh33Vb+Y9J04Uen/qwU4czBRZ9FMfloTa50=; b=VFQ9JZ6magrpHPWGfjaRA8Fl2PuvskWrnTbe4nZdNPFg1RFh5hfKz5qIDHwr+62idDr3AI LyUOD3GSM7oxGp4bfYLXPwC1oGicKepTsMOpAdpY5Ntlk2L1NzPGT9nI/LUAmHZsZL+fBv yEbWUYF6ZdkSAflZaLBVELXtfbpM2vUMWQUbh3ipI26uHUueKf3l7dctGKUQvRISMlq+oo FeymjWUaw2K3MnwIN6Cl2w5/94QIi5UlQ4ofoW6428M6PQfLRjI5/PwOli0vKoZAPB/Gmm DDFLTSGUPqd2vtyOSiwWdeptbFuFxIuFOIRz7oamqtlbNK7i6ipf+yOkISrV4Q== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1633458179; a=rsa-sha256; cv=none; b=nUU2PG8raS5fA/6KgO8070J7vyUBRTOVNqchqwd7LxL4+x1/k9Hnb2jzwnX6Z8Hx9khWSY arsEdLWJDdqfxb4h8eSYXsEBHca26rNgRb4AghhowKgRxKdezZbrA3rue5vXJMtv4gAH3M 3u3V4Pujza5Y6hJiUaOLixvkG5x98l7s8KMQo6oGr5KJTaka/AY1GkcxqRjfsgmwYa45hQ NA/iyq/Op7nKY3WSC+lX64EbNEOu6gFQu+4CpjpPHjltg/a3NVf/qw5gI7OdoyeA8xcbGB AbikSSMniRB7GOf2LbBErC5dwHmuCuTKek4YhxSgUWmUuHq5cM6xM9ieyOuYhg== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=gmail.com header.s=20210112 header.b=bIc+xH2p; 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: 3.59 Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=gmail.com header.s=20210112 header.b=bIc+xH2p; dmarc=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: 549CE26BCD X-Spam-Score: 3.59 X-Migadu-Scanner: scn0.migadu.com X-TUID: k8MqX8+nFSzi This generality is there because with this it is possible to bootstrap Idris HEAD all the way down from GHC. It requires patching past releases, which requires importing them into separate git branches. This has not been merged into upstream yet, therefore this commit only contains a single use of MAKE-IDRIS-PACKAGE, but that will change in the future. Add a symlink to a versioned binary; e.g. add a `bin/idris-1.3.3`. * gnu/packages/idris.scm (idris-1.3.3-1): New variable, the latest git commit from the v1.x line of Idris. (make-idris-package): New function to instantiate a package of Idris2. (idris2-0.5.1): New variable. --- gnu/packages/idris.scm | 182 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 179 insertions(+), 3 deletions(-) diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm index 1f6e984a90..4ef18c6da4 100644 --- a/gnu/packages/idris.scm +++ b/gnu/packages/idris.scm @@ -19,9 +19,22 @@ ;;; You should have received a copy of the GNU General Public License ;;; along with GNU Guix. If not, see . +;;; TODO +;;; +;;; - Idris has multiple backends, but we only register Chez as an +;;; input. Decide how to make backends optional, and/or which ones to package +;;; by default. +;;; +;;; - Set RUNPATH instead of using LD_LIBRARY_PATH. See +;;; http://blog.tremily.us/posts/rpath/ This needs patching Idris so that it +;;; stops using a wrapper script and finds its libidris_support.so +;;; e.g. relative to the executable. + (define-module (gnu packages idris) #:use-module (gnu packages) + #:use-module (gnu packages base) #: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) @@ -29,14 +42,21 @@ #:use-module (gnu packages llvm) #:use-module (gnu packages multiprecision) #:use-module (gnu packages ncurses) + #:use-module (gnu packages node) #:use-module (gnu packages perl) + #:use-module (gnu packages racket) + #:use-module (gnu packages version-control) #:use-module (guix build-system gnu) #:use-module (guix build-system haskell) #:use-module (guix download) + #:use-module (guix git) #:use-module (guix git-download) #:use-module ((guix licenses) #:prefix license:) #:use-module (guix packages) - #:use-module (guix utils)) + #:use-module (guix utils) + #:use-module (ice-9 match) + #:use-module (ice-9 regex) + #:export (make-idris-package)) (define-public idris-1.3.3 (package @@ -148,8 +168,10 @@ (let* ((out (assoc-ref outputs "out")) (exe (string-append out "/bin/idris"))) (wrap-program exe - `("IDRIS_CC" = (,',(cc-for-target))))) - #true))))) + `("IDRIS_CC" = (,',(cc-for-target)))) + (with-directory-excursion (string-append out "/bin/") + (symlink ,name (string-append ,name "-" ,version)))) + #t))))) (native-search-paths (list (search-path-specification (variable "IDRIS_LIBRARY_PATH") @@ -165,6 +187,160 @@ Epigram and Agda.") (define-public idris idris-1.3.3) +(define-public idris-1.3.3-1 + ;; This is the current latest from the v1.x branch. + (let ((commit "55459867fc3f1ac34527a5dd998c37e72b15d488") + (revision "1")) + (package + (inherit idris-1.3.3) + (version (git-version "1.3.3" revision commit)) + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/attila-lendvai/Idris2") + (commit commit))) + (sha256 + (base32 + "0qsn1953jy74pgppwkax8yrlswb3v46x541ahbl95rshf666nsj6")) + (file-name (git-file-name "idris" version)))) + (inputs + (append (package-inputs idris-1.3.3) + `(("ghc-haskeline-0.8" ,ghc-haskeline-0.8))))))) + +(define* (make-idris-package source version + #:key bootstrap-idris + (ignore-test-failures? #false) + (unwrap? #true) + (tests? #true) + (files-to-patch-for-shell + '("src/Compiler/Scheme/Chez.idr" + "src/Compiler/Scheme/Racket.idr" + "src/Compiler/Scheme/Gambit.idr" + "src/Compiler/ES/Node.idr" + "bootstrap/idris2_app/idris2.rkt" + "bootstrap/idris2_app/idris2.ss")) + (with-bootstrap-shortcut? #true)) + (package + (name "idris2") + (version version) + (source (match source + ((commit hash . url) + (origin + (method git-fetch) + (uri (git-reference + (url (if (null? url) + "https://github.com/idris-lang/Idris2.git" + (car url))) + (commit commit))) + (sha256 (base32 hash)) + (file-name (git-file-name name version)))) + ((? git-checkout?) + source))) + (build-system gnu-build-system) + (native-inputs + `(,@(if with-bootstrap-shortcut? + `(("chez-scheme" ,chez-scheme)) + `(("bootstrap-idris" ,bootstrap-idris))) + ("cc" ,clang-toolchain-12) ; clang or older clang-toolchain's don't have a bin/cc + ("coreutils" ,coreutils) + ("git" ,git) + ("node" ,node) ; only for the tests + ("racket" ,racket) ; only for the tests + ("sed" ,sed))) + (inputs + `(("bash" ,bash-minimal) + ("chez-scheme" ,chez-scheme) + ("gmp" ,gmp))) + (arguments + `(#:tests? ,tests? + #:make-flags + (list (string-append "CC=" ,(cc-for-target)) + ,@(if with-bootstrap-shortcut? + '((string-append "SCHEME=" + (assoc-ref %build-inputs "chez-scheme") + "/bin/scheme")) + `((string-append "BOOTSTRAP_IDRIS=" + (assoc-ref %build-inputs "bootstrap-idris") + "/bin/" ,(package-name bootstrap-idris)))) + (string-append "PREFIX=" (assoc-ref %outputs "out")) + "-j1") + #:phases + (modify-phases %standard-phases + (delete 'bootstrap) + (delete 'configure) + (delete 'check) ; check must happen after install and wrap-program + (add-after 'unpack 'patch-paths + (lambda* (#:key inputs #:allow-other-keys) + (substitute* ',files-to-patch-for-shell + ((,(regexp-quote "#!/bin/sh")) + (string-append "#!" (assoc-ref inputs "bash") "/bin/sh")) + (("/usr/bin/env") + (string-append (assoc-ref inputs "coreutils") "/bin/env"))) + #true)) + ,@(if unwrap? + `((add-after 'install 'unwrap + (lambda* (#:key outputs #:allow-other-keys) + ;; The bin/idris2 calls bin/idris2_app/idris2.so which is + ;; the real executable, but it sets LD_LIBRARY_PATH + ;; incorrectly. Remove bin/idris2 and replace it with + ;; bin/idris2_app/idris2.so instead. + (let ((out (assoc-ref outputs "out"))) + (delete-file (string-append out "/bin/idris2")) + (rename-file (string-append out "/bin/idris2_app/idris2.so") + (string-append out "/bin/idris2")) + (delete-file-recursively (string-append out "/bin/idris2_app")) + (delete-file-recursively (string-append out "/lib"))) + #true))) + '()) + ,@(if with-bootstrap-shortcut? + `((replace 'build + (lambda* (#:key make-flags #:allow-other-keys) + ;; i.e. do not build it using the previous version of + ;; Idris, but rather compile the comitted compiler + ;; output. + (apply invoke "make" "bootstrap" make-flags)))) + '()) + (add-after 'unwrap 'wrap-program + (lambda* (#:key outputs inputs #:allow-other-keys) + (let* ((chez (string-append (assoc-ref inputs "chez-scheme") + "/bin/scheme")) + (out (assoc-ref outputs "out")) + (exe (string-append out "/bin/" ,name)) + (version ,version)) + (wrap-program exe + `("IDRIS2_PREFIX" = (,out)) + `("LD_LIBRARY_PATH" prefix (,(string-append out "/idris2-" version "/lib"))) + `("CC" = (,',(cc-for-target))) + `("CHEZ" = (,chez))) + (with-directory-excursion (string-append out "/bin/") + (symlink ,name (string-append ,name "-" ,version)))) + #true)) + (add-after 'wrap-program 'check + (lambda* (#:key outputs make-flags #:allow-other-keys) + (,(if ignore-test-failures? + 'false-if-exception + 'begin) + (apply invoke "make" + "INTERACTIVE=" + (string-append "IDRIS2=" + (assoc-ref outputs "out") + "/bin/" ,name) + "test" make-flags)) + #true))))) + (home-page "https://www.idris-lang.org") + (synopsis "General purpose language with full dependent types") + (description "Idris is a general purpose language with full dependent +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. The language is closely related to +Epigram and Agda.") + (license license:bsd-3))) + +(define-public idris2-0.5.1 + (make-idris-package '("v0.5.1" + "09k5fxnplp6fv3877ynz1lwq9zapxcxbvfvkn6g68yb0ivrff978") + "0.5.1")) + ;; 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.33.0