making kompile/krun faster

[kheradmand]

Currently for each simple change I have to wait around 20s for kompile and 20s for krun. I was wondering if there any way/option to make kompile or krun faster?

┆Issue is synchronized with this Asana task

[radumereuta]

This sounds a bit much. Can you run the tools with the -v option? This should give out a bit more detail about how much each step takes. kompile also has incremental compilation. Can you post some outputs for the first (after clearing caches) and second kompilation?

Also, how big is your definition? And what machine are you using (cpu, memory, OS, SSD vs HDD). All these might affect time considerably.

[kheradmand]

to see the definition take a look at this: https://github.com/kframework/p4-semantics

this is the result of kompile when I remove the *-kompiled folder:

time kompile configuration.k --syntax-module P4-SYNTAX --debug -v
Parse command line options                                   =    63
...
Parse definition [87/87 rules]                               = 21250
Apply compile pipeline                                       =  6872
Save to disk                                                 =   472
Cleanup                                                      =     1
Total                                                        = 28658

real	0m29.214s
user	1m1.022s
sys	0m1.326s

here is the result of kompile for second time:

Parse command line options                                   =    67
...
Parse definition [0/87 rules]                                =  8873
Apply compile pipeline                                       =  4236
Save to disk                                                 =   224
Cleanup                                                      =     0
Total                                                        = 13400

real	0m13.921s
user	0m29.736s
sys	0m0.875s

here is the result of krun:

Parse command line options                                   =    85
...

real	0m12.521s
user	0m27.859s
sys	0m0.955s

I have Macbook Air (1.6 GHz Intel Core i5 with 8GB RAM and SSD Hard)

Waiting around 30s for each rule change (specially that I (have to) do everything by trial and error) is really annoying.

[radumereuta]

I still get 7s/4s on an i7 3.6 GHz for an empty definition. I think it might be mostly related to serialization, although applying the compile pipeline takes an awfully long time (much more than K3).

@cos opinions on this?