[Agda] Failure when importing stdlib file

[Anton Setzer]

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

-- 
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK

Telephone:
(national)        (01792) 513368
(international) +44 1792  513368
Fax:
(national)        (01792) 295708
(international) +44 1792  295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------