[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