Load times slower than emacs mode

[msuperdock]

Issue

After noticing that agda-vim has slower load times than the official emacs mode, I decided to try to figure out why. After some tests, I think the calls to make and AgdaLoad are doing duplicate work.

Tests

I originally posted an issue in the official agda repository with some tests, before I realized this issue was specific to agda-vim. When measuring the load time of one of the files (B.agda), I find that:

• agda-vim takes about 6s for the initial load, and 3s for reloads (without changing the buffer).
• agda2-mode.el takes about 3s for the initial load, and virtually no time for reloads.

When agda-vim initially loads, it calls AgdaReload near the bottom of ftplugin/agda.vim. This command calls make, after which the QuickfixCmdPost autocommand defined near the top of the file is triggered, which calls AgdaReloadSyntax, AgdaVersion, and AgdaLoad. By calling these commands manually, one by one, we get a sense of which commands are taking up time:

• make (about 3s)
• `AgdaReloadSyntax (fast)
• AgdaVersion (fast)
• AgdaLoad (about 3s)

On subsequent reloads (without changing the buffer), the AgdaLoad call takes virtually no time, so the call to make takes most of the time.

Workaround

I tried making the following adjustments:

• At the bottom of ftplugin/agda.vim, replace AgdaReload with call AgdaVersion(1) | call AgdaLoad(1). (I am not sure why, but leaving out the call to AgdaVersion results in an error.)
• To reload Agda, type :AgdaLoad(0) instead of using AgdaReload.

These result in load times comparable to the emacs mode, with the following tradeoffs:

• The quickfix list is not populated.
• The syntax highlighting information produced by agda is not used.

Thoughts

Could the make call be removed entirely without sacrificing features? It would be possible to populate the quickfix list just by scanning the buffer for patterns like {!!} and ?. (It wouldn't include the unresolved implicit arguments, but I personally don't like these appearing in the quickfix list anyway.) It might also be possible to recover the syntax highlighting.

If not, maybe it would make sense to include an option, so users can choose whether to sacrifice load times for these additional features.

[derekelkins]

It wouldn't be too hard to populate the quickfix window based on the agda process rather than parsing the output of running agda. Agda can provide syntax highlighting information dynamically, but not in a way that's that useful for vim. One option would be to execute the agda --vim command asynchronously. Of course, the suggestion of having a separate "update syntax" command would also work.

I just pushed a json branch I'm experimenting with that implements the asynchronous approach. It also uses Agda's new JSON API so it will only work for new versions of Agda.