Load libraries from central location

[nomeata]

Debian packages agda and agda-stdlib. Ideally, once you run

apt install agda

you should be able to run agda -l standard-library Foo.agda.

For this to be working, agda needs to be able to look for .agda-lib files in a well-known system-wide location.

I propose (and actually have prepared the agda-stdlib package in Debian accordingly) to load all files named *.agda-lib in

/var/lib/agda

Of course other package management systems can benefit from this as well, and for example university pool rooms can setup agda this way so that users don’t have to configure stuff in ~/.agda

[nomeata]

Here is the patch I am using for now, feel free to use this or to implement it a better way:

Index: agda/src/full/Agda/Interaction/Library.hs
===================================================================
--- agda.orig/src/full/Agda/Interaction/Library.hs	2017-10-13 21:58:48.432139892 -0400
+++ agda/src/full/Agda/Interaction/Library.hs	2017-10-13 22:39:44.970695744 -0400
@@ -215,13 +215,20 @@
   -> LibM [AgdaLibFile] -- ^ Content of library files.  (Might have empty @LibName@s.)
 getInstalledLibraries overrideLibFile = mkLibM [] $ do
     file <- lift $ getLibrariesFile overrideLibFile
-    ifNotM (lift $ doesFileExist file) (return []) $ {-else-} do
+    userlibs <- ifNotM (lift $ doesFileExist file) (return []) $ {-else-} do
       ls    <- lift $ stripCommentLines <$> readFile file
       files <- lift $ sequence [ (i, ) <$> expandEnvironmentVariables s | (i, s) <- ls ]
       parseLibFiles (Just file) files
+
+    systemlibs <- ifNotM (lift $ doesDirectoryExist systemLibDir) (return []) $ do
+      files <- lift $ filter isLibFile <$> listDirectory systemLibDir
+      parseLibFiles Nothing $ zip [1..] $ map (systemLibDir </>) files
+    return $ userlibs ++ systemlibs
   `catchIO` \ e -> do
     tell [ OtherError $ unlines ["Failed to read installed libraries.", show e] ]
     return []
+  where systemLibDir = "/var/lib/agda"
+        isLibFile fn = takeExtension fn == ".agda-lib" && not ("." `List.isPrefixOf` fn)
 
 -- | Parse the given library files.
 --

[andreasabel]

Thanks! What would be suitable locations for Windows and Mac OS?

[nomeata]

Sorry, not my field of expertise. Whoever creates ready-to-use packages of the standard library for these systems might have an opinion (homebrew etc.).

[nad]

None of the predefined directories in System.Directory seem to match. Perhaps we can have a list of system directories, and let the list be empty by default. Replacing this list with something suitable is then presumably easy for those who package Agda.

If such a list is added, then I think that it should be possible to override or ignore it by using command line options.

[UlfNorell]

I'm not sure I understand exactly what you are doing here. At the moment you "install" a library by adding the path to its .agda-lib file to your libraries file (typically in ~/.agda).

With your change it looks like you should copy the .agda-lib file to the /var/lib/agda directory? How does this work with include paths? For example, the standard library library file says include: src, do you have to change that to an absolute path when copying it?

Wouldn't it make more sense to load /var/lib/agda/*/*.agda-lib, having the entire library live under /var/lib/agda?

[nomeata]

Hmm, I don’t remember all my thoughts from back then, but yeah, I think the plan was for the package maintainer to adjust the include path to be absolute when a library is installed via a system package.

Wouldn't it make more sense to load /var/lib/agda//.agda-lib, having the entire library live under /var/lib/agda?

That would work as well!