warns when edit from other directories

[0kaguya]

For example, if there is already a written file localed at ~/foo/bar/name.agda and edit with ~/foo/$ vim bar/name.agda, it complains

"~/foo/bar/name.agda" 5L, 80C
/home/user/foo/bar/name.agda:1,8-19
The name of the top level module does not match the file name. The
module name should be defined in one of the following files:
  /home/user/builds/agda-stdlib/src/name.agda
  /home/user/builds/agda-stdlib/src/name.lagda
  /usr/share/agda/lib/prim/name.agda
  /usr/share/agda/lib/prim/name.lagda

[andrejtokarcik]

Doesn't the top-level module happen to be called hello-world in your name.agda file? If so, you should either rename the file or the top-level module. In Agda, the name of the top-level module must match the filename, which doesn't seem to hold in your case.

Another way to check: do you also get the same error if you run agda bar/name.agda directly? It's a bug pertaining to agda-vim specifically only if you do not get the same error when passing in the file to agda directly.

[0kaguya]

sorry not check my message carefully... I know they should match, the hello-world is a typo and now corrected.

yes, agda foo/bar/name.agda show error messages. now I add cd command in my vim config and it fixes.