From patchwork Sun Apr 30 10:53:10 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Josselin Poiret X-Patchwork-Id: 1462 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id C8BEA27BBE9; Sun, 30 Apr 2023 11:54:22 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,FROM_SUSPICIOUS_NTLD,MAILING_LIST_MULTI,PDS_OTHER_BAD_TLD, RCVD_IN_MSPIKE_H2,SPF_HELO_PASS,URIBL_BLOCKED autolearn=no autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id D4DCC27BBE2 for ; Sun, 30 Apr 2023 11:54:21 +0100 (BST) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1pt4gu-0002sd-4i; Sun, 30 Apr 2023 06:54:04 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1pt4gs-0002sB-JM for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:02 -0400 Received: from debbugs.gnu.org ([209.51.188.43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1pt4gs-0002Te-BW for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1pt4gr-0000VD-V3 for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:01 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#61915] [PATCH v2 00/13] Update agda, add build-system and libraries. Resent-From: Josselin Poiret Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 30 Apr 2023 10:54:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 61915 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Received: via spool by 61915-submit@debbugs.gnu.org id=B61915.16828520111735 (code B ref 61915); Sun, 30 Apr 2023 10:54:01 +0000 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== 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 X-Spamd-Bar: ++++ Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Reply-to: Josselin Poiret X-ACL-Warn: , Josselin Poiret via Guix-patches X-Patchwork-Original-From: Josselin Poiret via Guix-patches via From: Josselin Poiret Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches 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