Handle case-insensitive file systems in a better way

[andrejbauer]

Where do I report bugs?

open import Relation.Binary.PropositionalEquality

module Error where

  data N : Set where
    Z : N
    S : N → N

  infixr 5 _+_

  _+_ : N → N → N
  m + Z = m
  m + S n = S (m + n)

  problem : ∀ a → S Z + a ≡ S a
  problem Z = refl
  problem (S a) = trans (problem (S a)) refl

-- An internal error has occurred. Please report this as a bug.
-- Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Errors.hs:296:18 in
-- Agd-2.6.2-7cfdab78:Agda.TypeChecking.Errors

System info:

% uname -a
Darwin OA 20.6.0 Darwin Kernel Version 20.6.0: Mon Aug 30 06:12:21 PDT 2021; root:xnu7195.141.6~3/RELEASE_X86_64 x86_64

% agda --version
Agda version 2.6.2

Do you need anything else?

[Trebor-Huang]

A random guess: since you are on a case-insensitive system, does your module name agree exactly with your file name (including case)? See #5508

[jespercockx]

I failed to reproduce the error on Linux, so it could be something platform-related indeed. Can someone on Apple try if they can reproduce this?

[andreasabel]

A random guess: since you are on a case-insensitive system, does your module name agree exactly with your file name (including case)? See #5508

Yes, @andrejbauer :

• What is the filename of module Error?
• Does the issue go away with Agda-2.6.2.1?

[andreasabel]

The is likely no MWE coming. Closing.

[andrejbauer]

Sorry for the delay. Using Agda 2.6.2 on MacOS, I can confirm that the problem is caused by case-insensitive file names. When I make sure that the file name matches, I get a reasonable error (about termination checking).

Is there a way for Agda to fail more graciously, or should we just blame Apple for this bug?

[gallais]

Looks like Agda.Interaction.FindFile already has the right logic. Should this ifdef:

agda/src/full/Agda/Utils/FileName.hs

Lines 107 to 114 in 798be60

	#ifdef mingw32_HOST_OS
	doesFileExistCaseSensitive f = do
	doesFileExist f `and2M` do
	bracket (findFirstFile f) (findClose . fst) $
	fmap (takeFileName f ==) . getFindDataFileName . snd
	#else
	doesFileExistCaseSensitive = doesFileExist
	#endif

also be activated for mac?

[andreasabel]

Sorry for the delay. Using Agda 2.6.2 on MacOS, I can confirm that the problem is caused by case-insensitive file names. When I make sure that the file name matches, I get a reasonable error (about termination checking).

Is there a way for Agda to fail more graciously, or should we just blame Apple for this bug?

No, sorry @andrejbauer, this it totally Agda's fault. I am on macOS myself, so I would be curious to reproduce the issue, but I was lacking information (i.e., the spelling of the filename of the module). Issue #5508 could be related, which is fixed on Agda 2.6.2.1. Could you please try to reproduce the issue on 2.6.2.1 (or complete the information so I can reproduce it)?

[andreasabel]

Looks like Agda.Interaction.FindFile already has the right logic. Should this ifdef:

agda/src/full/Agda/Utils/FileName.hs

Lines 107 to 114 in 798be60

	#ifdef mingw32_HOST_OS
	doesFileExistCaseSensitive f = do
	doesFileExist f `and2M` do
	bracket (findFirstFile f) (findClose . fst) $
	fmap (takeFileName f ==) . getFindDataFileName . snd
	#else
	doesFileExistCaseSensitive = doesFileExist
	#endif

also be activated for mac?

Trying to remember my thought process here. OK:

• For one, fixing doesFileExistCaseSensitive according to the compile-time OS (rather than the runtime OS) is a hack in the first place (think cross-compilation), but well.
• But then, case-sensitivity is not really an OS-specific thing, but a it is file-system specific, if I am not mistaken. You can access a case-insensitive system also from Linux.
• Finally, the find API is different for Window and Unix (BSD/Linux). For Windows, we can ask to find all files matching a pattern, like dir/file.agda, whereas in Unix we only get to ask for the contents of dir/ search through them. This can be costly for large directories, and I did not want to have this running on every call to doesFileExistsCaseSensitive.

It would be optimal if there was a function that would tell you the case-sensitivity of a location (like dir/). In the testsuite, I have some code that infers the case-sensitivity by experiment. Not a hack to be proud of, but at least it should be correct:

agda/test/Fail/Tests.hs

Lines 93 to 106 in 719ba66

	-- | A test for case-insensitivity of the file system.
	caseInsensitiveFileSystem :: IO Bool
	caseInsensitiveFileSystem = fst <$> caseInsensitiveFileSystem4671
	-- | A test for case-insensitivity of the file system, using data of test 4671.
	caseInsensitiveFileSystem4671 :: IO (Bool, FilePath)
	caseInsensitiveFileSystem4671 = do
	b <- doesFileExist goldenFileInsens'
	return (b, if b then goldenFileInsens else goldenFileSens)
	where
	dir = testDir </> "customised"
	goldenFileSens = dir </> "Issue4671.err.case-sensitive"
	goldenFileInsens = dir </> "Issue4671.err.case-insensitive"
	goldenFileInsens' = dir </> "Issue4671.err.cAsE-inSensitive" -- case variant, to test file system

[nad]

Apparently some recent Linux kernel supports file systems for which floß and FLOSS refer to the same file.

What is the goal with Agda's support for case-insensitive file systems? One goal is presumably to avoid making users confused. Should we also aim to ensure maximum portability? In that case we should perhaps refuse having (say) both A.agda and a.agda on a case-sensitive file system. However, should we then also refuse having both floß.agda and FLOSS.agda? The rules of the file system I mentioned above supposedly depend on the version of Unicode that the file system uses.

[andreasabel]

In that case we should perhaps refuse having (say) both A.agda and a.agda on a case-sensitive file system.

Yes! I definitely support this.

However, should we then also refuse having both floß.agda and FLOSS.agda?

That sounds too complicated.
If you are using non-ASCII Unicode characters in your filenames, you have to be prepared for trouble.

I'd stick to the common case of upper/lowercase confusions.

[nad]

That sounds too complicated.

ghci> :set -XOverloadedStrings 
ghci> :set -package text-icu
package flags have changed, resetting and loading new packages...
ghci> import Data.Text.ICU
ghci> toCaseFold False "FLOSS" == toCaseFold False "floß"
True

[nad]

Perhaps one should first normalise:

ghci> "ö" == "ö"
False
ghci> toCaseFold False "ö" == toCaseFold False "ö"
False
ghci> normalize NFD "ö" == normalize NFD "ö"
True

[andreasabel]

This suggests that text-icu provides the standard. I can change my mind, knowing a standard exists...

[andreasabel]

Ping @andrejbauer for a self-contained reproducer.

[andreasabel]

Ping @andrejbauer for a self-contained reproducer.