[Agda] Development version of agda-mode doesn't recognize symlinks?

Jan Stolarek jan.stolarek at p.lodz.pl
Tue Nov 26 13:26:27 CET 2013


Hi *,

I just installed latest development version of Agda. I have agda-mode set up in Emacs, but when I 
try to load agda source file I get an error in AgdaInfo minibuffer:

You tried to load
/home/killy/.cabal/share/Agda-2.3.3/lib/prim/Agda/Primitive.agda
which defines the module Agda.Primitive. However, according to the
include path this module should be defined in
/dane/sandboxes/ghc/7.6.3/.cabal/share/Agda-2.3.3/lib/prim/Agda/Primitive.agda.

Now:
  1. ~/.cabal/ is a symlink to ~/.ghc-sandbox/.cabal/
  2. ~/.ghc-sandbox is a symlink to /dane/sandboxes/ghc/active/
  3. /dane/sandboxes/ghc/active/ is a symlink to a directory containing installation of GHC and 
Haskell libraries (/dane/sandboxes/ghc/7.6.3 in this case).

So Agda installation is logically located in /home/killy/.cabal/share/Agda-2.3.3/, but in reality 
(if you follow symlinks) it is located in /dane/sandboxes/ghc/7.6.3/.cabal/share/Agda-2.3.3/

It seems that symlinks are confusing agda-mode. Any way to solve that problem?

Janek


More information about the Agda mailing list