[Agda] Failed to find source of module

Sergei Meshveliani mechvel at botik.ru
Mon Feb 13 14:49:30 CET 2017


Dear Agda developers,

when I set to the directory  ~/mySource/Foo/  the file  TT.agda,  with
the heading

  module TT where

(instead of the correct  module Foo.TT where),
Agda 2.5.2 reports

 (*)   Failed to find source of module  ...

And it lists the directory names where it searched, and the directory
~/mySource  is not listed.
If I improve the name to  Foo.TT,  then it searches where it is needed.

And the error report (*) looks as misleading.

Regards,

------
Sergei



More information about the Agda mailing list