Optimize SExpression Parsing

[NightRa]

Before this pull request, loading a file not too big took 17 seconds to parse the S-Exprs coming from agda. Now it takes 20ms.

Also note that agda sends a huge agda2-highlight-add-annotations response, (500kb for not-so-big files) of which we usually use very little, only for unsolvedmeta and terminationproblem. We could possibly make agda send us only the information we need.

[banacorn]

Looks great! Thanks a lot!

[banacorn]

About the huge agda2-highlight-add-annotations response, there are two ways of receiving them, either directly via stdio or indirectly via some temporary file read/write:

HighlightingMethod, for example:

IOTCM "/some/path/to/file.agda" NonInteractive Indirect Cmd_constraint
IOTCM "/some/path/to/file.agda" NonInteractive Direct Cmd_constraints

And this is configurable from the package settings at Highlighting information passing, which was default to Direct here, but Indirect on Emacs.

I chose Direct as default because I thought the Indirect way of sending response would require more frequent file system access. I'm not sure which way is better or faster, since we only need very little of that information.

[markokoleznik]

Just jumping in with some thoughts.

@NightRa Can you please provide such file that takes 17seconds to parse? Because last time I did some serious "work" I was running some program (not written by me) with over 50 modules and parsing was almost instant.

@banacorn I chose indirect for two reasons. 1.) At the time of coding this stuff, I wasn't aware direct is an option (only after you pointed out 😄) 2.) After that I tried direct but wasn't satisfied because I've used the same pipe. I could fire up a new thread and listen on stdio for highlighting.

Instead I do this: When I receive highlighting signal, I fire up asynchronous task on files and I must say I'm rather amazed how well this performs.

I can go into more details, if you want.

Non related: After I saw all the activity on your channel I feel bad for not taking the time and fix my issues 😄

[NightRa]

@markokoleznik nat-thms.agda in the IAL caused the 17sec parsing time. I fixed a performance bug in jison which lisp-to-array uses to reduce it to 9sec (see zaach/jison#332), but just writing the parser isn't too hard and reduced it to 20ms.
The file itself is at: http://pastebin.com/j1qwJYV0.

[banacorn]

@markokoleznik hmm I think I should follow you and use Indirect. By the way, do you use highlighting information other than unsolvedmeta and terminationproblem?

@NightRa 17000ms => 20ms this is just amazing!

[NightRa]

@banacorn Not sure if switching to indirect would be good, writing to disk and all.. If there's no problem why fix it? (and make it more complicated) :)

[markokoleznik]

@banacorn I must agree on this one with @NightRa . But you can do a performance test with direct vs indirect and report the results :)

Also, I use all the operator highlighting I could find in Agda source with "Emacs" default colorization (lack of imagination from my side).
Here is everything I highlight (operator wise)
https://github.com/markokoleznik/agda-writer/blob/master/Agda%20Writer/AWColors.m

[banacorn]

@NightRa @markokoleznik You are right, I should do some benchmarks before doing anything stupid.

I should also adopt dynamic highlighting as what agda-writer and agda-mode on Emacs do, since the static highlighting on Atom is so lacking. The main reason I haven't look into it is because of performance concerns (with all that colors flying around), but I will only know after trying.

[markokoleznik]

That was my main concern as well, but like I've said, it parses out huge files almost instantly, and highlighting isn't the problem.

Side note: My only concern with this is handling the highlighting (but then again, Atom is hackable text editor, highlighting shouldn't be the problem).

I remember I faced the issue when highlighting was fast for small files but grew exponentially with larger files.
Details here:
http://stackoverflow.com/questions/28254068/method-settextcolorrange-on-nstextview-is-ridiculously-slow