UTF8 parsed incorrectly for literate agda files

[twanvl]

The following literate agda file (test.lagda) gives a parse error, at least on Windows:

\begin{code}
module _ where
id : {A : Set} → A → A
id x = x
\end{code}

Error:

test.lagda:3,16: Parse error
→<ERROR>
 A → A
id x = x

This is clearly an encoding issue.

Looking at the agda source code, it seems that non-literate .agda files are opened with Agda.Utils.IO.UTF8.readTextFile (see here), while literate agda files use Prelude.readFile (see here).

Version: Agda version 2.6.0-6ad752f, on windows 7.
Note: the agda command line gives no errors, but agda-mode from emacs does.

[andreasabel]

This might be an omission. @vlopezj , can you take a look?

[vlopezj]

@twanvl: I applied your suggestion, it is now on both the stable-2.5 and the master branch. Can you check if it works on Windows now?

[twanvl]

I have tested it, and the issues is fixed on the master branch on Windows.

[nad]

The readFile function uses the current locale to determine the encoding, at least on some systems. Agda sources must always be UTF8-encoded, and we should always use the UTF8 encoding when reading and writing Agda sources.

I can trigger a similar problem on my Linux machine:

$ LC_CTYPE=C agda test.lagda 
/tmp/test.lagda: hGetContents: invalid argument (invalid byte
sequence)

I suggest that we add test cases that set LC_CTYPE to C, like I do above, both for literate and for non-literate files.