Radu Mereuta

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...

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...

We decided in K4 to change the syntax of labels a bit. So I think there you have an issue because `roundFloat` can be also parsed as a KLabel. If...

Not in K4. If you ever need to see what's predefined in k, you can have a look in https://github.com/kframework/k/blob/master/k-distribution/include/builtin/domains.k Andhttps://github.com/kframework/k/blob/master/k-distribution/include/builtin/kast.k

I remember having a similar issue some time ago. Unfortunately is not something in the front end, and I don't know where to look in the backend.

This version of K is no longer in active development. You should try and switch to https://github.com/kframework/k

Somehow this escaped my attention at the time. It seems that for some reason, the length of that list is a problem with the way we're parsing cells in rules....

I don't know what changed in IntelliJ, but I would like to help. I always wanted to use the JavaCC parser of the outer K so we have way better...

Actually, having access to the meta level would work even better. I'm not sure what is the status of that. Do you have some documentation and examples?

Try adding klabels to your lists. The automatic klabel generation doesn't look for collisions and in this case krun gets confused. ``` syntax ListA ::= List{Int, ","} [strict, klabel(IntList)] syntax...