[Agda] Compilation of Parser.y depends on the locale on Debian too

Andrés Sicard-Ramírez asr at eafit.edu.co
Fri Jul 2 19:07:43 CEST 2021


Hi Eduardo,

Thank you for reporting the issue and his solution.

I could reproduce the issue after running `export LC_ALL=C` in my
Ubuntu machine.

Please report the issue in https://github.com/agda/agda/issues so we
can track similar issues. I shall update the documentation shortly.

Best,

On Fri, 2 Jul 2021 at 09:46, Eduardo Ochs <eduardoochs at gmail.com> wrote:
>
> Hi list,
>
> the latest version of the Agda Manual from
>
>   https://readthedocs.org/projects/agda/downloads/pdf/latest/
>
> mentions a certain error as something that can only happen on M$
> Windows. It says:
>
>   Warning: If you are installing Agda using Cabal on Windows,
>   depending on your system locale setting, cabal install Agda may fail
>   with an error message:
>
>   hGetContents: invalid argument (invalid byte sequence)
>
>   If this happens, you can try changing the console code page to UTF-8
>   using the command:
>
>   CHCP 65001
>
> I'm on Debian stable and I got something similar. I tried to install
> Agda with
>
>   cabal update
>   cabal install Agda
>
> and it failed with:
>
>   happy: src/full/Agda/Syntax/Parser/Parser.y: hGetContents: invalid
>   argument (invalid byte sequence)
>   cabal: Failed to build Agda-2.6.2. See the build log above for
>   details.
>
> My default value for $LC_ALL is "C" and the only uncommented line in
> my /etc/locale.gen is this one:
>
>   en_GB.UTF-8 UTF-8
>
> If I run this
>
>   export LC_ALL=en_GB.UTF-8
>   cabal install Agda
>
> instead of just "cabal install Agda" the compilation succeeds.
>
>   Cheers,
>     Eduardo Ochs
>     http://angg.twu.net/#eev
>     http://angg.twu.net/math-b.html
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> La información contenida en este correo electrónico está dirigida únicamente a su destinatario y puede contener información confidencial, material privilegiado o información protegida por derecho de autor. Está prohibida cualquier copia, utilización, indebida retención, modificación, difusión, distribución o reproducción total o parcial. Si usted recibe este mensaje por error, por favor contacte al remitente y elimínelo. La información aquí contenida es responsabilidad exclusiva de su remitente por lo tanto la Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The information contained in this email is addressed to its recipient only and may contain confidential information, privileged material or information protected by copyright. Its prohibited any copy, use, improper retention, modification, dissemination, distribution or total or partial reproduction. If you receive this message by error, please contact the sender and delete it. The information contained herein is the sole responsibility of the sender therefore Universidad EAFIT is not responsible for what the message contains.



-- 
Andrés


More information about the Agda mailing list