Provide a .agda-lib for Agda builtins (agda#6988)

* Ignore directories with an .agda-lib suffix

Co-authored-by: ibbem <ibbem@ibbem.net>

* 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>

* Decide between interface files based on their existence

---------

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"
           ])

doc/user-manual/tools/command-line-options.rst

@@ -309,9 +309,9 @@ Imports and libraries
 
      .. versionadded:: 2.6.1
 
-     Read and write interface files next to the Agda files they
-     correspond to (i.e. do not attempt to regroup them in a
-     ``_build/`` directory at the project's root).
+     Prefer to read and write interface files next to the Agda files they
+     correspond to (i.e. do not attempt to regroup them in a ``_build/``
+     directory at the project's root, except if they already exist there).
 
 .. option:: --no-default-libraries
 

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

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

src/full/Agda/Interaction/FindFile.hs

@@ -44,7 +44,7 @@ import qualified Agda.TypeChecking.Monad.Benchmark as Bench
 import {-# SOURCE #-} Agda.TypeChecking.Monad.Options
   (getIncludeDirs, libToTCM)
 import Agda.TypeChecking.Monad.State (topLevelModuleName)
-import Agda.TypeChecking.Warnings (runPM)
+import Agda.TypeChecking.Warnings (runPM, genericWarning)
 
 import Agda.Version ( version )
 
@@ -55,6 +55,7 @@ import Agda.Utils.List1 ( List1, pattern (:|) )
 import qualified Agda.Utils.List1 as List1
 import Agda.Utils.Monad ( ifM, unlessM )
 import Agda.Syntax.Common.Pretty ( Pretty(..), prettyShow )
+import qualified Agda.Syntax.Common.Pretty as P
 import Agda.Utils.Singleton
 
 import Agda.Utils.Impossible
@@ -87,15 +88,33 @@ mkInterfaceFile fp = do
 toIFile :: SourceFile -> TCM AbsolutePath
 toIFile (SourceFile src) = do
   let fp = filePath src
-  mroot <- ifM (optLocalInterfaces <$> commandLineOptions)
-               {- then -} (pure Nothing)
-               {- else -} (libToTCM $ findProjectRoot (takeDirectory fp))
-  pure $ replaceModuleExtension ".agdai" $ case mroot of
-    Nothing   -> src
+  let localIFile = replaceModuleExtension ".agdai" src
+  mroot <- libToTCM $ findProjectRoot (takeDirectory fp)
+  case mroot of
+    Nothing   -> pure localIFile
     Just root ->
       let buildDir = root </> "_build" </> version </> "agda"
-          fileName = makeRelative root fp
-      in mkAbsolute $ buildDir </> fileName
+          fileName = makeRelative root (filePath localIFile)
+          separatedIFile = mkAbsolute $ buildDir </> fileName
+          selectIFile = ifM (optLocalInterfaces <$> commandLineOptions)
+            (pure localIFile)
+            (pure separatedIFile)
+      in do
+        separatedIFileExists <- liftIO $ doesFileExistCaseSensitive $ filePath separatedIFile
+        localIFileExists <- liftIO $ doesFileExistCaseSensitive $ filePath localIFile
+        case (separatedIFileExists, localIFileExists) of
+          (False, False) -> selectIFile
+          (False, True) -> pure localIFile
+          (True, False) -> pure separatedIFile
+          (True, True) -> do
+            ifile <- selectIFile
+            genericWarning $ P.vcat
+                [ P.text "There are two interface files:"
+                , P.nest 4 $ P.text $ filePath separatedIFile
+                , P.nest 4 $ P.text $ filePath localIFile
+                , P.nest 2 $ P.text $ "Using " ++ filePath ifile ++ " for now but please remove at least one of them."
+                ]
+            pure ifile
 
 replaceModuleExtension :: String -> AbsolutePath -> AbsolutePath
 replaceModuleExtension ext@('.':_) = mkAbsolute . (++ ext) .  dropAgdaExtension . filePath

src/full/Agda/Interaction/Library.hs

@@ -194,7 +194,10 @@ findProjectConfig' root = do
   getCachedProjectConfig root >>= \case
     Just conf -> return conf
     Nothing   -> do
-      libFiles <- liftIO $ filter ((== ".agda-lib") . takeExtension) <$> getDirectoryContents root
+      libFiles <- liftIO $ getDirectoryContents root >>=
+        filterM (\file -> and2M
+          (pure $ takeExtension file == ".agda-lib")
+          (doesFileExist (root </> file)))
       case libFiles of
         []     -> liftIO (upPath root) >>= \case
           Just up -> do

src/full/Agda/Interaction/Options/Base.hs

@@ -1477,7 +1477,7 @@ standardOptions =
     , Option []     ["ignore-interfaces"] (NoArg ignoreInterfacesFlag)
                     "ignore interface files (re-type check everything)"
     , Option []     ["local-interfaces"] (NoArg localInterfacesFlag)
-                    "put interface files next to the Agda files they correspond to"
+                    "put new interface files next to the Agda files they correspond to"
     , Option ['i']  ["include-path"] (ReqArg includeFlag "DIR")
                     "look for imports in DIR"
     , Option ['l']  ["library"] (ReqArg libraryFlag "LIB")

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.