[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