diff options
| -rw-r--r-- | gnu/local.mk | 1 | ||||
| -rw-r--r-- | gnu/packages/agda.scm | 10 | ||||
| -rw-r--r-- | gnu/packages/patches/agda-libdirs-env-variable.patch | 49 |
3 files changed, 59 insertions, 1 deletions
diff --git a/gnu/local.mk b/gnu/local.mk index 7be3cc5464..d38329ea95 100644 --- a/gnu/local.mk +++ b/gnu/local.mk @@ -885,6 +885,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 d6c2e1e231..c73c238a35 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -23,6 +23,7 @@ ;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>. (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) @@ -51,7 +52,8 @@ (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 @@ -109,6 +111,12 @@ (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 <dev@jpoiret.xyz> +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 + |