[Agda] Failure when importing stdlib file

[Chantal KELLER]

Hi Anton,

Thank you for your answer, it was indeed the problem. I now get another
problem, but as it is different I will post another discussion.

Perhaps I am mistaking, but this is very weird that you have to be able
to write in the directories where the stdlib files are. Shouldn't they
be compiled once for all when installing? And even if you have to write
some files, why not in /tmp or in the directory you are working in?

Thanks,
Chantal.




Anton Setzer a écrit :
> Chantal KELLER wrote:
>> Hello Agda users,
>>
>> I have installed the Agda package for Linux Debian Sid, and I get an
>> error when I try to import files from the standard library. For
>> instance, consider the file "/home/keller/test.agda" containing:
>>
>> =======================
>> module test where
>> open import Data.Nat
>> =======================
>>
>> When I try to load this file (C-c C-l), the file
>> "/usr/share/agda-stdlib/Data/Nat.agda" opens, the file
>> "/home/keller/test.agda" is not loaded, and there are the following
>> lines in *ghci*:
>>
>> =======================
>> Prelude Agda.Interaction.GhciTop> cmd_load "/home/keller/test.agda"
>> ["/usr/share/agda-stdlib", "."]
>> Checking /home/keller/test.agda.
>> Checking Data.Nat (/usr/share/agda-stdlib/Data/Nat.agda).
>> Checking Data.Function (/usr/share/agda-stdlib/Data/Function.agda).
>> agda2_mode_code (annotation-goto
>>                  '("/usr/share/agda-stdlib/Data/Nat.agda" . 190))
>> agda2_mode_code (agda2-highlight-reload)
>> agda2_mode_code (agda2-annotate '())
>> *** Exception: ExitFailure 1
>> =======================
>>
>> Thanks for your help,
>>   
> Is the standard library at a location where you can write to. When Agda
> type checks files it creates files  file.agdai and .file.el
> If it can't create them (because they are for instance in a directory owned
> by root) it gives error messages.
> 
> Anton
> 

-- 
Chantal KELLER