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

showmsg=1'>tests</a>/<a href='/guix/log/tests/guix-git-authenticate.sh?id=1da863cc3bbb212db3c54bc1956892c3be77d563&amp;showmsg=1'>guix-git-authenticate.sh</a></div><div class='content'><table class='list nowrap'><tr class='nohover'><th class='left'>Age</th><th class='left'>Commit message (<a href='/guix/log/tests/guix-git-authenticate.sh?id=1da863cc3bbb212db3c54bc1956892c3be77d563'>Collapse</a>)</th><th class='left'>Author</th></tr>
<tr class='logheader'><td><span title='2023-04-21 16:16:38 +0200'>2023-04-21</span></td><td class='logsubject'><a href='/guix/commit/tests/guix-git-authenticate.sh?id=37dd69b44511dc73eb04bdebe8d82c9a0386338e'>tests: Fix checks for expected failures.</a></td><td>Eric Bavier</td></tr>
<tr class='nohover-highlight'><td/><td colspan='3' class='logmsg'>
Addresses &lt;https://issues.guix.gnu.org/62406&gt;.

With 'set -e', a return status inverted with '!' does not cause the shell to
exit immediately.  Instead use '&amp;&amp; false' to indicate an expected failure.

* tests/guix-archive.sh, tests/guix-build-branch.sh, tests/guix-build.sh,
tests/guix-daemon.sh, tests/guix-download.sh,
tests/guix-environment-container.sh, tests/guix-environment.sh,
tests/guix-gc.sh, tests/guix-git-authenticate.sh, tests/guix-graph.sh,
tests/guix-hash.sh, tests/guix-home.sh, tests/guix-pack-relocatable.sh,
tests/guix-pack.sh, tests/guix-package-aliases.sh, tests/guix-package-net.sh,
tests/guix-package.sh, tests/guix-refresh.sh, tests/guix-shell.sh,
tests/guix-style.sh, tests/guix-system.sh: Replace uses of '! ...' with
'... &amp;&amp; false' or `test ! ...` as appropriate.

Signed-off-by: Ludovic Courtès &lt;ludo@gnu.org&gt;


</td></tr>
<tr class='logheader'><td><span title='2022-02-14 11:23:08 +0100'>2022-02-14</span></td><td class='logsubject'><a href='/guix/commit/tests/guix-git-authenticate.sh?id=ca87601dd97dd9d356409827802eb0f8a3a535f0'>git-authenticate: Ensure the target is a descendant of the introductory commit.</a></td><td>Ludovic Courtès</td></tr>
<tr class='nohover-highlight'><td/><td colspan='3' class='logmsg'>
Fixes a bug whereby authentication of a commit *not* descending from the
introductory commit could succeed, provided the commit verifies the
authorization invariant.

In the example below, A is a common ancestor of the introductory commit
I and of commit X.  Authentication of X would succeed, even though it is
not a descendant of I, as long as X is authorized according to the
'.guix-authorizations' in A:

   X   	 I
    \   /
      A

This is because, 'authenticate-repository' would not check whether X
descends from I, and the call (commit-difference X I) would return X.

In practice that only affects forks because it means that ancestors of
the introductory commit already contain a '.guix-authorizations' file.

* guix/git-authenticate.scm (authenticate-repository): Add call to
'commit-descendant?'.
* tests/channels.scm ("authenticate-channel, not a descendant of introductory commit"):
New test.
* tests/git-authenticate.scm ("authenticate-repository, target not a descendant of intro"):
New test.
* tests/guix-git-authenticate.sh: Expect earlier test to fail since
9549f0283a78fe36f2d4ff2a04ef8ad6b0c02604 is not a descendant of
$intro_commit.  Add new test targeting an ancestor of the introductory
commit, and another test targeting the v1.2.0 commit.
* doc/guix.texi (Specifying Channel Authorizations): Add a sentence.


</td></tr>