[Agda] "Failed to find source"

mechvel at scico.botik.ru mechvel at scico.botik.ru
Sun May 10 23:21:09 CEST 2020


This is on Agda 2.6.1.

When in the file     foo/L/M.agda
it is set the module

----------------------
open import P using ...

module M {..} (S : Setoid _ _) where   -- top level parametric module
...
----------------------

(with forgetting to add "L." before "M"),
and it is being type-checked under  emacs,  the message is

"Failed to find source of module P in any of the following
  locations:
    /foo/L/P.agda
   ...
"

If it is type-checked by
> cd foo
> agda $agdaLibOpt L/M.agda

, then the message is helpful:

"The name of the top level module does not match the file name. ..."

If there is added the prefix "L.", then it is type-checked successfully 
in both cases.


Can Agda issue the latter message in both cases?

Regards,

------
Sergei



More information about the Agda mailing list