From unknown Sat Jun 21 17:34:40 2025 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Mailer: MIME-tools 5.509 (Entity 5.509) Content-Type: text/plain; charset=utf-8 From: bug#61915 <61915@debbugs.gnu.org> To: bug#61915 <61915@debbugs.gnu.org> Subject: Status: [PATCH 0/4] Update Agda to 2.6.3 Reply-To: bug#61915 <61915@debbugs.gnu.org> Date: Sun, 22 Jun 2025 00:34:40 +0000 retitle 61915 [PATCH 0/4] Update Agda to 2.6.3 reassign 61915 guix-patches submitter 61915 Josselin Poiret severity 61915 normal tag 61915 patch thanks From debbugs-submit-bounces@debbugs.gnu.org Thu Mar 02 09:10:42 2023 Received: (at submit) by debbugs.gnu.org; 2 Mar 2023 14:10:42 +0000 Received: from localhost ([127.0.0.1]:56211 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pXjdq-0005Xg-Hu for submit@debbugs.gnu.org; Thu, 02 Mar 2023 09:10:42 -0500 Received: from lists.gnu.org ([209.51.188.17]:48934) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pXjdo-0005XW-VZ for submit@debbugs.gnu.org; Thu, 02 Mar 2023 09:10:41 -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 ) id 1pXjdm-00085O-K4 for guix-patches@gnu.org; Thu, 02 Mar 2023 09:10:38 -0500 Received: from jpoiret.xyz ([206.189.101.64]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1pXjdj-0000QB-F9 for guix-patches@gnu.org; Thu, 02 Mar 2023 09:10:38 -0500 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id 74E9D185320; Thu, 2 Mar 2023 14:10:31 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1677766231; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding; bh=HG2QNp6w6CatSFothhehfRmq78JSsB5KIcQE17XGEg0=; b=J+5dAst4tIRQ/XTg3EgrCw+IFDtKAt8oNUuwufui3dimsk5q7GDPZzTDcLHZlVPrY1qLlu vYRRE2GIoAVkHMOd9rk5SQ9Prjk+k4hq11qyUs41IDlZelUfY3TmUrXgVl1PyUH6PEirR4 h644whDOjMHRi8rusTMuqjGYZmuC5w55+LV8ywOJCecA5wtuFcTL0jFDJ9t9ckNElBGmTz /sJsR8p2t6i7HvVi9M9hg30U9GB6eTF0RONCWG5oeUsUuU0oZtwbbQucGTuY36CY/+PmrB IWVI5Ip2mADpRm/r1IyY6SS1TRLqk0rBhx6N3rpT7jcTOd/Mif2ID1HZdZO5Tw== From: Josselin Poiret To: guix-patches@gnu.org Subject: [PATCH 0/4] Update Agda to 2.6.3 Date: Thu, 2 Mar 2023 15:10:25 +0100 Message-Id: MIME-Version: 1.0 Content-Transfer-Encoding: 8bit Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spam-Level: **** X-Spamd-Bar: ++++ Received-SPF: pass client-ip=206.189.101.64; envelope-from=dev@jpoiret.xyz; helo=jpoiret.xyz 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, SPF_HELO_PASS=-0.001, SPF_PASS=-0.001 autolearn=ham autolearn_force=no X-Spam_action: no action X-Spam-Score: 0.6 (/) X-Debbugs-Envelope-To: submit Cc: Josselin Poiret X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -2.4 (--) Hi everyone, This should update Agda to the newly released 2.6.3 version. I also thought it would be a good idea to build the user manual as an info manual, since sphinx has a texinfo backend! This means we have to switch to git-fetch, since the manual is not available in the upstream tarballs from hackage. I don't know how problematic it is wrt. updaters and friends though. Best, Josselin Poiret (4): gnu: Add ghc-peano gnu: Add ghc-vector-hashtables gnu: agda: Update to 2.6.3 and switch to git-fetch gnu: agda: Build info manual gnu/packages/agda.scm | 35 ++++++++++++++++++++++++------ gnu/packages/haskell-xyz.scm | 41 ++++++++++++++++++++++++++++++++++++ 2 files changed, 70 insertions(+), 6 deletions(-) base-commit: 307d1b626be86ed21d48d44a131ce8490f370a17 -- 2.39.1 From debbugs-submit-bounces@debbugs.gnu.org Thu Mar 02 09:13:48 2023 Received: (at 61915) by debbugs.gnu.org; 2 Mar 2023 14:13:48 +0000 Received: from localhost ([127.0.0.1]:56220 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pXjgq-0005cy-4t for submit@debbugs.gnu.org; Thu, 02 Mar 2023 09:13:48 -0500 Received: from jpoiret.xyz ([206.189.101.64]:54728) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pXjgo-0005cj-5z for 61915@debbugs.gnu.org; Thu, 02 Mar 2023 09:13:46 -0500 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id D3A4E184D70; Thu, 2 Mar 2023 14:13:44 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1677766425; 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=U5rHgDL9/7cHJEztWHa84efRkxFESbXYTRXWOE+IdEA=; b=At6jNeXeU8lKXDuX358GHc7OR3k2WsFXUjf/gi/dtrHHr0yrjLF3Lo0gpDjHTayRhx2hhy fcdUdmm18VS0R2iZ6NPB6YQoXZpqepA0NsZ+lizXoEMSnk50KDG2X5cRqH9kPp2JPhd++k XOhJR2EKL4cVilpIsLweuIKU6+sIy3tN8HiMOrA7x51XpGrhQMB+Jz36y3tOGxMufRDQxr /QHd74gYpcrKHQaTZX42WI0WcM6v7CugxdIXBlwEaaebjpat87KnxW8IdODgAxtnTEMS+O XERgWU8GWgjmjIlhEChXD7+wtX4RbCSUBzfSSNPeeeCTeJMlF74bbIfsDCtEng== From: Josselin Poiret To: Josselin Poiret , 61915@debbugs.gnu.org Subject: [PATCH 1/4] gnu: Add ghc-peano Date: Thu, 2 Mar 2023 15:13:33 +0100 Message-Id: <2e14cdd0ab2fb7159b6536ad2286bbb1ed793010.1677685282.git.dev@jpoiret.xyz> In-Reply-To: References: MIME-Version: 1.0 Content-Transfer-Encoding: 8bit Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spamd-Bar: / X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 61915 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) * 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 b6c3a71045..e7e566fcfc 100644 --- a/gnu/packages/haskell-xyz.scm +++ b/gnu/packages/haskell-xyz.scm @@ -8579,6 +8579,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") -- 2.39.1 From debbugs-submit-bounces@debbugs.gnu.org Thu Mar 02 09:13:49 2023 Received: (at 61915) by debbugs.gnu.org; 2 Mar 2023 14:13:49 +0000 Received: from localhost ([127.0.0.1]:56224 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pXjgq-0005d4-Hq for submit@debbugs.gnu.org; Thu, 02 Mar 2023 09:13:48 -0500 Received: from jpoiret.xyz ([206.189.101.64]:54804) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pXjgp-0005cq-7X for 61915@debbugs.gnu.org; Thu, 02 Mar 2023 09:13:47 -0500 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id 6229C185320; Thu, 2 Mar 2023 14:13:46 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1677766426; 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=egpW670P+vY2duP75uNLaCQsl9BDGepdjk/CqKlWPVw=; b=VbtKuwenpTt5vSehiylG+MfeVPt8qFtRE1nb9zxdWoNHsxhewBJrlWDxFzCDZoFj5MTZyQ MP/TzlsI5HFyz05+kVeuJjtEsvuU5C2Yb/S5nlWjRxXRCoqv5cUct+dm0QtHCXiGoJniXx 2dYAdDxwFkPLKBtdWwgNudeZUsrDwEqw3HVp4s1Epp7P9OdcSjYWi1nkrPMbzpQnQa11SV J9zPYhIrWCow2d/RNIYeJ7Q8ZGVt2QL1Qxctt+gUDGdeD/ccVN7GYbyfBkjQDByk2rUs6J TjHASGdhHoM6SjtpzGidOiXDDtEzF/N+C3REHk3bfDcZN4GKsl+idEEHO6Nk7Q== From: Josselin Poiret To: Josselin Poiret , 61915@debbugs.gnu.org Subject: [PATCH 2/4] gnu: Add ghc-vector-hashtables Date: Thu, 2 Mar 2023 15:13:34 +0100 Message-Id: <19d6b531d74ba3a36971000c304851fa29e4de5f.1677685282.git.dev@jpoiret.xyz> In-Reply-To: References: MIME-Version: 1.0 Content-Transfer-Encoding: 8bit Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spamd-Bar: / X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 61915 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) * 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 e7e566fcfc..a98f8adeb0 100644 --- a/gnu/packages/haskell-xyz.scm +++ b/gnu/packages/haskell-xyz.scm @@ -13305,6 +13305,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") -- 2.39.1 From debbugs-submit-bounces@debbugs.gnu.org Thu Mar 02 09:13:50 2023 Received: (at 61915) by debbugs.gnu.org; 2 Mar 2023 14:13:50 +0000 Received: from localhost ([127.0.0.1]:56228 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pXjgr-0005dK-Vw for submit@debbugs.gnu.org; Thu, 02 Mar 2023 09:13:50 -0500 Received: from jpoiret.xyz ([206.189.101.64]:54872) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pXjgq-0005cx-3Y for 61915@debbugs.gnu.org; Thu, 02 Mar 2023 09:13:48 -0500 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id 51B94184D70; Thu, 2 Mar 2023 14:13:47 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1677766427; 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=4msAWHEg0efsQs1ZfDR+7t1FUXp6fxu8++eZ+QwrCg4=; b=ktdnykO9CkPWQd4evFmgol8M7qnw1vJTMFXt3Tfth/yfbaZwOO2uViWW14aOnUB0YuXaeZ g2TS/jqsdLCjo0FhOZaXZedHuDnfKCpNUiD8/1JRXvmi32nJ1jy3RoZneDcIzzRd6xE92C fDsSc7ZiZ6Tu3OyLJE05KHHsnjCcI8ajDi3d6ri6ab+dS8Q/+ZGEID3ZNhDEA/kX4f0wfm qnHiV1tsbj4sBcdYSKOWDXRhrKsYfm6rzMcqc5/YJYLmNE+PAz+6u+u0uyqbaCxK0s21aV ta2qgPMQe4E7esPGj86Xd2Sg5nUDcJixqMsXbevkarU7+SrVXqC7bwCvuRw0eg== From: Josselin Poiret To: Josselin Poiret , 61915@debbugs.gnu.org Subject: [PATCH 3/4] gnu: agda: Update to 2.6.3 and switch to git-fetch Date: Thu, 2 Mar 2023 15:13:35 +0100 Message-Id: <00bf60ca441527bcd53f209fc9eca0f36389b42b.1677685282.git.dev@jpoiret.xyz> In-Reply-To: References: MIME-Version: 1.0 Content-Transfer-Encoding: 8bit Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spamd-Bar: / X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 61915 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) * gnu/packages/agda.scm (agda): Update to 2.6.3, switch to fetching using git so that doc files are included, and add new dependencies ghc-peano and ghc-vector-hashtables. --- gnu/packages/agda.scm | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index 7128a3f108..1595f2cd22 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 @@ -63,11 +65,13 @@ (define-public agda ghc-monad-control ghc-murmur-hash ghc-parallel + ghc-peano ghc-regex-tdfa ghc-split ghc-strict ghc-unordered-containers ghc-uri-encode + ghc-vector-hashtables ghc-zlib)) (arguments (list #:modules `((guix build haskell-build-system) -- 2.39.1 From debbugs-submit-bounces@debbugs.gnu.org Thu Mar 02 09:13:51 2023 Received: (at 61915) by debbugs.gnu.org; 2 Mar 2023 14:13:51 +0000 Received: from localhost ([127.0.0.1]:56230 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pXjgt-0005dZ-As for submit@debbugs.gnu.org; Thu, 02 Mar 2023 09:13:51 -0500 Received: from jpoiret.xyz ([206.189.101.64]:54938) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pXjgr-0005dE-8d for 61915@debbugs.gnu.org; Thu, 02 Mar 2023 09:13:49 -0500 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id 3AEE8185320; Thu, 2 Mar 2023 14:13:48 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1677766428; 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=v3h10WzqwYTpiBL1c8ZaRcOoNOZcepwpSeEDMR3AktU=; b=BRtfLyuc90rF3fNzmCmSx7r4YrYBEcs1q62bAT81j5eJ4s74ZbtpJCdOwEwdsfMTscba62 KU21CaCeo7enWWSYCzM3NgmwD65cu1uWOJnfT12VLBPUWsd2Rnj14PaF/XdttBArKxvSSq 1uJMCLgeZOOqdFEjXW2P3b2y0OlXiaSttTNvIQ1juAZ4QWrzT6B0Ewqo2bNezoEPtOGtg1 31r+vyIJQJT3w2O0TT8q03rN5yGSKVkCtfG/JdmIWMVkTJd8lNylpsSXCyw6q296DGS0Sj UXxdtsrX5SyrhZTRbdRT/q0+ZblllphX27CMCKLKxLhiGeSsQjnedbRNxdd9BQ== From: Josselin Poiret To: Josselin Poiret , 61915@debbugs.gnu.org Subject: [PATCH 4/4] gnu: agda: Build info manual Date: Thu, 2 Mar 2023 15:13:36 +0100 Message-Id: <81be0b60a3c43f9e5a20c662734b8eba2d6f457c.1677685282.git.dev@jpoiret.xyz> In-Reply-To: References: MIME-Version: 1.0 Content-Transfer-Encoding: 8bit Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spamd-Bar: / X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 61915 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) * 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 1595f2cd22..4a157d5c39 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 texinfo) + #:use-module (gnu packages sphinx) #:use-module (guix build-system emacs) #:use-module (guix build-system gnu) #:use-module (guix build-system haskell) @@ -73,6 +77,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) @@ -89,7 +99,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") -- 2.39.1 From debbugs-submit-bounces@debbugs.gnu.org Fri Mar 03 03:52:24 2023 Received: (at submit) by debbugs.gnu.org; 3 Mar 2023 08:52:24 +0000 Received: from localhost ([127.0.0.1]:59610 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pY19L-0004Ue-PD for submit@debbugs.gnu.org; Fri, 03 Mar 2023 03:52:24 -0500 Received: from lists.gnu.org ([209.51.188.17]:36474) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pY19K-0004UX-Pt for submit@debbugs.gnu.org; Fri, 03 Mar 2023 03:52:23 -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 ) id 1pY19G-00086M-OW for guix-patches@gnu.org; Fri, 03 Mar 2023 03:52:20 -0500 Received: from mail-wm1-x32b.google.com ([2a00:1450:4864:20::32b]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1pY197-0004fX-G3 for guix-patches@gnu.org; Fri, 03 Mar 2023 03:52:13 -0500 Received: by mail-wm1-x32b.google.com with SMTP id j19-20020a05600c191300b003eb3e1eb0caso3403752wmq.1 for ; Fri, 03 Mar 2023 00:52:08 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; t=1677833527; h=mime-version:message-id:date:references:in-reply-to:subject:cc:to :from:from:to:cc:subject:date:message-id:reply-to; bh=QUVJHyX+8f9M1GGMW2PGgcseh5oStdKIbnA04tcKsTc=; b=kUXS9s61jthv6c+nTRHpXjT2uhBsMRzQcDH2y6jCKtje/KOFzEkPcHzkKLBXXc30Cj 4r4XxfewfNZZIK4QdqfMb8RhibBw7AviQKEkyJeUYWTi51m/C0C6Q8r+9rmvPsDh5IAP MiKkiw4NPRv5SlyTIwBMK4LM+Z28O7gNyzaxreugEsxVQVyAopwU5jJRsEpkiv0R6tNe 1ZO+/JAcH+m9RbBaYOtxg5ev5Pp/C1nYvjvxExwLPJiYOKOoBiZhvOaq9JWY5DSbC8Zs owZr3ZImhMMxVk8tiCzW0o1p8UGDcz8ijmxHdPN2aYHg9jn/1T4B/OZt+ghR7i2uGsee Tkrg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; t=1677833527; h=mime-version:message-id:date:references:in-reply-to:subject:cc:to :from:x-gm-message-state:from:to:cc:subject:date:message-id:reply-to; bh=QUVJHyX+8f9M1GGMW2PGgcseh5oStdKIbnA04tcKsTc=; b=cwQR/vsWSw7NCQ24cOuF0NBvxO/UdsBC0bowrQJhL7+0iBoZOS3nWCiJXVDbuF0QkD qW47YtlhUdpYfQ71ObVXX8gXbl9ySUYMPgN/uG19hziaoZXEemSff630qQ/0LJnjnGv3 t/MWMc2+n/Jv0Ui9n08TDDBEtQqNKrRqvz70Fe+1OwkdA4tt/Gz/kz6DN5Gm1cRcvle1 wJW+ZQzRP2coH1ISPwp/K61cnyhttOPc3fRktWxE40ObNvrKytzismNWL7DlY4qdBkzc 0uoyRIaNB+PKHe78XJvQVdIubThYysPQvyxq8qYW3dA6f5KqSjczmOLChKmH85Alv8ur uUxg== X-Gm-Message-State: AO0yUKWhBZfxdJCi2RBfZNEtiC5nDPYjyjZjsEFMconplBUcLcUNN3qy WCZJg6IJFHJuQHGilBZWu0k= X-Google-Smtp-Source: AK7set/sd9ubG9mH9LIsvCYBUVQtkqxprhu2DtfusxuzSV1dFq3JyQ7XEI78e1PdfoxzBTDTsVAdBQ== X-Received: by 2002:a05:600c:1d03:b0:3ea:840c:e8ff with SMTP id l3-20020a05600c1d0300b003ea840ce8ffmr902367wms.3.1677833527682; Fri, 03 Mar 2023 00:52:07 -0800 (PST) Received: from lili ([2a01:e0a:59b:9120:65d2:2476:f637:db1e]) by smtp.gmail.com with ESMTPSA id v5-20020a5d43c5000000b002c55de1c72bsm1526802wrr.62.2023.03.03.00.52.07 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 03 Mar 2023 00:52:07 -0800 (PST) From: Simon Tournier To: Josselin Poiret via Guix-patches via , 61915@debbugs.gnu.org Subject: Re: [bug#61915] [PATCH 0/4] Update Agda to 2.6.3 In-Reply-To: References: Date: Fri, 03 Mar 2023 02:30:09 +0100 Message-ID: <86wn3yd3ku.fsf@gmail.com> MIME-Version: 1.0 Content-Type: text/plain Received-SPF: pass client-ip=2a00:1450:4864:20::32b; envelope-from=zimon.toutoune@gmail.com; helo=mail-wm1-x32b.google.com X-Spam_score_int: -5 X-Spam_score: -0.6 X-Spam_bar: / X-Spam_report: (-0.6 / 5.0 requ) BAYES_00=-1.9, DATE_IN_PAST_06_12=1.543, 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=no autolearn_force=no X-Spam_action: no action X-Spam-Score: -0.2 (/) X-Debbugs-Envelope-To: submit Cc: Josselin Poiret X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.2 (-) Hi Josselin, It seems some duplicate work with #61848 [1] from Monday. Maybe the two series could be merged. WDYT? On Thu, 02 Mar 2023 at 15:10, Josselin Poiret via Guix-patches via wrote: > This should update Agda to the newly released 2.6.3 version. I also thought it > would be a good idea to build the user manual as an info manual, since sphinx > has a texinfo backend! This means we have to switch to git-fetch, since the > manual is not available in the upstream tarballs from hackage. I don't know how > problematic it is wrt. updaters and friends though. > > Best, > > Josselin Poiret (4): > gnu: Add ghc-peano > gnu: Add ghc-vector-hashtables > gnu: agda: Update to 2.6.3 and switch to git-fetch > gnu: agda: Build info manual > > gnu/packages/agda.scm | 35 ++++++++++++++++++++++++------ > gnu/packages/haskell-xyz.scm | 41 ++++++++++++++++++++++++++++++++++++ > 2 files changed, 70 insertions(+), 6 deletions(-) Well, #61848 reads, 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(+) 1: Cheers, simon From debbugs-submit-bounces@debbugs.gnu.org Fri Mar 03 11:24:51 2023 Received: (at 61915) by debbugs.gnu.org; 3 Mar 2023 16:24:51 +0000 Received: from localhost ([127.0.0.1]:33788 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pY8DC-0004zB-N8 for submit@debbugs.gnu.org; Fri, 03 Mar 2023 11:24:50 -0500 Received: from jpoiret.xyz ([206.189.101.64]:57066) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pY8D9-0004yp-PK for 61915@debbugs.gnu.org; Fri, 03 Mar 2023 11:24:48 -0500 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id 4640C185310; Fri, 3 Mar 2023 16:24:43 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1677860683; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: in-reply-to:in-reply-to:references:references; bh=tHwdunR72/LboGiMwbSdkF6ohVpNx+W9zZU/SMe63fE=; b=WQcpphaNKrAKQqlmRRYSUeB/6Uywf1N2tlo6wnOkYOKFgoxc+tLJhU/ZoZ/YC/gyZ43jxs vsMCHWBUGkExGJWIY8ecwVPqGLg7TM/spKL4P+Q7kzY8V+bNAIAIwidvLii0vsi5JuBdHy 7h7ZTowQd8k+CFGt/aZ+u8f5lNXsP8WyclNpWls4ck4EhNVCSVakdn8o+P7wggnERKz6sD fq+id7wbDtn1ucIAo9ZyEp7612SG/d7ygXriYU5YHSGX5veMKzz2ZCoJ2SMrICE7R2MFsC 7JkfPhx8t8yLYaSL84udeGlmDSqKxi1ERWHRD/spmuvsR/8lZJYFy5qrA9ZUqQ== From: Josselin Poiret To: Simon Tournier , 61915@debbugs.gnu.org Subject: Re: [bug#61915] [PATCH 0/4] Update Agda to 2.6.3 In-Reply-To: <86wn3yd3ku.fsf@gmail.com> References: <86wn3yd3ku.fsf@gmail.com> Date: Fri, 03 Mar 2023 17:24:27 +0100 Message-ID: <87pm9pref8.fsf@jpoiret.xyz> MIME-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha256; protocol="application/pgp-signature" Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spamd-Bar: / X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 61915 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 0.0 (/) --=-=-= Content-Type: text/plain Content-Transfer-Encoding: quoted-printable Hi Simon, Simon Tournier writes: > Hi Josselin, > > It seems some duplicate work with #61848 [1] from Monday. > > Maybe the two series could be merged. WDYT? My bad, completely missed this one. I'm not too familiar with the reasonning behind keeping agda@2.6.2 around in that other patchset, but I'll have a look there soon. Best, =2D-=20 Josselin Poiret --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQHEBAEBCAAuFiEEOSSM2EHGPMM23K8vUF5AuRYXGooFAmQCHzsQHGRldkBqcG9p cmV0Lnh5egAKCRBQXkC5FhcaiprUC/40/Ga1sqmlit8TPaCNckB9wtT6MX+xyanv 0fdtZAnUMLa5qG7IzFZOp9l0eEinUmjtuSp+XpMtSetW/gkGeweCGDxp6nJjZIp5 V1gCcEoRA+Y9buW0FTpkcZLTa2iZyAL1nLg6hM63OJV5RTLfsAuTriTOTIP0fNHK DG7vgPg+BcMmmidxyAB4BL310VbodkpRvYQNmoB/OaJwgTDNpgg9Ce8PIbU2JBat JQG75ZD2o4MSPEyL+KWMB4mwXQLbmKMhHFCuqDAT7PonQOCMHmL5LxN+rmV8A9r2 L/k/VYJZEtzLV+xio/xl443d9EIoXuEaeKZ8PMVQT8ZbM0ZGlSuNB/mOdDaJ0FmP ylDgf8itVGNH8i+kuiam+hq40Y2LMCfhQOOEVemJXPjPO11ck4ZuvKfmdlZtfflS U0no6m8mOsJ7lLHVe450trwdscjrCrWlsWe36wvpNbHRmlgI6XlLCStrg1U54Utr 4PZB6n76/QpZHbU+RuS9vYKrvaxbD+o= =JJ9e -----END PGP SIGNATURE----- --=-=-=-- From debbugs-submit-bounces@debbugs.gnu.org Sun Apr 30 06:53:31 2023 Received: (at 61915) by debbugs.gnu.org; 30 Apr 2023 10:53:31 +0000 Received: from localhost ([127.0.0.1]:37316 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gM-0000Rp-E2 for submit@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:31 -0400 Received: from jpoiret.xyz ([206.189.101.64]:52616) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gJ-0000RW-6w for 61915@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:29 -0400 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id ADF1F185309; Sun, 30 Apr 2023 10:53:24 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1682852005; 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=RFalj5BPRR2kWYbArPlrefi9jjbgRwek09cOU7x62Lw=; b=MdCxdUSCGvDqB+/4+rDWSh/2JeCMHwW32UXkEElxcjrwBv0zWi5BYVXfC0mXLfS3DZGUvM oMA6T+G3TCJWfMMGj2xbb2bhGR2ZpPAmNbFlTPlVz6d4PJdgYPYcAl9/5yM84s/nrEvKFw Gq7/YbswCfAmJj0qk2AM5PIzQ9wntOgbxf+CJ3ECDKlbiXYm2uo4XlnEMivbOj1x3SFnBt FCQACi103Y6ebW8slqSnibzAv+U5fcSeS6FVxfYvG2Dnw5Aol7usO6aW9qTeDS+wxku1/U xuRXRc+GDGj0TozDWcQbdE8h1tmTfX7vaOYfv5/3VnhTCeJ14sPukDYxZI9z4Q== From: Josselin Poiret To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Subject: [PATCH v2 00/13] Update agda, add build-system and libraries. Date: Sun, 30 Apr 2023 12:53:10 +0200 Message-Id: In-Reply-To: <87pm9pref8.fsf@jpoiret.xyz> References: <87pm9pref8.fsf@jpoiret.xyz> MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spamd-Bar: ++++ Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spam-Level: **** X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 61915 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) Hi everyone, Took me quite some time to get back to this, but since I need this for work and I've been using my patches on top of master to get 2.6.3 for a while now I figured I needed to properly finish this. This series does a couple of things: * Update Agda to 2.6.3, and build its manual in the info format. Note that ghc-peano is not yet needed for 2.6.3 but anyone working on HEAD would need it. * Add a search-path to Agda (AGDA_LIBDIRS) that lets agda search for libraries in these directories. This lets Guix manage Agda libraries. * Add an agda-build-system. It should be quite simple to use for simple libraries but also supports using Haskell to generate Everything.agda or similar setups, like in agda-stdlib. * Add common libraries: agda-stdlib, cubical, agda-categories, 1lab. Most of them are off recent commits, because they don't really have a proper release schedule right now (99% of the users just use git checkouts on HEAD). With these, we can just do `guix shell agda agda-categories` and directly use agda-categories, without any setup like modifying `~/.agda/libraries`. Best, Josselin Poiret (13): gnu: Add ghc-peano. gnu: Add ghc-vector-hashtables. gnu: agda: Update to 2.6.3 and switch to git-fetch. gnu: agda: Build info manual. gnu: emacs-agda2-mode: No longer inherit from agda. gnu: emacs-agda2-mode: Switch to G-Exps. gnu: agda: Add AGDA_LIBDIRS search-path. build-system/haskell: Export default-haskell. build-system: New agda-build-system. gnu: Add agda-stdlib. gnu: Add agda-categories. gnu: Add agda-cubical. gnu: Add agda-1lab. Makefile.am | 2 + doc/guix.texi | 21 ++ gnu/local.mk | 5 + gnu/packages/agda.scm | 192 ++++++++++++++++-- gnu/packages/haskell-xyz.scm | 41 ++++ .../agda-categories-bump-stdlib-version.patch | 42 ++++ ...categories-remove-incompatible-flags.patch | 31 +++ .../patches/agda-categories-use-find.patch | 31 +++ .../patches/agda-libdirs-env-variable.patch | 49 +++++ .../patches/agda-stdlib-use-runhaskell.patch | 28 +++ guix/build-system/agda.scm | 105 ++++++++++ guix/build-system/haskell.scm | 1 + guix/build/agda-build-system.scm | 110 ++++++++++ 13 files changed, 645 insertions(+), 13 deletions(-) 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 create mode 100644 gnu/packages/patches/agda-libdirs-env-variable.patch create mode 100644 gnu/packages/patches/agda-stdlib-use-runhaskell.patch create mode 100644 guix/build-system/agda.scm create mode 100644 guix/build/agda-build-system.scm base-commit: 4884ee6dd4b1694a4a502dd8058d6c61fa0c0199 -- 2.39.2 From debbugs-submit-bounces@debbugs.gnu.org Sun Apr 30 06:53:36 2023 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== From: Josselin Poiret To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Subject: [PATCH v2 02/13] gnu: Add ghc-vector-hashtables. Date: Sun, 30 Apr 2023 12:53:12 +0200 Message-Id: In-Reply-To: References: MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 61915 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) 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") -- 2.39.2 From debbugs-submit-bounces@debbugs.gnu.org Sun Apr 30 06:53:37 2023 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== From: Josselin Poiret To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Subject: [PATCH v2 01/13] gnu: Add ghc-peano. 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 Content-Transfer-Encoding: 8bit X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 61915 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) 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") -- 2.39.2 From debbugs-submit-bounces@debbugs.gnu.org Sun Apr 30 06:53:37 2023 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== From: Josselin Poiret To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Subject: [PATCH v2 03/13] gnu: agda: Update to 2.6.3 and switch to git-fetch. 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 Content-Transfer-Encoding: 8bit X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 61915 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) 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) -- 2.39.2 From debbugs-submit-bounces@debbugs.gnu.org Sun Apr 30 06:53:53 2023 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== From: Josselin Poiret To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Subject: [PATCH v2 05/13] gnu: emacs-agda2-mode: No longer inherit from agda. Date: Sun, 30 Apr 2023 12:53:15 +0200 Message-Id: In-Reply-To: References: MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 61915 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) 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 -- 2.39.2 From debbugs-submit-bounces@debbugs.gnu.org Sun Apr 30 06:53:54 2023 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== From: Josselin Poiret To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Subject: [PATCH v2 04/13] gnu: agda: Build info manual. 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 Content-Transfer-Encoding: 8bit X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 61915 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) 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") -- 2.39.2 From debbugs-submit-bounces@debbugs.gnu.org Sun Apr 30 06:53:54 2023 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== From: Josselin Poiret To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Subject: [PATCH v2 08/13] build-system/haskell: Export default-haskell. Date: Sun, 30 Apr 2023 12:53:18 +0200 Message-Id: In-Reply-To: References: MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 61915 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) 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 -- 2.39.2 From debbugs-submit-bounces@debbugs.gnu.org Sun Apr 30 06:53:57 2023 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== From: Josselin Poiret To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Subject: [PATCH v2 07/13] gnu: agda: Add AGDA_LIBDIRS search-path. 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 Content-Transfer-Encoding: 8bit X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 61915 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) 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 + -- 2.39.2 From debbugs-submit-bounces@debbugs.gnu.org Sun Apr 30 06:53:57 2023 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== From: Josselin Poiret To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Subject: [PATCH v2 06/13] gnu: emacs-agda2-mode: Switch to G-Exps. 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 Content-Transfer-Encoding: 8bit X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 61915 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) 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 -- 2.39.2 From debbugs-submit-bounces@debbugs.gnu.org Sun Apr 30 06:53:58 2023 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== From: Josselin Poiret To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Subject: [PATCH v2 09/13] build-system: New agda-build-system. Date: Sun, 30 Apr 2023 12:53:19 +0200 Message-Id: In-Reply-To: References: MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 61915 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) 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)) -- 2.39.2 From debbugs-submit-bounces@debbugs.gnu.org Sun Apr 30 06:53:58 2023 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== From: Josselin Poiret To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Subject: [PATCH v2 11/13] gnu: Add agda-categories. 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 Content-Transfer-Encoding: 8bit X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 61915 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) 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 + -- 2.39.2 From debbugs-submit-bounces@debbugs.gnu.org Sun Apr 30 06:53:59 2023 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== From: Josselin Poiret To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Subject: [PATCH v2 12/13] gnu: Add agda-cubical. Date: Sun, 30 Apr 2023 12:53:22 +0200 Message-Id: In-Reply-To: References: MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 61915 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) 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)))) -- 2.39.2 From debbugs-submit-bounces@debbugs.gnu.org Sun Apr 30 06:53:59 2023 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== From: Josselin Poiret To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Subject: [PATCH v2 13/13] gnu: Add agda-1lab. 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 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-Spamd-Bar: --- Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 61915 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) 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)))) -- 2.39.2 From debbugs-submit-bounces@debbugs.gnu.org Sun Apr 30 06:54:16 2023 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== From: Josselin Poiret To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Subject: [PATCH v2 10/13] gnu: Add agda-stdlib. 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 Content-Transfer-Encoding: 8bit X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 61915 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) 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 + -- 2.39.2 From debbugs-submit-bounces@debbugs.gnu.org Sun Apr 30 07:23:54 2023 Received: (at control) by debbugs.gnu.org; 30 Apr 2023 11:23:54 +0000 Received: from localhost ([127.0.0.1]:37398 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt59l-0001XX-KX for submit@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 ) 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 To: Christopher Rodriguez , 61848@debbugs.gnu.org Subject: Re: [bug#61848] [[PATCH] 0/4] Agda Update and Standard Library In-Reply-To: <20230227181055.21133-1-yewscion@gmail.com> References: <20230227181055.21133-1-yewscion@gmail.com> Date: Sun, 30 Apr 2023 13:23:46 +0200 Message-ID: <87bkj5ehq5.fsf@jpoiret.xyz> 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@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: control Cc: control@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" 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----- --=-=-=-- From debbugs-submit-bounces@debbugs.gnu.org Sun Jun 04 05:47:43 2023 Received: (at 61915-done) by debbugs.gnu.org; 4 Jun 2023 09:47:43 +0000 Received: from localhost ([127.0.0.1]:45074 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1q5kKs-0006qJ-R3 for submit@debbugs.gnu.org; Sun, 04 Jun 2023 05:47:43 -0400 Received: from jpoiret.xyz ([206.189.101.64]:56296) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1q5kKq-0006q3-Nd for 61915-done@debbugs.gnu.org; Sun, 04 Jun 2023 05:47:41 -0400 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id D62691852FF for <61915-done@debbugs.gnu.org>; Sun, 4 Jun 2023 09:47:39 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1685872059; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: in-reply-to:in-reply-to:references:references; bh=P7ddRN8IzLaRvflFtqleclrNm+LELsWIXxthQPHmWYs=; b=CymYgS2JxpAecYJHGdci/XB0QKETgKVs+OVEvcomQZEpBlpIzCSxvEPiibJKjoBdgzB/WW 7OpUgTL+UpGXaTgyENoGGUHwJoPYZ7COfRxnKVMUAPwH24eeI6O11N2u4F79NJVqX5oaAL tBqMc8tY0xdLKSnxuqMBhODohNWUEk2WFHI6Uw94bW/GNvNOdUNkf9/cllfwj2uc5G28dP JsLuduw1eixVBDjw4KRv6mWwc35T2EiG5xdPamVi1r1jt1WrfCKVoMyvHi7tR7oP7GDGOj 1PY2iiSBcKXJZEltC6kCO7WFiGDLSd1pJB/ofHSeHWL1eV+bH4CUGIDtmFdprg== From: Josselin Poiret To: 61915-done@debbugs.gnu.org Subject: Re: [PATCH v2 00/13] Update agda, add build-system and libraries. In-Reply-To: References: <87pm9pref8.fsf@jpoiret.xyz> Date: Sun, 04 Jun 2023 11:47:37 +0200 Message-ID: <877csjeeyu.fsf@jpoiret.xyz> 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@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 61915-done X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 0.0 (/) --=-=-= Content-Type: text/plain Content-Transfer-Encoding: quoted-printable Hi everyone, Josselin Poiret writes: > Josselin Poiret (13): > gnu: Add ghc-peano. > gnu: Add ghc-vector-hashtables. > gnu: agda: Update to 2.6.3 and switch to git-fetch. > gnu: agda: Build info manual. > gnu: emacs-agda2-mode: No longer inherit from agda. > gnu: emacs-agda2-mode: Switch to G-Exps. > gnu: agda: Add AGDA_LIBDIRS search-path. > build-system/haskell: Export default-haskell. > build-system: New agda-build-system. > gnu: Add agda-stdlib. > gnu: Add agda-categories. > gnu: Add agda-cubical. > gnu: Add agda-1lab. Pushed as e198fe4e942c58136dd4cb8ebf49cade58a8f5e3 with some additions, notably refactoring some descriptions that the linter didn't like, and updating agda-categories to the new released version, agda-cubical and agda-ial to a new commit. Best, =2D-=20 Josselin Poiret --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQHEBAEBCgAuFiEEOSSM2EHGPMM23K8vUF5AuRYXGooFAmR8XbkQHGRldkBqcG9p cmV0Lnh5egAKCRBQXkC5FhcairgPC/42AKmOd7IYeIdUSf6qBwXiqpicFqpfBi4A IVdxUwBSXBDrnpnLqSHv0mAi/yx4By7hFUw7TOJJY/ybFKY8uu2BEU8WiTTobhXm uddDnaWUSpqA0zNdU4xK7EXkf0vfRygl10W73srn2WIiuCiUK9/rRYwwN4HSDim2 Ui0BLnnwtgwRSqnzFoPmTI1kcWRYNM9B2svfqwwWMyRuUVLpX+d4nOLLaKeZpRib daZXEwGTNtKx4nz9wOeNamFUgGXkrRG8dYQ/g0P/Ae+BqASjFUfqFgDa4FokQcbO kelvxYuMO6UyWMoEuF/X7qlCS5DVmGGX7NgnOTQi0sBQ6NG41CfLMQtibad8h3cb iQRWXu6K6aFA5KqSrJniUUTnD8x5i0Clho+XZO2NwbOyvj/cHi4H85k6oHyWVU5p npaQ+0dJKx6kwrOV6FhUZbIQ/aZ+KLd0MWQfC9p52QvR7vcthDsuhHQYtJC5LbSi kTNo7oc+N/XwIT6D7/gp5yXMnggdASI= =/847 -----END PGP SIGNATURE----- --=-=-=-- From unknown Sat Jun 21 17:34:40 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Sun, 02 Jul 2023 11:24:05 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator