Fix agda#7331: handle permission error when search for project file

Closes agda#7331.

src/full/Agda/Interaction/Library.hs

@@ -61,6 +61,7 @@ import qualified Data.Text as T
 import System.Directory
 import System.FilePath
 import System.Environment
+import System.IO.Error ( isPermissionError )
 
 import Agda.Interaction.Library.Base
 import Agda.Interaction.Library.Parse
@@ -191,7 +192,7 @@ findProjectConfig'
 findProjectConfig' root = do
   getCachedProjectConfig root >>= \case
     Just conf -> return conf
-    Nothing   -> do
+    Nothing   -> handlePermissionException do
       libFiles <- liftIO $ getDirectoryContents root >>=
         filterM (\file -> and2M
           (pure $ takeExtension file == ".agda-lib")
@@ -215,6 +216,13 @@ findProjectConfig' root = do
           return conf
 
   where
+    -- Andreas, 2024-06-26, issue #7331:
+    -- In case of missing permission we terminate our search for the project file
+    -- with the default value.
+    handlePermissionException :: LibErrorIO ProjectConfig -> LibErrorIO ProjectConfig
+    handlePermissionException = flip catchIO \ e ->
+      if isPermissionError e then return DefaultProjectConfig else liftIO $ E.throwIO e
+
     -- Note that "going up" one directory is OS dependent
     -- if the directory is a symlink.
     --

test/interaction/Issue7331.out

@@ -0,0 +1 @@
+Checking Issue7331 (Issue7331/dir/Issue7331.agda).

test/interaction/Issue7331.sh

@@ -0,0 +1,23 @@
+#!/usr/bin/env bash
+
+# Andreas, 2024-06-26, issue #7331:
+# Handle permission error sensibly when looking for project root.
+
+AGDA=${1}
+
+mkdir -p Issue7331/dir             > /dev/null
+touch Issue7331/dir/Issue7331.agda > /dev/null
+pushd Issue7331/dir                > /dev/null
+
+# Drop permissions for parent dir
+chmod -r ..                        > /dev/null
+
+${AGDA} --ignore-interfaces Issue7331.agda
+result=$?
+
+# Clean up
+popd                               > /dev/null
+chmod +r Issue7331                 > /dev/null
+rm -rf Issue7331                   > /dev/null
+
+exit $result