GNU bug report logs - #61848
[[PATCH] 0/4] Agda Update and Standard Library

Please note: This is a static page, with minimal formatting, updated once a day.
Click here to see this page with the latest information and nicer formatting.
Package: guix-patches; Reported by: Christopher Rodriguez <yewscion@HIDDEN>; Keywords: patch; merged with #61915; dated Mon, 27 Feb 2023 18:12:02 UTC; Maintainer for guix-patches is guix-patches@HIDDEN.
Merged 61848 61915. Request was from Josselin Poiret <dev@HIDDEN> to control <at> debbugs.gnu.org. Full text available.

Message received at 61848 <at> debbugs.gnu.org:


Received: (at 61848) by debbugs.gnu.org; 30 Apr 2023 11:23:53 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Sun Apr 30 07:23:53 2023
Received: from localhost ([127.0.0.1]:37396 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1pt59l-0001XT-Ag
	for submit <at> debbugs.gnu.org; Sun, 30 Apr 2023 07:23:53 -0400
Received: from jpoiret.xyz ([206.189.101.64]:55822)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <dev@HIDDEN>)
 id 1pt59i-0001XG-7e; Sun, 30 Apr 2023 07:23:52 -0400
Received: from authenticated-user (jpoiret.xyz [206.189.101.64])
 by jpoiret.xyz (Postfix) with ESMTPA id B1DCC185300;
 Sun, 30 Apr 2023 11:23:48 +0000 (UTC)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim;
 t=1682853829;
 h=from:from:reply-to:subject:subject:date:date:message-id:message-id:
 to:to:cc:cc:mime-version:mime-version:content-type:content-type:
 in-reply-to:in-reply-to:references:references;
 bh=cWPHhFSU5tk1BoLBs/uLFyuLtyL7tckpbKjzhK8eXEY=;
 b=BBXQ9BPE4gsPfrTsNVyPDCyqBYDYrel3mNr62y/eZF+ekcNFDrWnufCQE1I7IiTV4g3W//
 50Oul0nKmG0pTwL6elJKt5/UzXCZb2RnB33lk7qyEoAnNYz5C9RUBlnsfXuM1CnSABnPjz
 jWoZ+du9/cMknDUWKNkmk2Y8WYTxu58AMJmgY1OZBE9DesO/6ZTLEkxRkp2Vtiz/sc9fBi
 3Ui3tvc5/8o3xG4YtFmPcWlntl6veituWIACreSn98ntU6n7bp9mxr5LwpCXoDZb5UYZVl
 nRYOwrWfFMBARunIe+kxhnz1JHeg9nfODO4QQubJQOHKRsigdg2qBVWA5XgtGg==
From: Josselin Poiret <dev@HIDDEN>
To: Christopher Rodriguez <yewscion@HIDDEN>, 61848 <at> debbugs.gnu.org
Subject: Re: [bug#61848] [[PATCH] 0/4] Agda Update and Standard Library
In-Reply-To: <20230227181055.21133-1-yewscion@HIDDEN>
References: <20230227181055.21133-1-yewscion@HIDDEN>
Date: Sun, 30 Apr 2023 13:23:46 +0200
Message-ID: <87bkj5ehq5.fsf@HIDDEN>
MIME-Version: 1.0
Content-Type: multipart/signed; boundary="=-=-=";
 micalg=pgp-sha512; protocol="application/pgp-signature"
X-Spamd-Bar: /
Authentication-Results: jpoiret.xyz;
 auth=pass smtp.auth=jpoiret@HIDDEN smtp.mailfrom=dev@HIDDEN
X-Spam-Score: 0.0 (/)
X-Debbugs-Envelope-To: 61848
Cc: control <at> debbugs.gnu.org
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: 0.0 (/)

--=-=-=
Content-Type: text/plain
Content-Transfer-Encoding: quoted-printable

merge 61848 61915
thankyou

Hi Christopher,

Sorry to come back so late to this patchset.  I finally got around to
work on this, and decided to plainly add an agda-build-system, and
shuffle some stuff around to make Guix work properly with Agda
libraries.  This lets us add agda-stdlib, cubical, agda-categories, etc.
I'm merging both issues, I hope that's fine with you.  Let me know what
you think.

Best,
=2D-=20
Josselin Poiret

--=-=-=
Content-Type: application/pgp-signature; name="signature.asc"

-----BEGIN PGP SIGNATURE-----

iQHEBAEBCgAuFiEEOSSM2EHGPMM23K8vUF5AuRYXGooFAmROT8IQHGRldkBqcG9p
cmV0Lnh5egAKCRBQXkC5FhcaiuKWC/9CpM+11dIOqK+g78h1XSmQUQ0/JA4c7ASR
ZeGVR+WoK+s1Gvm+YqfROLvnSPsycJ5nkEu2DbNgd+O/dAUkzEkvpaJTeA745Cio
go8UZdZswy9i4uXJEIhznv4bGQseI3gjS/gr9lKCIa4V0kyHPH0ErNc/YiN7VHh7
F/sZqEQN5cPKS6bcVUQuF06IaIgUYDhSn/GbJJq1DMsc5WZ8zC1fYEdartRqLvPs
Vdbbs3mNbByqT2YG8G0D/8ApyRZfsAbKlWdFX5rnYBqWVy/xhX97jIkFIrXmUdEg
6wjvOlpxht0X8L9hmEmRf7zDKmlI+hscLIAi6ZEMTs1COETmPXMgogef8uQ3Sl+E
7tmDf8T89dPCizEcv9bdv/a4YfN8oXqhR01F/LQBG1zQ0oJIYF9ziYx1dWpEB08w
/Jg753tpTb/5DnuH4n5/7Q7dGXQBt76fuPZcOW1/FYh61hgawiGwbQA77mFxuXv6
6DzEk4u9QVg6KUsEbR1fzTqmEZvVRAo=
=tahV
-----END PGP SIGNATURE-----
--=-=-=--
Information forwarded to guix-patches@HIDDEN:
bug#61848; Package guix-patches. Full text available.

Message received at 61848 <at> debbugs.gnu.org:


Received: (at 61848) by debbugs.gnu.org; 27 Feb 2023 18:13:56 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Mon Feb 27 13:13:56 2023
Received: from localhost ([127.0.0.1]:48745 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1pWi0Z-00086c-VV
	for submit <at> debbugs.gnu.org; Mon, 27 Feb 2023 13:13:56 -0500
Received: from mail-qt1-f178.google.com ([209.85.160.178]:43925)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <yewscion@HIDDEN>) id 1pWi0Y-000866-1J
 for 61848 <at> debbugs.gnu.org; Mon, 27 Feb 2023 13:13:54 -0500
Received: by mail-qt1-f178.google.com with SMTP id cf14so7633982qtb.10
 for <61848 <at> debbugs.gnu.org>; Mon, 27 Feb 2023 10:13:54 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=gmail.com; s=20210112; t=1677521628;
 h=content-transfer-encoding:mime-version:references:in-reply-to
 :message-id:date:subject:cc:to:from:from:to:cc:subject:date
 :message-id:reply-to;
 bh=G4UGcGlW5ictJqbCsbZ8Ir8LhSlJXMS5wzO42oy4s+Y=;
 b=WGFerhpSrHt5HCivqHvgMLLpE7E23NSxhNh3mRugxIkJszxpf1XqVb2vEG/MbfR5/p
 mh5XcgfrgaE20CPAt5HPk3a5WTPWdb56FhJYhmXOp3/+wqqdAsGsZiqMbkMLRoM+LHIn
 piGRZe3UU85OjJ/fkJ3TPR96+ic5PTZuABaHshbJs0XWccqQ6+/Hhr7J1X9ntYfAR/Sp
 q7DYd/cChBe1zfFeEm7ZdVjde51b02eN+adeLGHX3Hc7yx7uGg+CJ07nj+wr2C6JlgbG
 ju4oeKdh8XYjYDOHlLl/hGew3D4BGAdWsGoGH5+bADZIJpNAvrzVmWHgozew/v12LSyG
 mWIw==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=1e100.net; s=20210112; t=1677521628;
 h=content-transfer-encoding:mime-version:references:in-reply-to
 :message-id:date:subject:cc:to:from:x-gm-message-state:from:to:cc
 :subject:date:message-id:reply-to;
 bh=G4UGcGlW5ictJqbCsbZ8Ir8LhSlJXMS5wzO42oy4s+Y=;
 b=Lv1QAaextxyP+oWUEhR9687x+/85h4n8FKasNZW3lbCe6lC7wrMY4gfSgHM59Hb1/S
 BMWQtdkIaWP9lXHdaoC7chk26RduIVn8SrJkB9bbctSqhJ2t8zk7/Y70Pxx0HVaJd8/f
 KfOjSqVVii4zv9dE9HzPr3LhfRl/O+Kqu0eHWe5uZ5DzQMjrIGh94zs4+W26H8+y9rOo
 Vpi+/pBxaO5BepIyZMQlmHGouCl5I+cLNDIgTi7WPld5UAboZ6S+duceaumWEnBT8CiQ
 QBeAYVHwCeExnT3x3sQFrNfaKSjiRpJ9ExRVke5igqO+pdyx0rWC0OUP0tjCNP66otd5
 fnZQ==
X-Gm-Message-State: AO0yUKWcUQA0JuiLzIl1FJ+fSkK4fORD4ekZqDNhFcN5MdKGPsT9sFgK
 3a9cYCnVe6ewlZjfcIFDs4fl4P5Fmu0=
X-Google-Smtp-Source: AK7set8opt8OwNxDD15ZmvHfRyLCPvrFWuq36hjzfdRYx2I98jUqxvh3NF5gONDZXa8H40t5jH4+2Q==
X-Received: by 2002:a05:622a:18a1:b0:3bf:a3d0:9023 with SMTP id
 v33-20020a05622a18a100b003bfa3d09023mr302453qtc.5.1677521628196; 
 Mon, 27 Feb 2023 10:13:48 -0800 (PST)
Received: from gmail.com (ec2-3-210-134-10.compute-1.amazonaws.com.
 [3.210.134.10]) by smtp.gmail.com with ESMTPSA id
 k8-20020a05620a142800b0073ba211e765sm5368650qkj.19.2023.02.27.10.13.47
 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256);
 Mon, 27 Feb 2023 10:13:47 -0800 (PST)
From: Christopher Rodriguez <yewscion@HIDDEN>
To: 61848 <at> debbugs.gnu.org
Subject: [[PATCH] 4/4] gnu/packages/agda.scm: Add agda-stdlib v1.7.2.
Date: Mon, 27 Feb 2023 13:13:23 -0500
Message-Id: <20230227181323.21387-4-yewscion@HIDDEN>
X-Mailer: git-send-email 2.39.1
In-Reply-To: <20230227181323.21387-1-yewscion@HIDDEN>
References: <20230227181323.21387-1-yewscion@HIDDEN>
MIME-Version: 1.0
Content-Transfer-Encoding: 8bit
X-Spam-Score: 0.0 (/)
X-Debbugs-Envelope-To: 61848
Cc: Christopher Rodriguez <yewscion@HIDDEN>
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)

Signed-off-by: Christopher Rodriguez <yewscion@HIDDEN>
---
 gnu/packages/agda.scm | 41 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)

diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 816a34fc10..488314473e 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -28,6 +28,7 @@ (define-module (gnu packages agda)
   #:use-module (guix build-system emacs)
   #:use-module (guix build-system gnu)
   #:use-module (guix build-system haskell)
+  #:use-module (guix build-system copy)
   #:use-module (guix gexp)
   #:use-module (guix download)
   #:use-module (guix git-download)
@@ -190,3 +191,43 @@ (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
+  (let* ((revision "1")
+         (commit "b2e6385c1636897dbee0b10f7194376ff2c1753b"))
+    (package
+      (name "agda-stdlib")
+      (version (git-version "1.7.2" revision commit))
+      (source (origin
+                (method git-fetch)
+                (uri (git-reference
+                      (url "https://github.com/agda/agda-stdlib")
+                      (commit commit)))
+                (file-name (git-file-name name version))
+                (sha256
+                 (base32
+                  "065hf24xjpciwdrvk4isslgcgi01q0k93ql0y1sjqqvy5ryg5xmy"))))
+      (outputs '("out"))
+      (build-system copy-build-system)
+      (arguments
+       (let ((library-directory (string-append "share/agda/agda-stdlib-"
+                                               version "/")))
+         (list #:install-plan #~'(("src" #$library-directory)
+                                  ("_build" #$library-directory)
+                                  ("standard-library.agda-lib" #$library-directory))
+               #:phases #~(modify-phases %standard-phases
+                            (add-before 'install 'create-interfaces
+                              (lambda _
+                                (map (lambda (x)
+                                       (system (string-append "agda " x)))
+                                     (find-files "src" ".*\\.agda"))))))))
+      (native-inputs (list agda-2.6.3))
+      (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))))
-- 
2.39.1
Information forwarded to guix-patches@HIDDEN:
bug#61848; Package guix-patches. Full text available.

Message received at 61848 <at> debbugs.gnu.org:


Received: (at 61848) by debbugs.gnu.org; 27 Feb 2023 18:13:56 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Mon Feb 27 13:13:55 2023
Received: from localhost ([127.0.0.1]:48743 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1pWi0Z-00086a-L8
	for submit <at> debbugs.gnu.org; Mon, 27 Feb 2023 13:13:55 -0500
Received: from mail-qt1-f171.google.com ([209.85.160.171]:38825)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <yewscion@HIDDEN>) id 1pWi0V-000862-Nl
 for 61848 <at> debbugs.gnu.org; Mon, 27 Feb 2023 13:13:52 -0500
Received: by mail-qt1-f171.google.com with SMTP id c18so7659584qte.5
 for <61848 <at> debbugs.gnu.org>; Mon, 27 Feb 2023 10:13:51 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112;
 h=content-transfer-encoding:mime-version:references:in-reply-to
 :message-id:date:subject:cc:to:from:from:to:cc:subject:date
 :message-id:reply-to;
 bh=INsOAIZLGWt41XrbdfaskJM0shDEs3nNVePQwfORvBA=;
 b=Pya5lFhjWgyzxkge/bI1H2JHB+P1sa4IUIuj4vaC2MNGeSXCa5mYPg0cLR68K65V2r
 PN+mK1rJ/UcTZWTkfiqKYS78Ad+yKLLs+cCWG64MO38Tg345I1JJVZaRDKxZ+8Z/ZiHd
 cizAw+T3qSxEwTkp1X+WJ/+n6yseEF6gmpNsYOPsPU7qGC/DF65srWsUv0OIvsqgVpiK
 BJQ2B8QlL1F1AWay7QqW01LizfdkoN9FeVOcy/L0I+dWPxe/SPGYSAcg8rOAv9smPxMv
 l5DnAlNkcYTzzWT+XFQQft+mXuF9lESLG6Jbqxr8IcYQHKfXPMgVkr9T/ewyvbpRn2rG
 dRIg==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=1e100.net; s=20210112;
 h=content-transfer-encoding:mime-version:references:in-reply-to
 :message-id:date:subject:cc:to:from:x-gm-message-state:from:to:cc
 :subject:date:message-id:reply-to;
 bh=INsOAIZLGWt41XrbdfaskJM0shDEs3nNVePQwfORvBA=;
 b=YbNxxtn075sbWfH0SYiHAkDVJco3oU+OUdB/r2pxsi0mEsbYaU09DxirtaJ5lMJ/HC
 rtHHH677SQ/5zgNrykCGalmMq+61znyfWcyC4GPfGynPOtSWLN8xAA5ZP4nfB3L3WpmP
 MmHUrrbwEcAsfuc99HQdNzjETODKW6MvAEF5MHqPRKV3XB68Z8nhDzCSm2BPk3vx3Jl8
 Uy0/QjHSHea4X634opgaaE9PsqTWKP/Mkf2mMGA9LHrDx6ooHPQhqlF0wZKoYhbt/1rI
 TvGfnXOt4KYJN+3Ss/0NK9oydMu6pnWkIOYkMjxme5QyVFC59ZcmQpp3EJ7YGNc7fEL9
 hzBQ==
X-Gm-Message-State: AO0yUKWxgffSeElbUO8ReR/2L8svZq+FLtlKZGPt45HEHF/bKE0B+BXR
 hut52Aorer3QEDq94GO7lQ+80+Hth/g=
X-Google-Smtp-Source: AK7set/5C1w8xJxCSiQheCezb+Qcex0IJCaacIfbwmxHQ9CltcZE44pF5GUaTUudPkoELvCDz6Ij9Q==
X-Received: by 2002:a05:622a:1106:b0:3bf:c38c:1d7a with SMTP id
 e6-20020a05622a110600b003bfc38c1d7amr556590qty.1.1677521625973; 
 Mon, 27 Feb 2023 10:13:45 -0800 (PST)
Received: from gmail.com (ec2-3-210-134-10.compute-1.amazonaws.com.
 [3.210.134.10]) by smtp.gmail.com with ESMTPSA id
 5-20020a05620a078500b0073bb0ef3a8esm5340189qka.21.2023.02.27.10.13.45
 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256);
 Mon, 27 Feb 2023 10:13:45 -0800 (PST)
From: Christopher Rodriguez <yewscion@HIDDEN>
To: 61848 <at> debbugs.gnu.org
Subject: [[PATCH] 3/4] gnu/packages/agda.scm: Add emacs-agda2-mode v2.6.3.
Date: Mon, 27 Feb 2023 13:13:22 -0500
Message-Id: <20230227181323.21387-3-yewscion@HIDDEN>
X-Mailer: git-send-email 2.39.1
In-Reply-To: <20230227181323.21387-1-yewscion@HIDDEN>
References: <20230227181323.21387-1-yewscion@HIDDEN>
MIME-Version: 1.0
Content-Transfer-Encoding: 8bit
X-Spam-Score: 0.0 (/)
X-Debbugs-Envelope-To: 61848
Cc: Christopher Rodriguez <yewscion@HIDDEN>
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)

Signed-off-by: Christopher Rodriguez <yewscion@HIDDEN>
---
 gnu/packages/agda.scm | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 7089ba5e93..816a34fc10 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -133,6 +133,22 @@ (define-public emacs-agda2-mode
     (description "This Emacs mode enables interactive development with
 Agda.  It also aids the input of Unicode characters.")))
 
+(define-public emacs-agda2-mode-2.6.3
+  (package
+    (inherit agda-2.6.3)
+    (name "emacs-agda2-mode")
+    (build-system emacs-build-system)
+    (inputs '())
+    (arguments
+     `(#:phases (modify-phases %standard-phases
+                  (add-after 'unpack 'enter-elisp-dir
+                    (lambda _
+                      (chdir "src/data/emacs-mode") #t)))))
+    (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.")))
+
 (define-public agda-ial
   (package
     (name "agda-ial")
-- 
2.39.1
Information forwarded to guix-patches@HIDDEN:
bug#61848; Package guix-patches. Full text available.

Message received at 61848 <at> debbugs.gnu.org:


Received: (at 61848) by debbugs.gnu.org; 27 Feb 2023 18:13:51 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Mon Feb 27 13:13:51 2023
Received: from localhost ([127.0.0.1]:48739 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1pWi0V-00086F-CR
	for submit <at> debbugs.gnu.org; Mon, 27 Feb 2023 13:13:51 -0500
Received: from mail-qt1-f181.google.com ([209.85.160.181]:36575)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <yewscion@HIDDEN>) id 1pWi0T-00085z-I0
 for 61848 <at> debbugs.gnu.org; Mon, 27 Feb 2023 13:13:49 -0500
Received: by mail-qt1-f181.google.com with SMTP id l13so7703377qtv.3
 for <61848 <at> debbugs.gnu.org>; Mon, 27 Feb 2023 10:13:49 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=gmail.com; s=20210112; t=1677521624;
 h=content-transfer-encoding:mime-version:references:in-reply-to
 :message-id:date:subject:cc:to:from:from:to:cc:subject:date
 :message-id:reply-to;
 bh=YO+dRA2/OKzCx6weu1cjxI/6IYmYkg3E6Ix69VF4quQ=;
 b=kPyJqTs8cfxZ8s64mGT8H8aqk04sLWQf4/nhqzcZOf+ONM74lvQIhyVAJggYx8lay7
 7jwlo4h9GUgpNi8P3g8GYJOuMN78vPu8eeiqXFLWF/fBUOXJP9vd09Z1CmwjV7zzdmlD
 ViFysPRmkoeJ7oK5tC/SWQEFIpI/8/Tv3MIdqw37CuaQAN5/pKaBFhjX0EJIcxAo58KX
 JT87bGjUTVx4qVzgtptYzEEcA+DYUGctEB1wcQ3SFQ3PJJkmte6s5BmSrRuAERao3DVX
 khg7uaXDz+ayUUFv4SJ0Si99wVwLJPS3pxnum6s4HfWITTtInLnIw4EJW50+46/E3EPR
 OqnQ==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=1e100.net; s=20210112; t=1677521624;
 h=content-transfer-encoding:mime-version:references:in-reply-to
 :message-id:date:subject:cc:to:from:x-gm-message-state:from:to:cc
 :subject:date:message-id:reply-to;
 bh=YO+dRA2/OKzCx6weu1cjxI/6IYmYkg3E6Ix69VF4quQ=;
 b=ea00VK5CVtu+1Xj9CDhsGvP1boHrJQ/+UUs2llecg7guUeSGVkP2oxlf8NN9avx3Sk
 yrvCKpUv9x+Tp3wS7V9IN5rpHUggWah2Ghj0S/yBmwYTeVW3FX2Nieq3xoykQRU7XvyE
 cQ7cBOzPCRmu+1CKn5weufMzXdkpYFI0yw7cCWC1MxnK/wE1DJNXubRLtbuRMgx3NDOX
 LUmQELmtf5s6XQMWw8CTzsdTvoEeWapy7cKti9iy6NDayHYH6ljRCbEKdG4DCvoDwNZt
 GHSevglU7by8GPYVVRpCivEcA7VKs2X72l1fYlBxU2MbnU8ZqS2Bko3GON95RGDxMLJa
 cQGA==
X-Gm-Message-State: AO0yUKUXYujVBoWjgMwxO9uMmqlcPS3Is9krsftv7qAumiGmyMcZnxzi
 NJ6PX8FcxTfOtxgrBnTsRBfoXCHf1u0=
X-Google-Smtp-Source: AK7set/yAWYW8jSrm+dQqp7rB+oG1rcqTarznuV26YPag+VCjF00o2IWvIbUFXPo0Y3sFMVliMKMfw==
X-Received: by 2002:a05:622a:15d4:b0:3b9:a4d4:7f37 with SMTP id
 d20-20020a05622a15d400b003b9a4d47f37mr400133qty.3.1677521623820; 
 Mon, 27 Feb 2023 10:13:43 -0800 (PST)
Received: from gmail.com (ec2-3-210-134-10.compute-1.amazonaws.com.
 [3.210.134.10]) by smtp.gmail.com with ESMTPSA id
 g23-20020ac87757000000b003b860983973sm4957032qtu.60.2023.02.27.10.13.43
 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256);
 Mon, 27 Feb 2023 10:13:43 -0800 (PST)
From: Christopher Rodriguez <yewscion@HIDDEN>
To: 61848 <at> debbugs.gnu.org
Subject: [[PATCH] 2/4] gnu/packages/agda.scm: Add agda v2.6.3.
Date: Mon, 27 Feb 2023 13:13:21 -0500
Message-Id: <20230227181323.21387-2-yewscion@HIDDEN>
X-Mailer: git-send-email 2.39.1
In-Reply-To: <20230227181323.21387-1-yewscion@HIDDEN>
References: <20230227181323.21387-1-yewscion@HIDDEN>
MIME-Version: 1.0
Content-Transfer-Encoding: 8bit
X-Spam-Score: 0.0 (/)
X-Debbugs-Envelope-To: 61848
Cc: Christopher Rodriguez <yewscion@HIDDEN>
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)

Signed-off-by: Christopher Rodriguez <yewscion@HIDDEN>
---
 gnu/packages/agda.scm | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 7128a3f108..7089ba5e93 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -104,6 +104,19 @@ (define-public agda
     ;; source files are BSD-3.  See LICENSE for details.
     (license (list license:expat license:bsd-3))))
 
+(define-public agda-2.6.3
+  (package
+    (inherit agda)
+    (version "2.6.3")
+    (source (origin
+              (method url-fetch)
+              (uri (hackage-uri "Agda" version))
+              (sha256
+               (base32
+                "05k0insn1c2dbpddl1slcdn972j8vgkzzy870yxl43j75j0ckb5y"))))
+    (inputs (modify-inputs (package-inputs agda)
+              (append ghc-vector-hashtables)))))
+
 (define-public emacs-agda2-mode
   (package
     (inherit agda)
-- 
2.39.1
Information forwarded to guix-patches@HIDDEN:
bug#61848; Package guix-patches. Full text available.

Message received at 61848 <at> debbugs.gnu.org:


Received: (at 61848) by debbugs.gnu.org; 27 Feb 2023 18:13:43 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Mon Feb 27 13:13:43 2023
Received: from localhost ([127.0.0.1]:48736 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1pWi0N-00085q-0T
	for submit <at> debbugs.gnu.org; Mon, 27 Feb 2023 13:13:43 -0500
Received: from mail-qt1-f172.google.com ([209.85.160.172]:41921)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <yewscion@HIDDEN>) id 1pWi0K-00085X-AO
 for 61848 <at> debbugs.gnu.org; Mon, 27 Feb 2023 13:13:42 -0500
Received: by mail-qt1-f172.google.com with SMTP id c3so3370806qtc.8
 for <61848 <at> debbugs.gnu.org>; Mon, 27 Feb 2023 10:13:40 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=gmail.com; s=20210112; t=1677521614;
 h=content-transfer-encoding:mime-version:message-id:date:subject:cc
 :to:from:from:to:cc:subject:date:message-id:reply-to;
 bh=0WtFNHGkBpu4GLPGDZR8E9iXpQd0aV+V65zjcC2nE2Y=;
 b=A4gZwg0KqMpUgWP4I/RiUqQrhYFFJd/O6eWvaDAm1dlcZl1UkFlXB8O7quT74iLNh1
 SJQUeXwg7Xr3EQgdCBqNtLdaQToYDntSGX8ZyRzIiwAoXkgbHZ5mAMd+OGJ3qMpKHBdT
 9Lz+f9k/oPlMEndus8DUdriT4A3aYOCWQXvPA5LeuDzUxohZu49Fkw1JdE3GEcmna5jj
 9b+NsIQvOIrYm9eb/GwE+fG8PdVlmUApD32zU42Kpxx9hCXatQOf/sUQTKZIBHCrfaCx
 7+j2PBlwrNNpZxYeT6I1lwTD+QO21sZHqo4a9bBWidx0P8CP1qBiDNm4m7MO8DxWbH+D
 +gKA==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=1e100.net; s=20210112; t=1677521614;
 h=content-transfer-encoding:mime-version:message-id:date:subject:cc
 :to:from:x-gm-message-state:from:to:cc:subject:date:message-id
 :reply-to;
 bh=0WtFNHGkBpu4GLPGDZR8E9iXpQd0aV+V65zjcC2nE2Y=;
 b=dmaY7cZMCfx9BYhh7EYAHHJM5g4/m5IrZjUyn6cGAP/sQqppzJHivj+hQV+WCWCmSx
 ecsz9y8JfSijuOi5Mdue+6ZazAgmG5KDV5ubGWckNRnPIBsAsM3ovtXga7EaVjZ1mV9G
 JgGxvkfkx5D+a4paMIblZqNCl85Tg7tFZmgbFnMNZ7FWBoLUtYxMbSiVsjEu/+zv0XQQ
 l91k3sNGgTVZurTmPuaI5jKVkh0RhzDPuQ/HR7nZw+FZK72JYXWoEO6HUfoBKXVZD+ze
 32c4W+iQS4nsr9ncnonoaFIyrrOd6Z51bBoC9NKCF1NGS/e4ChqL4itOh41D1kRozKHc
 aGRA==
X-Gm-Message-State: AO0yUKUS5YKOjja0K0uUucuDpiApE5bPk0ASeU8XDVn2dzjxZ4tzwfdt
 TM1tgsamvx8pGxCAMJ0k4rTYYECnSqA=
X-Google-Smtp-Source: AK7set8fih7r4ouAfZ2g0Dw71qoUfU2gKOD+5RfqXnHuY/Rb82uRC94uB4MV5aYls5FBZlRiLiJ3BQ==
X-Received: by 2002:a05:622a:18a1:b0:3bf:a3d0:9023 with SMTP id
 v33-20020a05622a18a100b003bfa3d09023mr301221qtc.5.1677521614492; 
 Mon, 27 Feb 2023 10:13:34 -0800 (PST)
Received: from gmail.com (ec2-3-210-134-10.compute-1.amazonaws.com.
 [3.210.134.10]) by smtp.gmail.com with ESMTPSA id
 e22-20020ac84b56000000b003b646123691sm5045144qts.31.2023.02.27.10.13.34
 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256);
 Mon, 27 Feb 2023 10:13:34 -0800 (PST)
From: Christopher Rodriguez <yewscion@HIDDEN>
To: 61848 <at> debbugs.gnu.org
Subject: [[PATCH] 1/4] gnu/packages/haskell-xyz.scm: Add ghc-vector-hashtables.
Date: Mon, 27 Feb 2023 13:13:20 -0500
Message-Id: <20230227181323.21387-1-yewscion@HIDDEN>
X-Mailer: git-send-email 2.39.1
MIME-Version: 1.0
Content-Transfer-Encoding: 8bit
X-Spam-Score: 0.0 (/)
X-Debbugs-Envelope-To: 61848
Cc: Christopher Rodriguez <yewscion@HIDDEN>
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)

Signed-off-by: Christopher Rodriguez <yewscion@HIDDEN>
---
 gnu/packages/haskell-xyz.scm | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/gnu/packages/haskell-xyz.scm b/gnu/packages/haskell-xyz.scm
index b6c3a71045..44d58d83e7 100644
--- a/gnu/packages/haskell-xyz.scm
+++ b/gnu/packages/haskell-xyz.scm
@@ -14033,6 +14033,29 @@ (define-public ghc-pointed
      "This Haskell library provides pointed and copointed data types.")
     (license license:bsd-3)))
 
+(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)
+    (properties '((upstream-name . "vector-hashtables")))
+    (inputs (list ghc-primitive ghc-vector ghc-hashable ghc-hspec-discover))
+    (native-inputs (list ghc-hspec ghc-quickcheck ghc-quickcheck-instances))
+    (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).  See
+\"Data.Vector.Hashtables\" for documentation.")
+    (license license:bsd-3)))
+
+
 (define-public ghc-vector-instances
   (package
     (name "ghc-vector-instances")
-- 
2.39.1
Information forwarded to guix-patches@HIDDEN:
bug#61848; Package guix-patches. Full text available.

Message received at submit <at> debbugs.gnu.org:


Received: (at submit) by debbugs.gnu.org; 27 Feb 2023 18:11:09 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Mon Feb 27 13:11:09 2023
Received: from localhost ([127.0.0.1]:48731 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1pWhxt-00081Q-H6
	for submit <at> debbugs.gnu.org; Mon, 27 Feb 2023 13:11:09 -0500
Received: from lists.gnu.org ([209.51.188.17]:37688)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <yewscion@HIDDEN>) id 1pWhxn-00081E-4R
 for submit <at> debbugs.gnu.org; Mon, 27 Feb 2023 13:11:08 -0500
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 <yewscion@HIDDEN>)
 id 1pWhxm-0002Lh-90
 for guix-patches@HIDDEN; Mon, 27 Feb 2023 13:11:02 -0500
Received: from mail-qv1-xf32.google.com ([2607:f8b0:4864:20::f32])
 by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
 (Exim 4.90_1) (envelope-from <yewscion@HIDDEN>)
 id 1pWhxk-00087z-S1
 for guix-patches@HIDDEN; Mon, 27 Feb 2023 13:11:02 -0500
Received: by mail-qv1-xf32.google.com with SMTP id jo29so5102238qvb.0
 for <guix-patches@HIDDEN>; Mon, 27 Feb 2023 10:11:00 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=gmail.com; s=20210112; t=1677521459;
 h=content-transfer-encoding:mime-version:message-id:date:subject:cc
 :to:from:from:to:cc:subject:date:message-id:reply-to;
 bh=D0xSeSFl3rGMEm5O/c4gbC1c9VVVgZrU41xy4TF8bR8=;
 b=kXzIF+qhvoApJRiZAsv6u+xDSWH8h7jDdL0VCeFuCYwokl2F4E0kd1leZfgaHFcxjQ
 xs5c+vk9NASV/XOvuLZ9b6jDFQkq8NsQy+eEd09P6pAqPFAUYe1qajt3BnVUTgPzhEMh
 +gt4T5a1o0AgbgF2U+7eeFLeEw9PZgKQyq1JgRBRKHUViIEksJTEeQAKmsq4xopCjLX6
 y3wNrNdawSUDl/VQu2pdrubMX4583OYLSqhR5zR86NcdBOQdAObr/jTTVeOO17/kN3Tt
 L6QuLunzFOXHzWY66gvl1zXzefgvDkL5dK5tBjz0H0/HRItSyxuN7IntP+GdYsvKVfAn
 dgHA==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=1e100.net; s=20210112; t=1677521459;
 h=content-transfer-encoding:mime-version:message-id:date:subject:cc
 :to:from:x-gm-message-state:from:to:cc:subject:date:message-id
 :reply-to;
 bh=D0xSeSFl3rGMEm5O/c4gbC1c9VVVgZrU41xy4TF8bR8=;
 b=AQAphXeBqjz0ukhtOCC0OWkg3kN79xh9+Qkt435KKQevwXeicyEP8bke4J2bE1oLVz
 l+CE4Cxlwyt4XjJ8XvuXZg48gEhKZLfiicfSuVe2cO+P1TY7bRrzPnymkbUwI773IJhd
 BtH5Xf4dvjNHxH6CbRHOHWCNoTBB7CYHOFTLKFyid2X1dFCetm1Mm+PJjd5INek/cNaS
 784fbDfO8v/NRF4dXtcI8puVJFZB743tQrpjgWKeSM9vRpM4PgEuLC+BCb8ITKnK4mnO
 Ww7gcM6CdvbiefdOJrVDQtwAwfZanR6Oa0UnYUw1OW9c5IYVD95F9kBCpdw4MJWcxb9s
 J17w==
X-Gm-Message-State: AO0yUKXyNdFXNYdal/Usp7JIYmBYzSp7DB/JI2jXqc7y3hZNUHcGQ3Px
 qg6xkvmMiIep8lzVLykDXv3vbpSo53M=
X-Google-Smtp-Source: AK7set98dsq8ZfFz6xBOkQeT5r4UKu/vnLu7afN7J23rmJDUfczaG+26OuENIaEc3iYQlkobMkYPhg==
X-Received: by 2002:a0c:9c0e:0:b0:56e:89b9:9a92 with SMTP id
 v14-20020a0c9c0e000000b0056e89b99a92mr818474qve.0.1677521458959; 
 Mon, 27 Feb 2023 10:10:58 -0800 (PST)
Received: from gmail.com (ec2-3-210-134-10.compute-1.amazonaws.com.
 [3.210.134.10]) by smtp.gmail.com with ESMTPSA id
 s72-20020a37454b000000b007417e60f621sm5290494qka.126.2023.02.27.10.10.58
 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256);
 Mon, 27 Feb 2023 10:10:58 -0800 (PST)
From: Christopher Rodriguez <yewscion@HIDDEN>
To: guix-patches@HIDDEN
Subject: [[PATCH] 0/4] Agda Update and Standard Library
Date: Mon, 27 Feb 2023 13:10:55 -0500
Message-Id: <20230227181055.21133-1-yewscion@HIDDEN>
X-Mailer: git-send-email 2.39.1
MIME-Version: 1.0
Content-Transfer-Encoding: 8bit
Received-SPF: pass client-ip=2607:f8b0:4864:20::f32;
 envelope-from=yewscion@HIDDEN; helo=mail-qv1-xf32.google.com
X-Spam_score_int: -20
X-Spam_score: -2.1
X-Spam_bar: --
X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
 DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001,
 RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001,
 SPF_PASS=-0.001 autolearn=ham autolearn_force=no
X-Spam_action: no action
X-Spam-Score: -1.3 (-)
X-Debbugs-Envelope-To: submit
Cc: Christopher Rodriguez <yewscion@HIDDEN>
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -2.3 (--)

Hello all,

This patch series adds the option to install agda v2.6.3, and the current
version of the standard library alongside it.

Salient Points:

* Agda v2.6.3 requires ghc-vector-hashtables to build.

* As v2.6.2.2 is an LTS on Stackage, v2.6.3 is implemented as a variant.

* Because of this, a variant of emacs-agda2-mode was created with the same
  version number.

* agda-stdlib needs to be precompiled in order to be usable due to limitations
  in the Agda tooling ecosystem (no way to specify a different default build
  directory aside from either _build or alongside the source, both of which
  are read-only. However, they are also not going to change post-install, so
  while the compilation takes a while it is merely a prerequisite to using the
  library, and not a blocker). I conferred with someone on #agda, and it seems
  this is how Nix does it, mostly (they opt for the --local-interfaces option,
  which makes all interfaces live next to their source files, instead of in a
  dedicated, versioned _build directory, which is the default and what this
  patch does).

Christopher Rodriguez (4):
  gnu/packages/haskell-xyz.scm: Add ghc-vector-hashtables.
  gnu/packages/agda.scm: Add agda v2.6.3.
  gnu/packages/agda.scm: Add emacs-agda2-mode v2.6.3.
  gnu/packages/agda.scm: Add agda-stdlib v1.7.2.

 gnu/packages/agda.scm        | 70 ++++++++++++++++++++++++++++++++++++
 gnu/packages/haskell-xyz.scm | 23 ++++++++++++
 2 files changed, 93 insertions(+)

-- 
2.39.1
Acknowledgement sent to Christopher Rodriguez <yewscion@HIDDEN>:
New bug report received and forwarded. Copy sent to guix-patches@HIDDEN. Full text available.
Report forwarded to guix-patches@HIDDEN:
bug#61848; Package guix-patches. Full text available.
Please note: This is a static page, with minimal formatting, updated once a day.
Click here to see this page with the latest information and nicer formatting.
Last modified: Sun, 30 Apr 2023 11:30:02 UTC

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997 nCipher Corporation Ltd, 1994-97 Ian Jackson.