From patchwork Sun Apr 30 10:53:11 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Josselin Poiret X-Patchwork-Id: 49708 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 88DFB27BBEA; Sun, 30 Apr 2023 11:55:30 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,FROM_SUSPICIOUS_NTLD,MAILING_LIST_MULTI,PDS_OTHER_BAD_TLD, RCVD_IN_MSPIKE_H2,SPF_HELO_PASS,URIBL_BLOCKED autolearn=no autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 22B2C27BBE2 for ; Sun, 30 Apr 2023 11:55:30 +0100 (BST) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1pt4gy-0002tR-NA; Sun, 30 Apr 2023 06:54:08 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1pt4gt-0002sT-7v for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:03 -0400 Received: from debbugs.gnu.org ([209.51.188.43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1pt4gs-0002Tt-VX for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1pt4gs-0000VS-Nc for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:02 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#61915] [PATCH v2 01/13] gnu: Add ghc-peano. Resent-From: Josselin Poiret Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 30 Apr 2023 10:54:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 61915 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Received: via spool by 61915-submit@debbugs.gnu.org id=B61915.16828520171784 (code B ref 61915); Sun, 30 Apr 2023 10:54:02 +0000 Received: (at 61915) by debbugs.gnu.org; 30 Apr 2023 10:53:37 +0000 Received: from localhost ([127.0.0.1]:37331 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gS-0000ST-EH for submit@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:36 -0400 Received: from jpoiret.xyz ([206.189.101.64]:52702) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gK-0000RZ-Gv for 61915@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:30 -0400 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id C7A60185317; Sun, 30 Apr 2023 10:53:26 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1682852007; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=1RT2RhT00cUZnzWnxCuJ+iPMmPqdXhYv4GUsMgOGmvg=; b=fd5qjv2dqyXPHmZjQrzZ0Pvc4UkH1ZbOEKixrwMEfUcfLPR8PgSC7mJ9vuQuU0Mh1O9oSl kV41PTFPXXHag81muPWeew4WgsxnXOiPfT3XyWSpYorY+5X9bbtum8Dkb1KfZXENRFAPRZ vkaw6DlzvPjj5WlqsoPB2NNSe5ql/icvg7cKiAy7vB8sTGEachjrisztQSlZBNV2UuTNXi QhGU3cjPviBVCwSmVDOenI61bv5p0K0s4SoSjfjhKslGiL+MOfPZ8I/Grh0enJ4YYL/LSS lq5X6KE16vjXnH2z211oH5j8P54UQT1n9QTpHVBV49sbX8YlSO+de9TP6+70PA== Date: Sun, 30 Apr 2023 12:53:11 +0200 Message-Id: <17476252dbebbd0db027cb941820f2d728eb9d7c.1682851600.git.dev@jpoiret.xyz> In-Reply-To: References: MIME-Version: 1.0 X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz 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: , Reply-to: Josselin Poiret X-ACL-Warn: , Josselin Poiret via Guix-patches X-Patchwork-Original-From: Josselin Poiret via Guix-patches via From: Josselin Poiret Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches From: Josselin Poiret * gnu/packages/haskell-xyz.scm (ghc-peano): New variable. --- gnu/packages/haskell-xyz.scm | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/gnu/packages/haskell-xyz.scm b/gnu/packages/haskell-xyz.scm index a411bfc40a..0c1eb15d79 100644 --- a/gnu/packages/haskell-xyz.scm +++ b/gnu/packages/haskell-xyz.scm @@ -8602,6 +8602,26 @@ (define-public ghc-pcre-light syntax and semantics as Perl 5.") (license license:bsd-3))) +(define-public ghc-peano + (package + (name "ghc-peano") + (version "0.1.0.1") + (source (origin + (method url-fetch) + (uri (hackage-uri "peano" version)) + (sha256 + (base32 + "0yzcxrl41dacvx2wkyxjj7hgvz56l4qb59r4h9rmaqd7jcwx5z9i")))) + (build-system haskell-build-system) + (arguments + `(#:cabal-revision ("3" + "0wl22dnz6ld300cg6id3lw991bp8kdfi8h0nbv37vn79i1zdcj5n"))) + (home-page "http://hackage.haskell.org/package/peano") + (synopsis "Peano numbers") + (description "Provides an efficient Haskell implementation of Peano +numbers") + (license license:bsd-3))) + (define-public ghc-persistent (package (name "ghc-persistent") From patchwork Sun Apr 30 10:53:12 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Josselin Poiret X-Patchwork-Id: 49706 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 F366827BBEC; Sun, 30 Apr 2023 11:55:26 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,FROM_SUSPICIOUS_NTLD,MAILING_LIST_MULTI,PDS_OTHER_BAD_TLD, RCVD_IN_MSPIKE_H2,SPF_HELO_PASS,URIBL_BLOCKED autolearn=no autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 5FC4F27BBEA for ; Sun, 30 Apr 2023 11:55:26 +0100 (BST) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1pt4gy-0002t7-EA; Sun, 30 Apr 2023 06:54:08 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1pt4gs-0002sD-Mq for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:02 -0400 Received: from debbugs.gnu.org ([209.51.188.43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1pt4gs-0002Th-Dp for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1pt4gs-0000VK-AJ for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:02 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#61915] [PATCH v2 02/13] gnu: Add ghc-vector-hashtables. Resent-From: Josselin Poiret Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 30 Apr 2023 10:54:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 61915 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Received: via spool by 61915-submit@debbugs.gnu.org id=B61915.16828520161768 (code B ref 61915); Sun, 30 Apr 2023 10:54:02 +0000 Received: (at 61915) by debbugs.gnu.org; 30 Apr 2023 10:53:36 +0000 Received: from localhost ([127.0.0.1]:37325 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gS-0000SR-2E for submit@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:36 -0400 Received: from jpoiret.xyz ([206.189.101.64]:52790) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gL-0000Rg-N8 for 61915@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:30 -0400 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id A3DBA18531A; Sun, 30 Apr 2023 10:53:28 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1682852009; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=uUBvkhwz2JpAvXLObbdNKiI3umiSK+eBaQ0fwj5lNe0=; b=ftciCpBX9rV0xfX9SZeytuq6NQHC6W7gcxbBOq93G/CNUxaiVq1NGSM8IfQ/aNr3NAeAmY zCvKepuPi2ECTob5YtV5atXaeOhG0u7fQX05Zfw/U/rQ61gxIIIncN5q0nOSSrbmklDNpq 1/x6xjfDTwHBzMwaYAPpKopkh/+PySoTO9EHgm5cRgN7AeQk7/Gjf6OcYLU+OGQRaAP7pA wqT00kVxhL+XITF58Nr/O+gBzNhDjVZjRYsBpx8mlfzz5sGjoVqmTxNWxZkwmgPeRI1TLf +GhVINE+vXMDuDU4jq7iWUxTeaKZGELloJDrtQnF7x/XFSf9bmQlvxVCMpA+FQ== Date: Sun, 30 Apr 2023 12:53:12 +0200 Message-Id: In-Reply-To: References: MIME-Version: 1.0 X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz 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: , Reply-to: Josselin Poiret X-ACL-Warn: , Josselin Poiret via Guix-patches X-Patchwork-Original-From: Josselin Poiret via Guix-patches via From: Josselin Poiret Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches From: Josselin Poiret * gnu/packages/haskell-xyz.scm (ghc-vector-hashtables): New variable. --- gnu/packages/haskell-xyz.scm | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/gnu/packages/haskell-xyz.scm b/gnu/packages/haskell-xyz.scm index 0c1eb15d79..aaa7255956 100644 --- a/gnu/packages/haskell-xyz.scm +++ b/gnu/packages/haskell-xyz.scm @@ -13328,6 +13328,27 @@ (define-public ghc-vector-builder vector.") (license license:expat))) +(define-public ghc-vector-hashtables + (package + (name "ghc-vector-hashtables") + (version "0.1.1.2") + (source (origin + (method url-fetch) + (uri (hackage-uri "vector-hashtables" version)) + (sha256 + (base32 + "0hrjvy9qg1m5g3w91zxy4syqmp8jk7ajjbxbzkhy282dwfigkyd2")))) + (build-system haskell-build-system) + (inputs (list ghc-primitive ghc-vector ghc-hashable)) + (native-inputs (list ghc-hspec ghc-quickcheck ghc-quickcheck-instances + hspec-discover)) + (home-page "https://github.com/klapaucius/vector-hashtables#readme") + (synopsis "Efficient vector-based mutable hashtables implementation") + (description + "This package provides efficient vector-based hashtable implementation +similar to .NET Generic Dictionary implementation (at the time of 2015).") + (license license:bsd-3))) + (define-public ghc-vector-th-unbox (package (name "ghc-vector-th-unbox") From patchwork Sun Apr 30 10:53:13 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Josselin Poiret X-Patchwork-Id: 49704 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 A078B27BBEC; Sun, 30 Apr 2023 11:55:22 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,FROM_SUSPICIOUS_NTLD,MAILING_LIST_MULTI,PDS_OTHER_BAD_TLD, RCVD_IN_MSPIKE_H2,SPF_HELO_PASS,URIBL_BLOCKED autolearn=no autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 4633327BBE2 for ; Sun, 30 Apr 2023 11:55:22 +0100 (BST) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1pt4h1-0002wW-OX; Sun, 30 Apr 2023 06:54:11 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1pt4gu-0002sc-60 for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:04 -0400 Received: from debbugs.gnu.org ([209.51.188.43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1pt4gt-0002U2-CR for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:03 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1pt4gt-0000VZ-8h for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:03 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#61915] [PATCH v2 03/13] gnu: agda: Update to 2.6.3 and switch to git-fetch. Resent-From: Josselin Poiret Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 30 Apr 2023 10:54:03 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 61915 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Received: via spool by 61915-submit@debbugs.gnu.org id=B61915.16828520171796 (code B ref 61915); Sun, 30 Apr 2023 10:54:03 +0000 Received: (at 61915) by debbugs.gnu.org; 30 Apr 2023 10:53:37 +0000 Received: from localhost ([127.0.0.1]:37333 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gT-0000Si-0N for submit@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:37 -0400 Received: from jpoiret.xyz ([206.189.101.64]:52880) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gM-0000Ro-Mh for 61915@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:31 -0400 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id BDC80185309; Sun, 30 Apr 2023 10:53:29 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1682852010; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=1q+YkSPkuAh8v29h6zhDQp6JgBxU3Hz0rXq4KzXUFiI=; b=cZKpPyBm4D5UKsMD2tJTQUnZHr/3e+HyJm+/jKWvMTZe5mL908sUyb+zTYZzXruMn0xECc KEB8Ur8SHOTrqngCgRxdC7+Sy+9s+RiTdJ4lZ4gC8lJIeEAtaUoc+hCMSlvBw36E38jhRr sU0UJXA7rlKLm8aSV+/4IsMU9yw+b9eMnpEF7al+5aahdUa8tR9NLAkg8yavBzeQm3S21+ WGBnJcI+hQ/lb/36h55Cz5mYd1GoWsX2tMC+djLnFWxJ3YGNDsvXWv1RtnrBfHXZskF9v7 OoGHjitj9TI6iD/brNplgXG6ioHLR8MWFfiyLEDGGwz6hoDalGyUOp5jI3fB4g== Date: Sun, 30 Apr 2023 12:53:13 +0200 Message-Id: <7643fdda3f1dbbc200b4d212fab1edc17741e06a.1682851600.git.dev@jpoiret.xyz> In-Reply-To: References: MIME-Version: 1.0 X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz 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: , Reply-to: Josselin Poiret X-ACL-Warn: , Josselin Poiret via Guix-patches X-Patchwork-Original-From: Josselin Poiret via Guix-patches via From: Josselin Poiret Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches From: Josselin Poiret * gnu/packages/agda.scm (agda): Update to 2.6.3, switch to fetching using git so that doc files are included, and add new dependency ghc-vector-hashtables. --- gnu/packages/agda.scm | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index 7128a3f108..252193de90 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -37,15 +37,17 @@ (define-module (gnu packages agda) (define-public agda (package (name "agda") - (version "2.6.2.2") + (version "2.6.3") (source (origin - (method url-fetch) - (uri (hackage-uri "Agda" version)) + (method git-fetch) + (uri (git-reference + (url "https://github.com/agda/agda.git") + (commit (string-append "v" version)))) + (file-name (git-file-name name version)) (sha256 - (base32 "0yjjbhc593ylrm4mq4j01nkdvh7xqsg5in30wxj4y53vf5hkggp5")))) + (base32 "1s7zd01i8pmvi90ywx497kc07z50nah7h0fc2dn6jzb132k5sh1q")))) (build-system haskell-build-system) - (properties '((upstream-name . "Agda"))) (inputs (list ghc-aeson ghc-alex @@ -68,6 +70,7 @@ (define-public agda ghc-strict ghc-unordered-containers ghc-uri-encode + ghc-vector-hashtables ghc-zlib)) (arguments (list #:modules `((guix build haskell-build-system) From patchwork Sun Apr 30 10:53:14 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Josselin Poiret X-Patchwork-Id: 49710 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 6AAF027BBE2; Sun, 30 Apr 2023 11:55:32 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,FROM_SUSPICIOUS_NTLD,MAILING_LIST_MULTI,PDS_OTHER_BAD_TLD, RCVD_IN_MSPIKE_H2,SPF_HELO_PASS,URIBL_BLOCKED autolearn=no autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id E83D727BBEA for ; Sun, 30 Apr 2023 11:55:30 +0100 (BST) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1pt4h0-0002v4-00; Sun, 30 Apr 2023 06:54:10 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1pt4gu-0002t5-CL for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:08 -0400 Received: from debbugs.gnu.org ([209.51.188.43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1pt4gu-0002UC-2n for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:04 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1pt4gt-0000Vo-Vb for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:03 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#61915] [PATCH v2 04/13] gnu: agda: Build info manual. Resent-From: Josselin Poiret Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 30 Apr 2023 10:54:03 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 61915 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Received: via spool by 61915-submit@debbugs.gnu.org id=B61915.16828520341861 (code B ref 61915); Sun, 30 Apr 2023 10:54:03 +0000 Received: (at 61915) by debbugs.gnu.org; 30 Apr 2023 10:53:54 +0000 Received: from localhost ([127.0.0.1]:37348 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gj-0000Tr-TN for submit@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:54 -0400 Received: from jpoiret.xyz ([206.189.101.64]:52966) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gO-0000S8-0Z for 61915@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:34 -0400 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id A9DB418531A; Sun, 30 Apr 2023 10:53:30 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1682852011; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=b6rZv4Koqc0Btpsmqle9BgZEKGnkEFmjkvlND1/ONwM=; b=AhmLBrwkcbA0pnv3Nn7/GqerIqe3O1deu/PjXUbNImrxvU4OJ/5dS22pSRCU0FDN+gX+DZ saXdwh+YkaybsgUHJl8LTs6g7MQOtZSY1Khs8hTBbgmTTf8zTFBO6GkLBFuoeS+XWyi7Oi r2KVv+RYCt38ER2gsVI+eFH5XaJXedm9OjowxJR2txAM7Z0RJIYo/cN05y/0W1OCN3uD3s tLUURgzCn8k9MlKLjdoamUvLoO5DgoMSiXI56TapeMJ6haxad3AcVykji8Eh936p9wDYvb /vBN7MB+L9+QhPgBzaz8rN4gJT2NhSPXCM17aTOuEKEFR6yrxipJSCf6wqEHFg== Date: Sun, 30 Apr 2023 12:53:14 +0200 Message-Id: <8ae7a9d4c6b42c227f602dd302dda1f3c7f97361.1682851600.git.dev@jpoiret.xyz> In-Reply-To: References: MIME-Version: 1.0 X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz 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: , Reply-to: Josselin Poiret X-ACL-Warn: , Josselin Poiret via Guix-patches X-Patchwork-Original-From: Josselin Poiret via Guix-patches via From: Josselin Poiret Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches From: Josselin Poiret * gnu/packages/agda.scm (agda): Build the user manual as an info manual. --- gnu/packages/agda.scm | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index 252193de90..eba48da0ff 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -25,6 +25,10 @@ (define-module (gnu packages agda) #:use-module (gnu packages haskell-check) #:use-module (gnu packages haskell-web) #:use-module (gnu packages haskell-xyz) + #:use-module (gnu packages imagemagick) + #:use-module (gnu packages python) + #:use-module (gnu packages sphinx) + #:use-module (gnu packages texinfo) #:use-module (guix build-system emacs) #:use-module (guix build-system gnu) #:use-module (guix build-system haskell) @@ -72,6 +76,12 @@ (define-public agda ghc-uri-encode ghc-vector-hashtables ghc-zlib)) + (native-inputs + (list python + python-sphinx + python-sphinx-rtd-theme + texinfo + imagemagick)) (arguments (list #:modules `((guix build haskell-build-system) (guix build utils) @@ -88,7 +98,16 @@ (define-public agda (let ((agda-compiler (string-append #$output "/bin/agda"))) (for-each (cut invoke agda-compiler <>) (find-files (string-append #$output "/share") - "\\.agda$")))))))) + "\\.agda$"))))) + (add-after 'agda-compile 'install-info + (lambda _ + (with-directory-excursion "doc/user-manual" + (invoke "sphinx-build" "-b" "texinfo" + "." "_build_texinfo") + (with-directory-excursion "_build_texinfo" + (setenv "infodir" (string-append #$output + "/share/info")) + (invoke "make" "install-info")))))))) (home-page "https://wiki.portal.chalmers.se/agda/") (synopsis "Dependently typed functional programming language and proof assistant") From patchwork Sun Apr 30 10:53:15 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Josselin Poiret X-Patchwork-Id: 49701 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 6505027BBE2; Sun, 30 Apr 2023 11:54:48 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,FROM_SUSPICIOUS_NTLD,MAILING_LIST_MULTI,PDS_OTHER_BAD_TLD, RCVD_IN_MSPIKE_H2,SPF_HELO_PASS,URIBL_BLOCKED autolearn=no autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id A30EA27BBE9 for ; Sun, 30 Apr 2023 11:54:47 +0100 (BST) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1pt4h1-0002vw-Cc; Sun, 30 Apr 2023 06:54:11 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1pt4gu-0002se-06 for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:04 -0400 Received: from debbugs.gnu.org ([209.51.188.43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1pt4gt-0002U7-OT for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:03 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1pt4gt-0000Vh-Jr for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:03 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#61915] [PATCH v2 05/13] gnu: emacs-agda2-mode: No longer inherit from agda. Resent-From: Josselin Poiret Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 30 Apr 2023 10:54:03 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 61915 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Received: via spool by 61915-submit@debbugs.gnu.org id=B61915.16828520341854 (code B ref 61915); Sun, 30 Apr 2023 10:54:03 +0000 Received: (at 61915) by debbugs.gnu.org; 30 Apr 2023 10:53:54 +0000 Received: from localhost ([127.0.0.1]:37338 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gU-0000Sv-OQ for submit@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:53 -0400 Received: from jpoiret.xyz ([206.189.101.64]:53052) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gP-0000SA-4Y for 61915@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:33 -0400 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id 19BE0185309; Sun, 30 Apr 2023 10:53:32 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1682852012; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=3SDbm0Zlav9bOt5CS1+ABG2iLVSbEbeFbvgC0X0ErEA=; b=G6mfReq8WuQWOrmwzaS0g8b8F6yzS8MXt43Gi3jp54XG5ZHFaUMpQzeyFQ3LOFfqc5LXUG LKV4+YedZE79voqNHNVrHrWqZXX3q9Jh60RCXER2FruDnPgUQWJYNqT9Rc3JRJPkKouDXl pbDnjT2rDRmQ8KxDoYp2aHRjWby7fuiZpwomUP//h2/VD2O1oP6i4XvosSkSaybza6jQjV K59XQLkPBHHQ6om1QDLWcXI46tNcpSU/oNmfuJ+7UZR8M+J6KrDO+fDyUoGlmjm/IuMn1x 1RbbDa74n3+o5CwCCcBBRf1lSbPhMcxMtonkD2ap1aUVYfP+HyG7opC7xgZUeg== Date: Sun, 30 Apr 2023 12:53:15 +0200 Message-Id: In-Reply-To: References: MIME-Version: 1.0 X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz 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: , Reply-to: Josselin Poiret X-ACL-Warn: , Josselin Poiret via Guix-patches X-Patchwork-Original-From: Josselin Poiret via Guix-patches via From: Josselin Poiret Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches From: Josselin Poiret * gnu/packages/agda.scm (emacs-agda2-mode): Remove it. Made no sense, as we only need the source, which we can refer to without inheriting the whole thing. --- gnu/packages/agda.scm | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index eba48da0ff..69d6d22d32 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -128,10 +128,10 @@ (define-public agda (define-public emacs-agda2-mode (package - (inherit agda) (name "emacs-agda2-mode") + (version (package-version agda)) + (source (package-source agda)) (build-system emacs-build-system) - (inputs '()) (arguments `(#:phases (modify-phases %standard-phases @@ -140,7 +140,8 @@ (define-public emacs-agda2-mode (home-page "https://agda.readthedocs.io/en/latest/tools/emacs-mode.html") (synopsis "Emacs mode for Agda") (description "This Emacs mode enables interactive development with -Agda. It also aids the input of Unicode characters."))) +Agda. It also aids the input of Unicode characters.") + (license (package-license agda)))) (define-public agda-ial (package From patchwork Sun Apr 30 10:53:16 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Josselin Poiret X-Patchwork-Id: 49709 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 8639D27BBEB; Sun, 30 Apr 2023 11:55:31 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,FROM_SUSPICIOUS_NTLD,MAILING_LIST_MULTI,PDS_OTHER_BAD_TLD, RCVD_IN_MSPIKE_H2,SPF_HELO_PASS,URIBL_BLOCKED autolearn=no autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id E4A9F27BBE9 for ; Sun, 30 Apr 2023 11:55:30 +0100 (BST) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1pt4h0-0002vQ-8p; Sun, 30 Apr 2023 06:54:10 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1pt4gy-0002tP-LZ for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:08 -0400 Received: from debbugs.gnu.org ([209.51.188.43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1pt4gv-0002UN-9L for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:08 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1pt4gv-0000WC-3b for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:05 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#61915] [PATCH v2 06/13] gnu: emacs-agda2-mode: Switch to G-Exps. Resent-From: Josselin Poiret Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 30 Apr 2023 10:54:05 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 61915 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Received: via spool by 61915-submit@debbugs.gnu.org id=B61915.16828520371887 (code B ref 61915); Sun, 30 Apr 2023 10:54:05 +0000 Received: (at 61915) by debbugs.gnu.org; 30 Apr 2023 10:53:57 +0000 Received: from localhost ([127.0.0.1]:37354 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gn-0000UH-36 for submit@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:57 -0400 Received: from jpoiret.xyz ([206.189.101.64]:53142) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gQ-0000SJ-6u for 61915@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:37 -0400 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id 332AD185317; Sun, 30 Apr 2023 10:53:33 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1682852013; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=7WgdzWoywDarAkBWIX+9wn59seC2QcchCJf0/3eR0A4=; b=rDdTZ7giGROiz3dWfouFn+GH8MaCXXH8BBNUystgzGcedIabK4udUSWLr5twg9stOoQhtQ P4BaZdoxacg8PFi+VVcC8NWkQfDec0ma6wwuVGrCEAu3vL8B0la2kuvt2wvA1dkdpkG+lm E8seeQfinh/K1r6Lg1sUXGw/3YtwzrZdOm5JPG5yIneg/CmdDl2Zs9rmuiY7pNV3gwGWHN 0lWqjXOut+g2/Uh4pJPz0TyuCBCMDdcnzxWYQAKHlg200OEnhLScIjNIoa8kGsTBf019Tx GiADvYP07SvKR55Gpcn106H29oOiFqJQwhqaWpJWbgcPp6jLIy/VBSxlK6MvTA== Date: Sun, 30 Apr 2023 12:53:16 +0200 Message-Id: <324731741e39c483c01cb6202153839ed8a56f7a.1682851600.git.dev@jpoiret.xyz> In-Reply-To: References: MIME-Version: 1.0 X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz 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: , Reply-to: Josselin Poiret X-ACL-Warn: , Josselin Poiret via Guix-patches X-Patchwork-Original-From: Josselin Poiret via Guix-patches via From: Josselin Poiret Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches From: Josselin Poiret * gnu/packages/agda.scm (emacs-agda2-mode): Switch it up. --- gnu/packages/agda.scm | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index 69d6d22d32..d94036939c 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -133,10 +133,11 @@ (define-public emacs-agda2-mode (source (package-source agda)) (build-system emacs-build-system) (arguments - `(#:phases - (modify-phases %standard-phases - (add-after 'unpack 'enter-elisp-dir - (lambda _ (chdir "src/data/emacs-mode") #t))))) + (list + #:phases + #~(modify-phases %standard-phases + (add-after 'unpack 'enter-elisp-dir + (lambda _ (chdir "src/data/emacs-mode")))))) (home-page "https://agda.readthedocs.io/en/latest/tools/emacs-mode.html") (synopsis "Emacs mode for Agda") (description "This Emacs mode enables interactive development with From patchwork Sun Apr 30 10:53:17 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Josselin Poiret X-Patchwork-Id: 49707 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 1D77427BBEA; Sun, 30 Apr 2023 11:55:28 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,FROM_SUSPICIOUS_NTLD,MAILING_LIST_MULTI,PDS_OTHER_BAD_TLD, RCVD_IN_MSPIKE_H2,SPF_HELO_PASS,URIBL_BLOCKED autolearn=no autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 3BC4C27BBE2 for ; Sun, 30 Apr 2023 11:55:26 +0100 (BST) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1pt4h0-0002vV-8q; Sun, 30 Apr 2023 06:54:10 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1pt4gy-0002tX-NE for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:08 -0400 Received: from debbugs.gnu.org ([209.51.188.43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1pt4gu-0002UM-Sf for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:08 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1pt4gu-0000W5-O3 for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:04 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#61915] [PATCH v2 07/13] gnu: agda: Add AGDA_LIBDIRS search-path. Resent-From: Josselin Poiret Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 30 Apr 2023 10:54:04 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 61915 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Received: via spool by 61915-submit@debbugs.gnu.org id=B61915.16828520371880 (code B ref 61915); Sun, 30 Apr 2023 10:54:04 +0000 Received: (at 61915) by debbugs.gnu.org; 30 Apr 2023 10:53:57 +0000 Received: from localhost ([127.0.0.1]:37352 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gm-0000UE-JF for submit@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:57 -0400 Received: from jpoiret.xyz ([206.189.101.64]:53234) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gS-0000SP-Aa for 61915@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:37 -0400 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id 5E634185309; Sun, 30 Apr 2023 10:53:34 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1682852014; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=mmqWKWO6LbU0Z0KH0b+zcEI+HiJdrSTIf5vVIe7NfEQ=; b=HA17wlQi/uF016gqVZ325klZIOYfmt3BsGKAlQw8qXFSA4Y1gM2jB9TEd9+h1vyr9Rw62M 8WCQONP+BYd8U/opM2V16KMs8/T3GGah7nil7dADi2KqjYXq7IDv4znqaG0zpejm+0AlPn 5Ymop+xO3FToMFJ3SSilERWpFv2Bdo2JtCGS5tJ3jxZPNto5kKT4+M3/o/TWNRO5yawXvm vG5+lmKxynCOYShirkCuLzGfFa0ApWu/qp9d9tUDQQ8cydjmR5RZuOlB+g8ZKS4IGnMVpm w7nMm5Qhq7a5zQjZjjaBgTgHAvD88ostS6pca7lfad3JSED876uVn3GEH0ZvQA== Date: Sun, 30 Apr 2023 12:53:17 +0200 Message-Id: <7d567a3e6da787aa9757c0f265469393dde01833.1682851600.git.dev@jpoiret.xyz> In-Reply-To: References: MIME-Version: 1.0 X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz 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: , Reply-to: Josselin Poiret X-ACL-Warn: , Josselin Poiret via Guix-patches X-Patchwork-Original-From: Josselin Poiret via Guix-patches via From: Josselin Poiret Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches From: Josselin Poiret * gnu/packages/patches/agda-libdirs-env-variable.patch: New patch. * gnu/local.mk (dist_patch_DATA): Register it. * gnu/packages/agda.scm (agda): Patch agda, and add search path. --- gnu/local.mk | 1 + gnu/packages/agda.scm | 10 +++- .../patches/agda-libdirs-env-variable.patch | 49 +++++++++++++++++++ 3 files changed, 59 insertions(+), 1 deletion(-) create mode 100644 gnu/packages/patches/agda-libdirs-env-variable.patch diff --git a/gnu/local.mk b/gnu/local.mk index 1a84e5b499..712649c5fc 100644 --- a/gnu/local.mk +++ b/gnu/local.mk @@ -880,6 +880,7 @@ dist_patch_DATA = \ %D%/packages/patches/aegisub-icu59-include-unistr.patch \ %D%/packages/patches/aegisub-boost68.patch \ %D%/packages/patches/aegisub-make43.patch \ + %D%/packages/patches/agda-libdirs-env-variable.patch \ %D%/packages/patches/agg-am_c_prototype.patch \ %D%/packages/patches/agg-2.5-gcc8.patch \ %D%/packages/patches/akonadi-paths.patch \ diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index d94036939c..17ea5b62be 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -22,6 +22,7 @@ ;;; along with GNU Guix. If not, see . (define-module (gnu packages agda) + #:use-module (gnu packages) #:use-module (gnu packages haskell-check) #:use-module (gnu packages haskell-web) #:use-module (gnu packages haskell-xyz) @@ -50,7 +51,8 @@ (define-public agda (commit (string-append "v" version)))) (file-name (git-file-name name version)) (sha256 - (base32 "1s7zd01i8pmvi90ywx497kc07z50nah7h0fc2dn6jzb132k5sh1q")))) + (base32 "1s7zd01i8pmvi90ywx497kc07z50nah7h0fc2dn6jzb132k5sh1q")) + (patches (search-patches "agda-libdirs-env-variable.patch")))) (build-system haskell-build-system) (inputs (list ghc-aeson @@ -108,6 +110,12 @@ (define-public agda (setenv "infodir" (string-append #$output "/share/info")) (invoke "make" "install-info")))))))) + (search-paths + (list (search-path-specification + (variable "AGDA_LIBDIRS") + (files (list "lib/agda"))))) + (native-search-paths + search-paths) (home-page "https://wiki.portal.chalmers.se/agda/") (synopsis "Dependently typed functional programming language and proof assistant") diff --git a/gnu/packages/patches/agda-libdirs-env-variable.patch b/gnu/packages/patches/agda-libdirs-env-variable.patch new file mode 100644 index 0000000000..3b291358a6 --- /dev/null +++ b/gnu/packages/patches/agda-libdirs-env-variable.patch @@ -0,0 +1,49 @@ +From 457bc7438a4f0801dbf332fa2369248bddf5da0c Mon Sep 17 00:00:00 2001 +Message-Id: <457bc7438a4f0801dbf332fa2369248bddf5da0c.1678309546.git.dev@jpoiret.xyz> +From: Josselin Poiret +Date: Wed, 8 Mar 2023 18:31:52 +0100 +Subject: [PATCH] Add environment variable for library directories + +AGDA_LIBDIRS is a new environment colon-separated variable for site libraries. +Agda will look for .agda-lib files directly inside direct descendants of these. +--- + src/full/Agda/Interaction/Library.hs | 16 ++++++++++++++-- + 1 file changed, 14 insertions(+), 2 deletions(-) + +diff --git a/src/full/Agda/Interaction/Library.hs b/src/full/Agda/Interaction/Library.hs +index 09c1f2a82..774cc3e74 100644 +--- a/src/full/Agda/Interaction/Library.hs ++++ b/src/full/Agda/Interaction/Library.hs +@@ -323,13 +323,25 @@ getInstalledLibraries overrideLibFile = mkLibM [] $ do + raiseErrors' [ LibrariesFileNotFound theOverrideLibFile ] + return [] + Right file -> do +- if not (lfExists file) then return [] else do ++ siteLibDirs <- liftIO $ fromMaybe [] . fmap splitAtColon . lookup "AGDA_LIBDIRS" <$> getEnvironment ++ siteLibs <- liftIO $ concat <$> mapM findSiteLibs siteLibDirs ++ if not (lfExists file) then parseLibFiles Nothing $ nubOn snd ((0,) <$> siteLibs) else do + ls <- liftIO $ stripCommentLines <$> UTF8.readFile (lfPath file) + files <- liftIO $ sequence [ (i, ) <$> expandEnvironmentVariables s | (i, s) <- ls ] +- parseLibFiles (Just file) $ nubOn snd files ++ parseLibFiles (Just file) $ nubOn snd (files ++ fmap (0,) siteLibs) + `catchIO` \ e -> do + raiseErrors' [ ReadError e "Failed to read installed libraries." ] + return [] ++ where splitAtColon :: String -> [String] ++ splitAtColon "" = [] ++ splitAtColon str = case break (==':') str of ++ (a, _:b) -> a : splitAtColon b ++ (a, "") -> [a] ++ findSiteLibs :: String -> IO [String] ++ findSiteLibs dir = do ++ subDirs <- filterM doesDirectoryExist =<< map (dir ) <$> listDirectory dir ++ subFiles <- mapM (\dir -> map (dir ) <$> listDirectory dir) subDirs ++ return $ concatMap (filter (List.isSuffixOf ".agda-lib")) subFiles + + -- | Parse the given library files. + -- + +base-commit: 183534bc41af5a53daf685122997dc98883f2be2 +-- +2.39.1 + From patchwork Sun Apr 30 10:53:18 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Josselin Poiret X-Patchwork-Id: 49699 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 DC83727BBE9; Sun, 30 Apr 2023 11:54:28 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,FROM_SUSPICIOUS_NTLD,MAILING_LIST_MULTI,PDS_OTHER_BAD_TLD, RCVD_IN_MSPIKE_H2,SPF_HELO_PASS,URIBL_BLOCKED autolearn=no autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 71E1727BBE2 for ; Sun, 30 Apr 2023 11:54:28 +0100 (BST) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1pt4h3-0002x6-GA; Sun, 30 Apr 2023 06:54:13 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1pt4gy-0002tQ-LW for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:08 -0400 Received: from debbugs.gnu.org ([209.51.188.43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1pt4gu-0002UJ-Se for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:08 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1pt4gu-0000Vv-CM for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:04 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#61915] [PATCH v2 08/13] build-system/haskell: Export default-haskell. Resent-From: Josselin Poiret Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 30 Apr 2023 10:54:04 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 61915 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Received: via spool by 61915-submit@debbugs.gnu.org id=B61915.16828520341867 (code B ref 61915); Sun, 30 Apr 2023 10:54:04 +0000 Received: (at 61915) by debbugs.gnu.org; 30 Apr 2023 10:53:54 +0000 Received: from localhost ([127.0.0.1]:37350 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gk-0000U0-AM for submit@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:54 -0400 Received: from jpoiret.xyz ([206.189.101.64]:53322) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gS-0000SQ-8G for 61915@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:36 -0400 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id 6F44C18531A; Sun, 30 Apr 2023 10:53:35 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1682852015; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=pI0Zsxyw9aF1aIRiLLBNEmMSnmN76sm0fEW8qvrzkaU=; b=wu+6GMvjnbqG4LTd4xEN7nssYH9KY+epVQlGBq/XTAxhapx+6msD5Jl6Hq+CVKcfOIo24P EkMai5+nCYjKWbrPKjxglq3YehawYi3Sh6ZI4xJJ7sZo1csQZgglUb0M0PJcqek4KwhTp/ Z8R8ZTbF+OiB8txqGid/tZsghMmYkNTv6FAAL3MfhUpXSL6hqpqOQvt0+GoMe6UACvNOfP sx1ANNGjiprHi4/BCR5stZbvuRfsvFR0jHdpV/WfjagJ7FWQJAu6tGxF7wuoBTqeH0ou9i 7eeih2SIiL2HDPqKJGaF/Tcbb9xvzWRl83Tdppz4BEtismZnF+pb9X1E0vAt9Q== Date: Sun, 30 Apr 2023 12:53:18 +0200 Message-Id: In-Reply-To: References: MIME-Version: 1.0 X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz 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: , Reply-to: Josselin Poiret X-ACL-Warn: , Josselin Poiret via Guix-patches X-Patchwork-Original-From: Josselin Poiret via Guix-patches via From: Josselin Poiret Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches From: Josselin Poiret * guix/build-system/haskell.scm: Export default-haskell. --- guix/build-system/haskell.scm | 1 + 1 file changed, 1 insertion(+) diff --git a/guix/build-system/haskell.scm b/guix/build-system/haskell.scm index b8858421c2..f8568e33db 100644 --- a/guix/build-system/haskell.scm +++ b/guix/build-system/haskell.scm @@ -33,6 +33,7 @@ (define-module (guix build-system haskell) #:use-module (ice-9 match) #:use-module (srfi srfi-1) #:export (hackage-uri + default-haskell %haskell-build-system-modules haskell-build From patchwork Sun Apr 30 10:53:19 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Josselin Poiret X-Patchwork-Id: 49703 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 A081A27BBE2; Sun, 30 Apr 2023 11:55:10 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,FROM_SUSPICIOUS_NTLD,MAILING_LIST_MULTI,PDS_OTHER_BAD_TLD, RCVD_IN_MSPIKE_H2,SPF_HELO_PASS,URIBL_BLOCKED autolearn=no autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id E3C3B27BBE9 for ; Sun, 30 Apr 2023 11:55:08 +0100 (BST) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1pt4h2-0002wj-6a; Sun, 30 Apr 2023 06:54:12 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1pt4gy-0002tZ-NZ for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:08 -0400 Received: from debbugs.gnu.org ([209.51.188.43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1pt4gv-0002UO-MX for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:08 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1pt4gv-0000WK-HH for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:05 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#61915] [PATCH v2 09/13] build-system: New agda-build-system. Resent-From: Josselin Poiret Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 30 Apr 2023 10:54:05 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 61915 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Received: via spool by 61915-submit@debbugs.gnu.org id=B61915.16828520381896 (code B ref 61915); Sun, 30 Apr 2023 10:54:05 +0000 Received: (at 61915) by debbugs.gnu.org; 30 Apr 2023 10:53:58 +0000 Received: from localhost ([127.0.0.1]:37356 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gn-0000UO-Ds for submit@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:58 -0400 Received: from jpoiret.xyz ([206.189.101.64]:53322) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gS-0000SQ-Sm for 61915@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:38 -0400 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id 57DE7185328; Sun, 30 Apr 2023 10:53:36 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1682852016; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=pPL/DSCQF+3W4K+1Gvyk7r296y2+46/+M+J37j5HEv4=; b=TuzlN2YNQ3pUH3P9/FboktAGFcuqf4wr+oH075I4bns4L2uHUhMhp79M3Udax1oR7RM0vS GqCGtKaJqLmTB6VtXHZw74siI20qh1iDHZeLPyjWur/4C821HJT6m6B1g2ZzqAV1HwXT+y 0QunaB1zZMGjBU6JswF7fJVjmjG03sa+00OVS/v58XAWRQTVpz36n3G7OI5KwD3suLqyp7 T3beP5uIsgB+XMnBcNE2aDY3JmTGkbrF9jKODG9LSPjVoJDrnBm30WyCCDBdSt5Z3ceBi/ N9AnAuAX0ZX0JgpG2HizJH8f06dQTZJHLX58i/F9HMaci7rEzjrXxZdWyEC5OQ== Date: Sun, 30 Apr 2023 12:53:19 +0200 Message-Id: In-Reply-To: References: MIME-Version: 1.0 X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz 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: , Reply-to: Josselin Poiret X-ACL-Warn: , Josselin Poiret via Guix-patches X-Patchwork-Original-From: Josselin Poiret via Guix-patches via From: Josselin Poiret Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches From: Josselin Poiret * guix/build-system/agda.scm: New file. * guix/build/agda-build-system.scm: New file. * Makefile.am (MODULES): Register them. * doc/guix.texi (Build Systems): Add documentation for agda-build-system. --- Makefile.am | 2 + doc/guix.texi | 21 ++++++ guix/build-system/agda.scm | 105 +++++++++++++++++++++++++++++ guix/build/agda-build-system.scm | 110 +++++++++++++++++++++++++++++++ 4 files changed, 238 insertions(+) create mode 100644 guix/build-system/agda.scm create mode 100644 guix/build/agda-build-system.scm diff --git a/Makefile.am b/Makefile.am index a763a7e305..9d137cfbb3 100644 --- a/Makefile.am +++ b/Makefile.am @@ -140,6 +140,7 @@ MODULES = \ guix/platforms/riscv.scm \ guix/platforms/x86.scm \ guix/build-system.scm \ + guix/build-system/agda.scm \ guix/build-system/android-ndk.scm \ guix/build-system/ant.scm \ guix/build-system/cargo.scm \ @@ -195,6 +196,7 @@ MODULES = \ guix/diagnostics.scm \ guix/ui.scm \ guix/status.scm \ + guix/build/agda-build-system.scm \ guix/build/android-ndk-build-system.scm \ guix/build/ant-build-system.scm \ guix/build/download.scm \ diff --git a/doc/guix.texi b/doc/guix.texi index 46e7fd3908..01cd199f0a 100644 --- a/doc/guix.texi +++ b/doc/guix.texi @@ -8885,6 +8885,27 @@ of @code{gnu-build-system}, and differ mainly in the set of inputs implicitly added to the build process, and in the list of phases executed. Some of these build systems are listed below. +@defvar agda-build-system +This variable is exported by @code{(guix build-system agda)}. It +implements a build procedure for Agda libraries. + +It adds @code{agda} to the set of inputs. A different Agda can be +specified with the @code{#:agda} key. + +The @code{#:plan} key is a list of cons cells @code{(@var{regexp} +. @var{parameters})}, where @var{regexp} is a regexp that should match +the @code{.agda} files to build, and @var{parameters} is an optional +list of parameters that will be passed to @code{agda} when type-checking +it. + +When the library uses Haskell to generate a file containing all imports, +the convenience @code{#:gnu-and-haskell?} can be set to @code{#t} to add +@code{ghc} and the standard inputs of @code{gnu-build-system} to the +input list. You will still need to manually add a phase or tweak the +@code{'build} phase, as in the definition of @code{agda-stdlib}. + +@end defvar + @defvar ant-build-system This variable is exported by @code{(guix build-system ant)}. It implements the build procedure for Java packages that can be built with diff --git a/guix/build-system/agda.scm b/guix/build-system/agda.scm new file mode 100644 index 0000000000..cf96ffaa68 --- /dev/null +++ b/guix/build-system/agda.scm @@ -0,0 +1,105 @@ +(define-module (guix build-system agda) + #:use-module (guix build-system) + #:use-module (guix build-system gnu) + #:use-module (guix build-system haskell) + #:use-module (guix gexp) + #:use-module (guix monads) + #:use-module (guix packages) + #:use-module (guix search-paths) + #:use-module (guix store) + #:use-module (guix utils) + #:export (default-agda + + %agda-build-system-modules + agda-build-system)) + +(define (default-agda) + ;; Lazily resolve the binding to avoid a circular dependency. + (let ((agda (resolve-interface '(gnu packages agda)))) + (module-ref agda 'agda))) + +(define %agda-build-system-modules + `((guix build agda-build-system) + ,@%gnu-build-system-modules)) + +(define %default-modules + '((guix build agda-build-system) + (guix build utils))) + +(define* (lower name + #:key source inputs native-inputs outputs system target + (agda (default-agda)) + gnu-and-haskell? + #:allow-other-keys + #:rest arguments) + "Return a bag for NAME." + (define private-keywords + '(#:target #:agda #:gnu-and-haskell? #:inputs #:native-inputs)) + + ;; TODO: cross-compilation support + (and (not target) + (bag + (name name) + (system system) + (host-inputs `(,@(if source + `(("source" ,source)) + '()) + ,@inputs)) + (build-inputs `(("agda" ,agda) + ,@(if gnu-and-haskell? + (cons* + (list "ghc" (default-haskell)) + (standard-packages)) + '()) + ,(assoc "locales" (standard-packages)) + ,@native-inputs)) + (outputs outputs) + (build agda-build) + (arguments (strip-keyword-arguments private-keywords arguments))))) + +(define* (agda-build name inputs + #:key + source + (phases '%standard-phases) + (outputs '("out")) + (search-paths '()) + (unpack-path "") + (build-flags ''()) + (tests? #t) + (system (%current-system)) + (guile #f) + plan + (extra-files '("^\\./.*\\.agda-lib$")) + (imported-modules %agda-build-system-modules) + (modules %default-modules)) + (define builder + (with-imported-modules imported-modules + #~(begin + (use-modules #$@(sexp->gexp modules)) + (agda-build #:name #$name + #:source #+source + #:system #$system + #:phases #$phases + #:outputs #$(outputs->gexp outputs) + #:search-paths '#$(sexp->gexp + (map search-path-specification->sexp + search-paths)) + #:unpack-path #$unpack-path + #:build-flags #$build-flags + #:tests? #$tests? + #:inputs #$(input-tuples->gexp inputs) + #:plan '#$plan + #:extra-files '#$extra-files)))) + + (mlet %store-monad ((guile (package->derivation (or guile (default-guile)) + system #:graft? #f))) + (gexp->derivation name builder + #:system system + #:guile-for-build guile))) + +(define agda-build-system + (build-system + (name 'agda) + (description + "Build system for Agda libraries") + (lower lower))) diff --git a/guix/build/agda-build-system.scm b/guix/build/agda-build-system.scm new file mode 100644 index 0000000000..1d7e80d61b --- /dev/null +++ b/guix/build/agda-build-system.scm @@ -0,0 +1,110 @@ +(define-module (guix build agda-build-system) + #:use-module ((guix build gnu-build-system) #:prefix gnu:) + #:use-module (guix build utils) + #:use-module (srfi srfi-26) + #:use-module (srfi srfi-34) + #:use-module (srfi srfi-35) + #:use-module (ice-9 ftw) + #:use-module (ice-9 match) + #:export (%standard-phases + agda-build)) + +(define* (set-locpath #:key inputs native-inputs #:allow-other-keys) + (let ((locales (assoc-ref (or native-inputs inputs) "locales"))) + (setenv "GUIX_LOCPATH" (string-append locales "/lib/locale")))) + +(define %agda-possible-extensions + (cons + ".agda" + (map (cute string-append ".lagda" <>) + '("" + ".md" + ".org" + ".rst" + ".tex")))) + +(define (pattern-predicate pattern) + (define compiled-rx (make-regexp pattern)) + (lambda (file stat) + (regexp-exec compiled-rx file))) + +(define* (build #:key plan #:allow-other-keys) + (for-each + (match-lambda + ((pattern . options) + (for-each + (lambda (file) + (apply invoke (cons* "agda" file options))) + (let ((files (find-files "." (pattern-predicate pattern)))) + (if (null? files) + (raise + (make-compound-condition + (condition + (&message + (message (format #f "Plan pattern `~a' did not match any files" + pattern)))) + (condition + (&error)))) + files)))) + (x + (raise + (make-compound-condition + (condition + (&message + (message (format #f "Malformed plan element `~a'" x)))) + (condition + (&error)))))) + plan)) + +(define* (install #:key outputs name extra-files #:allow-other-keys) + (define libdir (string-append (assoc-ref outputs "out") "/lib/agda/" name)) + (define agda-version + (car (scandir "./_build/" + (lambda (entry) + (not (member entry '("." ".."))))))) + (define agdai-files + (with-directory-excursion + (string-join (list "." "_build" agda-version "agda") "/") + (find-files "."))) + (define (install-source agdai) + (define dir (dirname agdai)) + ;; Drop .agdai + (define no-ext (string-drop-right agdai 6)) + (define source + (match (filter file-exists? (map (cute string-append no-ext <>) + %agda-possible-extensions)) + ((single) single) + (res (raise + (make-compound-condition + (condition + (&message + (message + (format #f + "Cannot find unique source file for agdai file `~a`, got `~a`" + agdai res)))) + (condition + (&error))))))) + (install-file source (string-append libdir "/" dir))) + (for-each install-source agdai-files) + (copy-recursively "_build" (string-append libdir "/_build")) + (for-each + (lambda (pattern) + (for-each + (lambda (file) + (install-file file libdir)) + (find-files "." (pattern-predicate pattern)))) + extra-files)) + +(define %standard-phases + (modify-phases gnu:%standard-phases + (add-before 'install-locale 'set-locpath set-locpath) + (delete 'bootstrap) + (delete 'configure) + (replace 'build build) + (delete 'check) ;; No universal checker + (replace 'install install))) + +(define* (agda-build #:key inputs (phases %standard-phases) + #:allow-other-keys #:rest args) + "Build the given Agda package, applying all of PHASES in order." + (apply gnu:gnu-build #:inputs inputs #:phases phases args)) From patchwork Sun Apr 30 10:53:20 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Josselin Poiret X-Patchwork-Id: 49705 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 5878127BBE2; Sun, 30 Apr 2023 11:55:24 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,FROM_SUSPICIOUS_NTLD,MAILING_LIST_MULTI,PDS_OTHER_BAD_TLD, RCVD_IN_MSPIKE_H2,SPF_HELO_PASS,URIBL_BLOCKED autolearn=no autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 4658027BBE9 for ; Sun, 30 Apr 2023 11:55:22 +0100 (BST) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1pt4hx-0003Mj-OE; Sun, 30 Apr 2023 06:55:11 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1pt4hr-0003KL-6u for guix-patches@gnu.org; Sun, 30 Apr 2023 06:55:03 -0400 Received: from debbugs.gnu.org ([209.51.188.43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1pt4hq-0002h0-Pi for guix-patches@gnu.org; Sun, 30 Apr 2023 06:55:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1pt4hq-0000b8-LU for guix-patches@gnu.org; Sun, 30 Apr 2023 06:55:02 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#61915] [PATCH v2 10/13] gnu: Add agda-stdlib. Resent-From: Josselin Poiret Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 30 Apr 2023 10:55:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 61915 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Received: via spool by 61915-submit@debbugs.gnu.org id=B61915.16828520562066 (code B ref 61915); Sun, 30 Apr 2023 10:55:02 +0000 Received: (at 61915) by debbugs.gnu.org; 30 Apr 2023 10:54:16 +0000 Received: from localhost ([127.0.0.1]:37379 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4h5-0000XE-OO for submit@debbugs.gnu.org; Sun, 30 Apr 2023 06:54:16 -0400 Received: from jpoiret.xyz ([206.189.101.64]:53234) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gU-0000SP-4w for 61915@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:53 -0400 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id 3ABDE18531A; Sun, 30 Apr 2023 10:53:37 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1682852017; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=mYGSblUGzIIkj+N/tdYL1iNvRjHO7pmCEgsheblgH4Q=; b=wc30Q7cANPWQ/CLgIE8GoKiLGoWem0slYMMHQBvfZDfkgIIB8qChvS+bXFwDaInHd3LHWu Mz/HDJBdKmWj66w2NCX6U0Rqo8V59aVesr8FGhzRbZ5W7M/QqqkGJmZUAmZ5yQqE5Wqza1 w0YCHx/CTA8VF4zrajG06u2gvbsNtPNoKWVwHtMD9NXfUGUIrjpLHSlsXQxqUSuLeCcYd5 YpEM6pCu+AGqlNrPMtXLBkfF3aR1jqb8y2o5VMlogNoxcvBNZb86xE7qg/Vo7wJnkCtmVF DnfgZ5/U4sWUDBFDSksk1Afd0Y22b8BTYxKxGdffGXSqlO5sWfTfLCLtI8PzBg== Date: Sun, 30 Apr 2023 12:53:20 +0200 Message-Id: <5182ba2731eb1f2e4b27164f9409cace176710de.1682851600.git.dev@jpoiret.xyz> In-Reply-To: References: MIME-Version: 1.0 X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz 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: , Reply-to: Josselin Poiret X-ACL-Warn: , Josselin Poiret via Guix-patches X-Patchwork-Original-From: Josselin Poiret via Guix-patches via From: Josselin Poiret Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches From: Josselin Poiret * gnu/packages/patches/agda-stdlib-use-runhaskell.patch: New patch. * gnu/local.mk (dist_patch_DATA): Register it. * gnu/packages/agda.scm: New variable agda-stdlib. --- gnu/local.mk | 1 + gnu/packages/agda.scm | 37 +++++++++++++++++++ .../patches/agda-stdlib-use-runhaskell.patch | 28 ++++++++++++++ 3 files changed, 66 insertions(+) create mode 100644 gnu/packages/patches/agda-stdlib-use-runhaskell.patch diff --git a/gnu/local.mk b/gnu/local.mk index 712649c5fc..0a1c4dfb24 100644 --- a/gnu/local.mk +++ b/gnu/local.mk @@ -881,6 +881,7 @@ dist_patch_DATA = \ %D%/packages/patches/aegisub-boost68.patch \ %D%/packages/patches/aegisub-make43.patch \ %D%/packages/patches/agda-libdirs-env-variable.patch \ + %D%/packages/patches/agda-stdlib-use-runhaskell.patch \ %D%/packages/patches/agg-am_c_prototype.patch \ %D%/packages/patches/agg-2.5-gcc8.patch \ %D%/packages/patches/akonadi-paths.patch \ diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index 17ea5b62be..a6ff01b737 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -30,6 +30,7 @@ (define-module (gnu packages agda) #:use-module (gnu packages python) #:use-module (gnu packages sphinx) #:use-module (gnu packages texinfo) + #:use-module (guix build-system agda) #:use-module (guix build-system emacs) #:use-module (guix build-system gnu) #:use-module (guix build-system haskell) @@ -193,3 +194,39 @@ (define-public agda-ial trees, tries, vectors, and rudimentary IO. A number of good ideas come from Agda's standard library.") (license license:expat))) + +(define-public agda-stdlib + (package + (name "agda-stdlib") + (version "1.7.2") + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/agda/agda-stdlib") + (commit (string-append "v" version)))) + (sha256 + (base32 + "065hf24xjpciwdrvk4isslgcgi01q0k93ql0y1sjqqvy5ryg5xmy")))) + (build-system agda-build-system) + (arguments + (list + #:plan '(("^\\./README.agda$" "-i.")) + #:gnu-and-haskell? #t + #:phases + #~(modify-phases %standard-phases + (add-before 'build 'generate-everything + (lambda* (#:key inputs native-inputs #:allow-other-keys) + (invoke + (search-input-file (or native-inputs inputs) "/bin/runhaskell") + "GenerateEverything.hs")))))) + (native-inputs (list ghc-filemanip)) + (synopsis "The Agda Standard Library") + (description + "The standard library aims to contain all the tools needed to write +both programs and proofs easily. While we always try and write efficient +code, we prioritize ease of proof over type-checking and normalization +performance. If computational performance is important to you, then perhaps +try agda-prelude instead.") + (home-page "https://wiki.portal.chalmers.se/agda/pmwiki.php") + (license license:expat))) + diff --git a/gnu/packages/patches/agda-stdlib-use-runhaskell.patch b/gnu/packages/patches/agda-stdlib-use-runhaskell.patch new file mode 100644 index 0000000000..21ce16689f --- /dev/null +++ b/gnu/packages/patches/agda-stdlib-use-runhaskell.patch @@ -0,0 +1,28 @@ +From 3dc3c0856906d25bb697a4480a8457a69637cd51 Mon Sep 17 00:00:00 2001 +Message-Id: <3dc3c0856906d25bb697a4480a8457a69637cd51.1682798848.git.dev@jpoiret.xyz> +From: Josselin Poiret +Date: Sat, 29 Apr 2023 22:06:55 +0200 +Subject: [PATCH] Makefile: use runhaskell instead of cabal + +From: Josselin Poiret + +--- + GNUmakefile | 2 +- + 1 file changed, 1 insertion(+), 1 deletion(-) + +diff --git a/GNUmakefile b/GNUmakefile +index c5d886e03..f3cb2a1e7 100644 +--- a/GNUmakefile ++++ b/GNUmakefile +@@ -21,7 +21,7 @@ Everything.agda: + # command `cabal install` is needed by cabal-install <= 2.4.*. I did + # not found any problem running both commands with different versions + # of cabal-install. See Issue #1001. +- cabal run GenerateEverything ++ runhaskell GenerateEverything + + .PHONY: listings + listings: Everything.agda +-- +2.39.2 + From patchwork Sun Apr 30 10:53:21 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Josselin Poiret X-Patchwork-Id: 49698 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 D651627BBEA; Sun, 30 Apr 2023 11:54:24 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,FROM_SUSPICIOUS_NTLD,MAILING_LIST_MULTI,PDS_OTHER_BAD_TLD, RCVD_IN_MSPIKE_H2,SPF_HELO_PASS,URIBL_BLOCKED autolearn=no autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id AB1E827BBE9 for ; Sun, 30 Apr 2023 11:54:23 +0100 (BST) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1pt4h3-0002xO-NS; Sun, 30 Apr 2023 06:54:13 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1pt4gy-0002tY-NJ for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:08 -0400 Received: from debbugs.gnu.org ([209.51.188.43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1pt4gw-0002UP-1z for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:08 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1pt4gv-0000WS-Ui for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:05 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#61915] [PATCH v2 11/13] gnu: Add agda-categories. Resent-From: Josselin Poiret Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 30 Apr 2023 10:54:05 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 61915 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Received: via spool by 61915-submit@debbugs.gnu.org id=B61915.16828520391909 (code B ref 61915); Sun, 30 Apr 2023 10:54:05 +0000 Received: (at 61915) by debbugs.gnu.org; 30 Apr 2023 10:53:59 +0000 Received: from localhost ([127.0.0.1]:37358 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4go-0000UX-3W for submit@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:58 -0400 Received: from jpoiret.xyz ([206.189.101.64]:53586) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4ga-0000TJ-9w for 61915@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:44 -0400 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id 886A3185309; Sun, 30 Apr 2023 10:53:38 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1682852018; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=A0yDo8vue0W+vSJ0wKJ7KU5tbn+r72lpGbjDlPht2w0=; b=qHcPYO4/phy0+1udh0TIKE3/LcmoUqvXZYiw4o+VnvVCNyVeASMFygch6qmT14+cWqhvLF 4paF/sIbc4R7rN4B0vC30dPhfp9hAW4JcZFtjz7SUmfuqPVpzMr/58Rg9HfYDQ7cc06WP5 OSQX3EQ9Qs+dTIo9XZ2Lm5SYaCUU+1v66PvHMYpBY4Li/PjNT7MnAy0UtWi1DdsbrQa/Xw L9rJpw28r4QrQZkWJjASiq1EXWHWyEFHwbrqxUpOhiyHtQbHf9H1fKxqJORVLOa8cdiPxx iKsaRXc2o5JVakFIp68LjCFw6BsZd0Zq+A3YkgBMussQ9122R1o9W5vIqhs59g== Date: Sun, 30 Apr 2023 12:53:21 +0200 Message-Id: <667b750918cd5dc1b5ae8b635871aa9f942b763b.1682851600.git.dev@jpoiret.xyz> In-Reply-To: References: MIME-Version: 1.0 X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz 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: , Reply-to: Josselin Poiret X-ACL-Warn: , Josselin Poiret via Guix-patches X-Patchwork-Original-From: Josselin Poiret via Guix-patches via From: Josselin Poiret Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches From: Josselin Poiret * gnu/packages/patches/agda-categories-bump-stdlib-version.patch * gnu/packages/patches/agda-categories-remove-incompatible-flags.patch * gnu/packages/patches/agda-categories-use-find.patch: New patches. * gnu/local.mk (dist_patch_DATA): Register them. * gnu/packages/agda.scm: New variable agda-categories. --- gnu/local.mk | 3 ++ gnu/packages/agda.scm | 35 ++++++++++++++++ .../agda-categories-bump-stdlib-version.patch | 42 +++++++++++++++++++ ...categories-remove-incompatible-flags.patch | 31 ++++++++++++++ .../patches/agda-categories-use-find.patch | 31 ++++++++++++++ 5 files changed, 142 insertions(+) create mode 100644 gnu/packages/patches/agda-categories-bump-stdlib-version.patch create mode 100644 gnu/packages/patches/agda-categories-remove-incompatible-flags.patch create mode 100644 gnu/packages/patches/agda-categories-use-find.patch diff --git a/gnu/local.mk b/gnu/local.mk index 0a1c4dfb24..4193146862 100644 --- a/gnu/local.mk +++ b/gnu/local.mk @@ -880,6 +880,9 @@ dist_patch_DATA = \ %D%/packages/patches/aegisub-icu59-include-unistr.patch \ %D%/packages/patches/aegisub-boost68.patch \ %D%/packages/patches/aegisub-make43.patch \ + %D%/packages/patches/agda-categories-bump-stdlib-version.patch \ + %D%/packages/patches/agda-categories-remove-incompatible-flags.patch \ + %D%/packages/patches/agda-categories-use-find.patch \ %D%/packages/patches/agda-libdirs-env-variable.patch \ %D%/packages/patches/agda-stdlib-use-runhaskell.patch \ %D%/packages/patches/agg-am_c_prototype.patch \ diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index a6ff01b737..1068d8734f 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -230,3 +230,38 @@ (define-public agda-stdlib (home-page "https://wiki.portal.chalmers.se/agda/pmwiki.php") (license license:expat))) +(define-public agda-categories + ;; Upstream hasn't released in a very long time, especially not against + ;; 2.6.3. + (let* ((revision "1") + (commit "20397e93a60ed1439ed57ee76ae377c66a5eb8d9")) + (package + (name "agda-categories") + (version (git-version "0.4" revision commit)) + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/agda/agda-categories.git") + (commit commit))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "0q4dqvs4ig138wghlglz37ay5i524gk6k5x476ki5mnxc603bmqy")) + (patches (search-patches "agda-categories-bump-stdlib-version.patch" + "agda-categories-remove-incompatible-flags.patch" + "agda-categories-use-find.patch")))) + (build-system agda-build-system) + (arguments + (list + #:gnu-and-haskell? #t + #:phases + #~(modify-phases %standard-phases + (replace 'build + (lambda _ + (invoke "make")))))) + (propagated-inputs + (list agda-stdlib)) + (synopsis "A new Categories library for Agda") + (description "A new Categories library for Agda") + (home-page "https://github.com/agda/agda-categories") + (license license:expat)))) diff --git a/gnu/packages/patches/agda-categories-bump-stdlib-version.patch b/gnu/packages/patches/agda-categories-bump-stdlib-version.patch new file mode 100644 index 0000000000..2e78cc1446 --- /dev/null +++ b/gnu/packages/patches/agda-categories-bump-stdlib-version.patch @@ -0,0 +1,42 @@ +From 080eae2adc1b0e8f1829c4138b3d462218a02f36 Mon Sep 17 00:00:00 2001 +Message-Id: <080eae2adc1b0e8f1829c4138b3d462218a02f36.1682840777.git.dev@jpoiret.xyz> +From: Josselin Poiret +Date: Sun, 30 Apr 2023 09:32:59 +0200 +Subject: [PATCH] Bump Agda to 2.6.3 and stdlib to 1.7.2 + +From: Josselin Poiret + +--- + .github/workflows/ci-ubuntu.yml | 4 ++-- + agda-categories.agda-lib | 2 +- + 2 files changed, 3 insertions(+), 3 deletions(-) + +diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml +index ab26835d..25604420 100644 +--- a/.github/workflows/ci-ubuntu.yml ++++ b/.github/workflows/ci-ubuntu.yml +@@ -45,8 +45,8 @@ on: + ######################################################################## + + env: +- AGDA_COMMIT: tags/v2.6.2 +- STDLIB_VERSION: 1.7.1 ++ AGDA_COMMIT: tags/v2.6.3 ++ STDLIB_VERSION: 1.7.2 + + GHC_VERSION: 8.6.5 + CABAL_VERSION: 3.2.0.0 +diff --git a/agda-categories.agda-lib b/agda-categories.agda-lib +index 186e350b..5b19c405 100644 +--- a/agda-categories.agda-lib ++++ b/agda-categories.agda-lib +@@ -1,3 +1,3 @@ + name: agda-categories +-depend: standard-library-1.7.1 ++depend: standard-library-1.7.2 + include: src/ + +base-commit: 20397e93a60ed1439ed57ee76ae377c66a5eb8d9 +-- +2.39.2 + diff --git a/gnu/packages/patches/agda-categories-remove-incompatible-flags.patch b/gnu/packages/patches/agda-categories-remove-incompatible-flags.patch new file mode 100644 index 0000000000..dc33af7cf9 --- /dev/null +++ b/gnu/packages/patches/agda-categories-remove-incompatible-flags.patch @@ -0,0 +1,31 @@ +From 3d73d59617281c6ae9c19032eae381ff77fd2e65 Mon Sep 17 00:00:00 2001 +Message-Id: <3d73d59617281c6ae9c19032eae381ff77fd2e65.1682841188.git.dev@jpoiret.xyz> +From: Josselin Poiret +Date: Sun, 30 Apr 2023 09:51:12 +0200 +Subject: [PATCH] Remove stdlib-incompatible flags + +From: Josselin Poiret + +--- + Makefile | 2 +- + 1 file changed, 1 insertion(+), 1 deletion(-) + +diff --git a/Makefile b/Makefile +index 68846579..ba5923a2 100644 +--- a/Makefile ++++ b/Makefile +@@ -1,6 +1,6 @@ + .PHONY: test Everything.agda clean + +-OTHEROPTS = --auto-inline -Werror ++OTHEROPTS = + + RTSARGS = +RTS -M6G -A128M -RTS ${OTHEROPTS} + + +base-commit: 20397e93a60ed1439ed57ee76ae377c66a5eb8d9 +prerequisite-patch-id: da10df58fa86d08b31174a01db7b9a02377aba55 +prerequisite-patch-id: 508dabd923ba9ac1ee4d8dab6697432b4bd8ba18 +-- +2.39.2 + diff --git a/gnu/packages/patches/agda-categories-use-find.patch b/gnu/packages/patches/agda-categories-use-find.patch new file mode 100644 index 0000000000..772352a0cb --- /dev/null +++ b/gnu/packages/patches/agda-categories-use-find.patch @@ -0,0 +1,31 @@ +From 53922aedd81d5111d9007b41235aa12eaa2a863d Mon Sep 17 00:00:00 2001 +Message-Id: <53922aedd81d5111d9007b41235aa12eaa2a863d.1682840933.git.dev@jpoiret.xyz> +From: Josselin Poiret +Date: Sun, 30 Apr 2023 09:48:21 +0200 +Subject: [PATCH] Use find instead of git ls-tree in Makefile + +From: Josselin Poiret + +--- + Makefile | 2 +- + 1 file changed, 1 insertion(+), 1 deletion(-) + +diff --git a/Makefile b/Makefile +index 158802d1..68846579 100644 +--- a/Makefile ++++ b/Makefile +@@ -11,7 +11,7 @@ html: Everything.agda + agda ${RTSARGS} --html -i. Everything.agda + + Everything.agda: +- git ls-tree --full-tree -r --name-only HEAD | grep '^src/[^\.]*.agda' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' | LC_COLLATE='C' sort > Everything.agda ++ find src -iname '*.agda' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' | LC_COLLATE='C' sort > Everything.agda + + clean: + find . -name '*.agdai' -exec rm \{\} \; + +base-commit: 20397e93a60ed1439ed57ee76ae377c66a5eb8d9 +prerequisite-patch-id: da10df58fa86d08b31174a01db7b9a02377aba55 +-- +2.39.2 + From patchwork Sun Apr 30 10:53:22 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Josselin Poiret X-Patchwork-Id: 49702 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 55A2E27BBEA; Sun, 30 Apr 2023 11:54:49 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,FROM_SUSPICIOUS_NTLD,MAILING_LIST_MULTI,PDS_OTHER_BAD_TLD, RCVD_IN_MSPIKE_H2,SPF_HELO_PASS,URIBL_BLOCKED autolearn=no autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id DB04627BBE2 for ; Sun, 30 Apr 2023 11:54:48 +0100 (BST) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1pt4h0-0002vn-GW; Sun, 30 Apr 2023 06:54:10 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1pt4gy-0002tU-Mw for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:08 -0400 Received: from debbugs.gnu.org ([209.51.188.43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1pt4gw-0002UQ-DQ for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:08 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1pt4gw-0000Wa-9z for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:06 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#61915] [PATCH v2 12/13] gnu: Add agda-cubical. Resent-From: Josselin Poiret Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 30 Apr 2023 10:54:06 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 61915 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Received: via spool by 61915-submit@debbugs.gnu.org id=B61915.16828520391917 (code B ref 61915); Sun, 30 Apr 2023 10:54:06 +0000 Received: (at 61915) by debbugs.gnu.org; 30 Apr 2023 10:53:59 +0000 Received: from localhost ([127.0.0.1]:37360 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4go-0000Uk-Se for submit@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:59 -0400 Received: from jpoiret.xyz ([206.189.101.64]:53688) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gg-0000TW-B5 for 61915@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:50 -0400 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id 7A03E185317; Sun, 30 Apr 2023 10:53:44 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1682852024; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=R+m2Rb1HsVD0k91rF+mWTVmSxKsd4hTQ+agi5nwJIag=; b=tgg/0L7Ac7uKV3HJ2JtX09BYiIqBtLVIrrLv3W7CcW13y1k6TWm2ktxTAx/FRWG6kDQ8PK Kl/a65AupHXRT4kLnbXKlGWPOJA83wRwat99llz9WITnL5MXZqHFIv8ImWjajGvZVaTLtZ gIuIy51adYFOUo3TCaHpvO1joYqyiBgn3aqn3nHMHC2H6anrcG+EVkA1r2LcKG3gI1rt7G X0o72+f90OoEkijI6EaMyWAh1MYRX5gRqOS48YPjOlgmhnney/WF6raL7vIDNSnwBAxt/j q3RQOxE5BTjNUW68QyDecYpLmGGMyd4SpDyGRrBLqPnExkwcD+wrrucGV5861g== Date: Sun, 30 Apr 2023 12:53:22 +0200 Message-Id: In-Reply-To: References: MIME-Version: 1.0 X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz 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: , Reply-to: Josselin Poiret X-ACL-Warn: , Josselin Poiret via Guix-patches X-Patchwork-Original-From: Josselin Poiret via Guix-patches via From: Josselin Poiret Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches From: Josselin Poiret * gnu/packages/agda.scm: New variable agda-cubical. --- gnu/packages/agda.scm | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index 1068d8734f..e75386c990 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -265,3 +265,36 @@ (define-public agda-categories (description "A new Categories library for Agda") (home-page "https://github.com/agda/agda-categories") (license license:expat)))) + +(define-public agda-cubical + ;; Upstream's HEAD follows the latest Agda release, but they don't release + ;; until a newer Agda release comes up, so their releases are always one + ;; version late. + (let* ((revision "1") + (commit "3dc3cd12579544c8c1c1d2c5f64fd8d577fd3d66")) + (package + (name "agda-cubical") + (version (git-version "0.4" revision commit)) + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/agda/cubical.git") + (commit commit))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "1b40adjgwrrdarzk0yiy2jmjgmf455ax6z70hfzdgc6j06vdb6mg")))) + (build-system agda-build-system) + (arguments + (list + #:gnu-and-haskell? #t + #:phases + #~(modify-phases %standard-phases + (replace 'build + (lambda _ + (invoke "make")))))) + (synopsis "A standard library for Cubical Agda") + (description "A standard library for Cubical Agda, comparable to +agda-stdlib but using cubical methods.") + (home-page "https://github.com/agda/cubical") + (license license:expat)))) From patchwork Sun Apr 30 10:53:23 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Patchwork-Submitter: Josselin Poiret X-Patchwork-Id: 49700 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 D5A8427BBEA; Sun, 30 Apr 2023 11:54:46 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,FROM_SUSPICIOUS_NTLD,MAILING_LIST_MULTI,PDS_OTHER_BAD_TLD, RCVD_IN_MSPIKE_H2,SPF_HELO_PASS,URIBL_BLOCKED autolearn=no autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 4862827BBE9 for ; Sun, 30 Apr 2023 11:54:46 +0100 (BST) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1pt4h0-0002vo-GZ; Sun, 30 Apr 2023 06:54:10 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1pt4gy-0002tT-Mo for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:08 -0400 Received: from debbugs.gnu.org ([209.51.188.43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1pt4gw-0002US-Pq for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:08 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1pt4gw-0000Wh-MX for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:06 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#61915] [PATCH v2 13/13] gnu: Add agda-1lab. Resent-From: Josselin Poiret Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 30 Apr 2023 10:54:06 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 61915 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Received: via spool by 61915-submit@debbugs.gnu.org id=B61915.16828520391923 (code B ref 61915); Sun, 30 Apr 2023 10:54:06 +0000 Received: (at 61915) by debbugs.gnu.org; 30 Apr 2023 10:53:59 +0000 Received: from localhost ([127.0.0.1]:37362 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gp-0000Us-6v for submit@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:59 -0400 Received: from jpoiret.xyz ([206.189.101.64]:53688) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gh-0000TW-RI for 61915@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:52 -0400 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id 7111D185309; Sun, 30 Apr 2023 10:53:50 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1682852031; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=DdSpPyuUWFRCUHBcQmdriYmRs0c5cTY6AGDMUAf0AnA=; b=HVZHI7AkqObScKd93SmbyM3ohGIuMsaB6eJ9XDmroNGMGRSnqNMMPdyG7pgB3JkMMo31Zp CdBrG5KabWDRLW0ob5Y4BI24rg0tz6MgJxEOaZcM40YlvR4QnijEq4dXX/zpDtfiyJytaV P4IX8bSrfxQaubfO78vYrw7rqamSgaiuLLQeMoX3A4FbMG4FxJvn91CXp8pNFvt1yFwmGi wp6iHpDBD/OfjVEgB7gNfj7DASsamqsB0R6vKkwFPImDbxPMp05JhAu4QyC/KHzFBV7VFR h9AqE7v/GbCn4IA+Wh8Vy5YA/s5pfYlgFc3dFB4zZVtKjTFoW+inlcdiPT9Hbw== Date: Sun, 30 Apr 2023 12:53:23 +0200 Message-Id: <964670c477f99bf7473fd497eae3059440ce3ced.1682851600.git.dev@jpoiret.xyz> In-Reply-To: References: MIME-Version: 1.0 X-Spamd-Bar: --- Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz 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: , Reply-to: Josselin Poiret X-ACL-Warn: , Josselin Poiret via Guix-patches X-Patchwork-Original-From: Josselin Poiret via Guix-patches via From: Josselin Poiret Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches From: Josselin Poiret * gnu/packages/agda.scm: New variable agda-1lab. --- gnu/packages/agda.scm | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index e75386c990..2116ceced3 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -298,3 +298,32 @@ (define-public agda-cubical agda-stdlib but using cubical methods.") (home-page "https://github.com/agda/cubical") (license license:expat)))) + +(define-public agda-1lab + ;; Upstream doesn't do releases (yet). Use a commit that builds with 2.6.3, + ;; since they use Agda HEAD. + (let* ((revision "1") + (commit "47ca1d23640a6f49a3abe3c2fe27738bcc10c9c6")) + (package + (name "agda-1lab") + (version (git-version "0.0" revision commit)) + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/plt-amy/1lab.git") + (commit commit))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "0j7mp6c0xd0849skdxzncklkxynxnyfrbpcjv4qp5p1xfn0dnfqx")))) + (build-system agda-build-system) + (arguments + (list #:plan '(("src/index\\.lagda\\.md$")))) + (synopsis "Areference resource for mathematics done in Homotopy Type Theory") + (description "A formalised, cross-linked reference resource for +mathematics done in Homotopy Type Theory. Unlike the HoTT book, the 1lab is +not a “linear” resource: Concepts are presented as a directed graph, with +links indicating dependencies.") + (home-page "https://1lab.dev") + (license license:agpl3))))