[Agda] Failure when importing stdlib file
Chantal KELLER
chantal.keller at wanadoo.fr
Tue Sep 8 17:27:51 CEST 2009
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,
--
Chantal KELLER
More information about the Agda
mailing list