From patchwork Sun Apr 30 10:53:17 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Josselin Poiret X-Patchwork-Id: 49707 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 1D77427BBEA; Sun, 30 Apr 2023 11:55:28 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,FROM_SUSPICIOUS_NTLD,MAILING_LIST_MULTI,PDS_OTHER_BAD_TLD, RCVD_IN_MSPIKE_H2,SPF_HELO_PASS,URIBL_BLOCKED autolearn=no autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 3BC4C27BBE2 for ; Sun, 30 Apr 2023 11:55:26 +0100 (BST) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1pt4h0-0002vV-8q; Sun, 30 Apr 2023 06:54:10 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1pt4gy-0002tX-NE for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:08 -0400 Received: from debbugs.gnu.org ([209.51.188.43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1pt4gu-0002UM-Sf for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:08 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1pt4gu-0000W5-O3 for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:04 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#61915] [PATCH v2 07/13] gnu: agda: Add AGDA_LIBDIRS search-path. Resent-From: Josselin Poiret Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 30 Apr 2023 10:54:04 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 61915 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Received: via spool by 61915-submit@debbugs.gnu.org id=B61915.16828520371880 (code B ref 61915); Sun, 30 Apr 2023 10:54:04 +0000 Received: (at 61915) by debbugs.gnu.org; 30 Apr 2023 10:53:57 +0000 Received: from localhost ([127.0.0.1]:37352 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gm-0000UE-JF for submit@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:57 -0400 Received: from jpoiret.xyz ([206.189.101.64]:53234) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gS-0000SP-Aa for 61915@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:37 -0400 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id 5E634185309; Sun, 30 Apr 2023 10:53:34 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1682852014; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=mmqWKWO6LbU0Z0KH0b+zcEI+HiJdrSTIf5vVIe7NfEQ=; b=HA17wlQi/uF016gqVZ325klZIOYfmt3BsGKAlQw8qXFSA4Y1gM2jB9TEd9+h1vyr9Rw62M 8WCQONP+BYd8U/opM2V16KMs8/T3GGah7nil7dADi2KqjYXq7IDv4znqaG0zpejm+0AlPn 5Ymop+xO3FToMFJ3SSilERWpFv2Bdo2JtCGS5tJ3jxZPNto5kKT4+M3/o/TWNRO5yawXvm vG5+lmKxynCOYShirkCuLzGfFa0ApWu/qp9d9tUDQQ8cydjmR5RZuOlB+g8ZKS4IGnMVpm w7nMm5Qhq7a5zQjZjjaBgTgHAvD88ostS6pca7lfad3JSED876uVn3GEH0ZvQA== Date: Sun, 30 Apr 2023 12:53:17 +0200 Message-Id: <7d567a3e6da787aa9757c0f265469393dde01833.1682851600.git.dev@jpoiret.xyz> In-Reply-To: References: MIME-Version: 1.0 X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Reply-to: Josselin Poiret X-ACL-Warn: , Josselin Poiret via Guix-patches X-Patchwork-Original-From: Josselin Poiret via Guix-patches via From: Josselin Poiret Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches From: Josselin Poiret * gnu/packages/patches/agda-libdirs-env-variable.patch: New patch. * gnu/local.mk (dist_patch_DATA): Register it. * gnu/packages/agda.scm (agda): Patch agda, and add search path. --- gnu/local.mk | 1 + gnu/packages/agda.scm | 10 +++- .../patches/agda-libdirs-env-variable.patch | 49 +++++++++++++++++++ 3 files changed, 59 insertions(+), 1 deletion(-) create mode 100644 gnu/packages/patches/agda-libdirs-env-variable.patch diff --git a/gnu/local.mk b/gnu/local.mk index 1a84e5b499..712649c5fc 100644 --- a/gnu/local.mk +++ b/gnu/local.mk @@ -880,6 +880,7 @@ dist_patch_DATA = \ %D%/packages/patches/aegisub-icu59-include-unistr.patch \ %D%/packages/patches/aegisub-boost68.patch \ %D%/packages/patches/aegisub-make43.patch \ + %D%/packages/patches/agda-libdirs-env-variable.patch \ %D%/packages/patches/agg-am_c_prototype.patch \ %D%/packages/patches/agg-2.5-gcc8.patch \ %D%/packages/patches/akonadi-paths.patch \ diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index d94036939c..17ea5b62be 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -22,6 +22,7 @@ ;;; along with GNU Guix. If not, see . (define-module (gnu packages agda) + #:use-module (gnu packages) #:use-module (gnu packages haskell-check) #:use-module (gnu packages haskell-web) #:use-module (gnu packages haskell-xyz) @@ -50,7 +51,8 @@ (define-public agda (commit (string-append "v" version)))) (file-name (git-file-name name version)) (sha256 - (base32 "1s7zd01i8pmvi90ywx497kc07z50nah7h0fc2dn6jzb132k5sh1q")))) + (base32 "1s7zd01i8pmvi90ywx497kc07z50nah7h0fc2dn6jzb132k5sh1q")) + (patches (search-patches "agda-libdirs-env-variable.patch")))) (build-system haskell-build-system) (inputs (list ghc-aeson @@ -108,6 +110,12 @@ (define-public agda (setenv "infodir" (string-append #$output "/share/info")) (invoke "make" "install-info")))))))) + (search-paths + (list (search-path-specification + (variable "AGDA_LIBDIRS") + (files (list "lib/agda"))))) + (native-search-paths + search-paths) (home-page "https://wiki.portal.chalmers.se/agda/") (synopsis "Dependently typed functional programming language and proof assistant") diff --git a/gnu/packages/patches/agda-libdirs-env-variable.patch b/gnu/packages/patches/agda-libdirs-env-variable.patch new file mode 100644 index 0000000000..3b291358a6 --- /dev/null +++ b/gnu/packages/patches/agda-libdirs-env-variable.patch @@ -0,0 +1,49 @@ +From 457bc7438a4f0801dbf332fa2369248bddf5da0c Mon Sep 17 00:00:00 2001 +Message-Id: <457bc7438a4f0801dbf332fa2369248bddf5da0c.1678309546.git.dev@jpoiret.xyz> +From: Josselin Poiret +Date: Wed, 8 Mar 2023 18:31:52 +0100 +Subject: [PATCH] Add environment variable for library directories + +AGDA_LIBDIRS is a new environment colon-separated variable for site libraries. +Agda will look for .agda-lib files directly inside direct descendants of these. +--- + src/full/Agda/Interaction/Library.hs | 16 ++++++++++++++-- + 1 file changed, 14 insertions(+), 2 deletions(-) + +diff --git a/src/full/Agda/Interaction/Library.hs b/src/full/Agda/Interaction/Library.hs +index 09c1f2a82..774cc3e74 100644 +--- a/src/full/Agda/Interaction/Library.hs ++++ b/src/full/Agda/Interaction/Library.hs +@@ -323,13 +323,25 @@ getInstalledLibraries overrideLibFile = mkLibM [] $ do + raiseErrors' [ LibrariesFileNotFound theOverrideLibFile ] + return [] + Right file -> do +- if not (lfExists file) then return [] else do ++ siteLibDirs <- liftIO $ fromMaybe [] . fmap splitAtColon . lookup "AGDA_LIBDIRS" <$> getEnvironment ++ siteLibs <- liftIO $ concat <$> mapM findSiteLibs siteLibDirs ++ if not (lfExists file) then parseLibFiles Nothing $ nubOn snd ((0,) <$> siteLibs) else do + ls <- liftIO $ stripCommentLines <$> UTF8.readFile (lfPath file) + files <- liftIO $ sequence [ (i, ) <$> expandEnvironmentVariables s | (i, s) <- ls ] +- parseLibFiles (Just file) $ nubOn snd files ++ parseLibFiles (Just file) $ nubOn snd (files ++ fmap (0,) siteLibs) + `catchIO` \ e -> do + raiseErrors' [ ReadError e "Failed to read installed libraries." ] + return [] ++ where splitAtColon :: String -> [String] ++ splitAtColon "" = [] ++ splitAtColon str = case break (==':') str of ++ (a, _:b) -> a : splitAtColon b ++ (a, "") -> [a] ++ findSiteLibs :: String -> IO [String] ++ findSiteLibs dir = do ++ subDirs <- filterM doesDirectoryExist =<< map (dir ) <$> listDirectory dir ++ subFiles <- mapM (\dir -> map (dir ) <$> listDirectory dir) subDirs ++ return $ concatMap (filter (List.isSuffixOf ".agda-lib")) subFiles + + -- | Parse the given library files. + -- + +base-commit: 183534bc41af5a53daf685122997dc98883f2be2 +-- +2.39.1 +