Fix agda#4526, agda#4613: Add .agda-lib for builtins

By default Agda tries to traverse the filesystem upwards until it hits
the filesystem root or it finds a .agda-lib file. This traversal can be
very slow if the Agda builtin sources are contained in a big directory
(e.g. on NixOS where /nix/store, inside which Agda is stored, often
contains ten to hundred thousand files). Hence we introduce the
.agda-lib file to prevent this traversal for the Agda builtins.

Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>

Agda.cabal

@@ -108,6 +108,7 @@ data-files:
     JS/agda-rts.amd.js
     latex/agda.sty
     latex/postprocess-latex.pl
+    lib/prim/agda-builtins.agda-lib
     lib/prim/Agda/Builtin/Bool.agda
     lib/prim/Agda/Builtin/Char.agda
     lib/prim/Agda/Builtin/Char/Properties.agda

Setup.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE NondecreasingIndentation #-}
 
+import Data.List
 import Data.Maybe
 
 import Distribution.Simple
@@ -32,7 +33,7 @@ userhooks = simpleUserHooks
 -- Install and copy hooks are default, but amended with .agdai files in data-files.
 instHook' :: PackageDescription -> LocalBuildInfo -> UserHooks -> InstallFlags -> IO ()
 instHook' pd lbi hooks flags = instHook simpleUserHooks pd' lbi hooks flags where
-  pd' = pd { dataFiles = concatMap expandAgdaExt $ dataFiles pd }
+  pd' = pd { dataFiles = concatMap (expandAgdaExt pd) $ dataFiles pd }
 
 -- Andreas, 2020-04-25, issue #4569: defer 'generateInterface' until after
 -- the library has been copied to a destination where it can be found.
@@ -48,7 +49,7 @@ copyHook' pd lbi hooks flags = do
     copyHook simpleUserHooks pd' lbi hooks flags
   where
   pd' = pd
-    { dataFiles = concatMap expandAgdaExt $ dataFiles pd
+    { dataFiles = concatMap (expandAgdaExt pd) $ dataFiles pd
       -- Andreas, 2020-04-25, issue #4569:
       -- I tried clearing some fields to avoid copying again.
       -- However, cabal does not like me messing with the PackageDescription.
@@ -66,12 +67,22 @@ copyHook' pd lbi hooks flags = do
     }
 
 -- Used to add .agdai files to data-files
-expandAgdaExt :: FilePath -> [FilePath]
-expandAgdaExt fp | takeExtension fp == ".agda" = [ fp, toIFile fp ]
-                 | otherwise                   = [ fp ]
+expandAgdaExt :: PackageDescription -> FilePath -> [FilePath]
+expandAgdaExt pd fp | takeExtension fp == ".agda" = [ fp, toIFile pd fp ]
+                    | otherwise                   = [ fp ]
 
-toIFile :: FilePath -> FilePath
-toIFile file = replaceExtension file ".agdai"
+version :: PackageDescription -> String
+version = intercalate "." . map show . versionNumbers . pkgVersion . package
+
+projectRoot :: PackageDescription -> FilePath
+projectRoot pd = takeDirectory agdaLibFile where
+  [agdaLibFile] = filter ((".agda-lib" ==) . takeExtension) $ dataFiles pd
+
+toIFile :: PackageDescription -> FilePath -> FilePath
+toIFile pd file = buildDir </> fileName where
+  root = projectRoot pd
+  buildDir = root </> "_build" </> version pd </> "agda"
+  fileName = makeRelative root $ replaceExtension file ".agdai"
 
 -- Andreas, 2019-10-21, issue #4151:
 -- skip the generation of interface files with program suffix "-quicker"
@@ -101,7 +112,7 @@ generateInterfaces pd lbi = do
 
   -- Remove all existing .agdai files.
   forM_ builtins $ \fp -> do
-    let fullpathi = toIFile (ddir </> fp)
+    let fullpathi = toIFile pd (ddir </> fp)
 
         handleExists e | isDoesNotExistError e = return ()
                        | otherwise             = throwIO e
@@ -124,8 +135,6 @@ generateInterfaces pd lbi = do
       (proc agda
           [ "--interaction"
           , "--interaction-exit-on-error"
-          , "--no-libraries"
-          , "--local-interfaces"
           , "-Werror"
           , "-v0"
           ])

src/data/lib/prim/agda-builtins.agda-lib

@@ -0,0 +1,2 @@
+name: agda-builtins
+include: .

test/Fail/Issue641-all-interfaces.err

@@ -20,7 +20,7 @@ Building interface...
 Finished serialization.
 Considering writing to interface file.
 Actually calling writeInterface.
-Writing interface file agda-default-include-path/Agda/Primitive.agdai.
+Writing interface file agda-default-include-path/_build/2.6.4.1/agda/Agda/Primitive.agdai.
 Wrote interface file.
 Finished writing to interface file.
 Accumulated statistics.
@@ -54,7 +54,7 @@ Building interface...
 Finished serialization.
 Considering writing to interface file.
 Actually calling writeInterface.
-Writing interface file agda-default-include-path/Agda/Primitive/Cubical.agdai.
+Writing interface file agda-default-include-path/_build/2.6.4.1/agda/Agda/Primitive/Cubical.agdai.
 Wrote interface file.
 Finished writing to interface file.
 Accumulated statistics.

test/Fail/Issue641.err

@@ -2,17 +2,17 @@ Importing the primitive modules.
   Getting interface for Agda.Primitive
   Check for cycle
   Agda.Primitive is up-to-date.
-  no stored version, reading agda-default-include-path/Agda/Primitive.agdai
-Loading  Agda.Primitive (agda-default-include-path/Agda/Primitive.agdai).
+  no stored version, reading agda-default-include-path/_build/2.6.4.1/agda/Agda/Primitive.agdai
+Loading  Agda.Primitive (agda-default-include-path/_build/2.6.4.1/agda/Agda/Primitive.agdai).
   imports: []
   New module. Let's check it out.
 Merging interface
   Now we've looked at Agda.Primitive
   Getting interface for Agda.Primitive.Cubical
   Check for cycle
   Agda.Primitive.Cubical is up-to-date.
-  no stored version, reading agda-default-include-path/Agda/Primitive/Cubical.agdai
-Loading  Agda.Primitive.Cubical (agda-default-include-path/Agda/Primitive/Cubical.agdai).
+  no stored version, reading agda-default-include-path/_build/2.6.4.1/agda/Agda/Primitive/Cubical.agdai
+Loading  Agda.Primitive.Cubical (agda-default-include-path/_build/2.6.4.1/agda/Agda/Primitive/Cubical.agdai).
   imports: [(Agda.Primitive, 450520314077838934)]
   Already visited Agda.Primitive
   New module. Let's check it out.