Meta-Issue to track/understand CoqJS performance.

[ejgallego]

Hi everybody,

[I hope the issue tracker is the right place for this kind of discussion, otherwise feel free to remove/close the issue]

We did some progress in trying to compile Coq with js_of_ocaml, a prototype is available at the jscoq github repository and it can be seen live at https://x80.org/rhino-coq/

In Chrome Dev (45) the situation seems quite good. I was able to do ssrnat without much trouble using an increased stack size. An issue is to improve plugin loading time, as jscoq has to compile large chunks of js.

Some example Coq test scripts:

Regular Coq:

Require Import Coq.Init.Prelude.
Lemma addn0 n : n + 0 = 0 + n.
now induction n; auto; simpl; rewrite IHn.
Qed.

Ssreflect:

Require Import Ssreflect.ssreflect.
Lemma addn0 n : n + 0 = 0 + n.
by elim: n => [|n /= ->].
Qed.

Mozilla Firefox

With limited informal testing, the performance in Mozilla seems on par with the bytecode interpreter.

Stack Overflows are a problem when dynamically loading large plugins (cma files). One solution could be precompiling (see #307, #313), another one would be to increase SpiderMonkey stack size, but this seems hard. Would we solve that, the performance in Mozilla should be good.

Chrome

Chrome 45 seems to work very well. 43 44 run very slow.

Chrome does also suffer from a short stack, but passing the --js-flags="--stack-size=65536" command line option seems to enable Coq to run quite OK.

Thanks,
E.

[Drup]

Let me first say that this is amazing.

Now, I can't help you on the performance side, I'll let that to @vouillon and @hhugo, but don't you want to at least pass -opt 3 to js_of_ocaml here ?

[vouillon]

The -opt option has mostly an impact on code size, not much on performance.

[gasche]

I would guess that exceptions (which are very efficient in the OCaml runtime system, and not so much everywhere else) might be the cause of performance slowdown on other backends.

Emilio, being more familiar with the Coq codebase than many people around here, could you point to the code portions in the Coq source that are actually involved in the computations you observe are slow? (Where is the code of unification? Where is the Ltac-interpreter hot loop?) That would help finding suspicious patterns.

[ejgallego]

Thanks for the explanations. Indeed -opt seems not to help, Coq is still quite slow but usable.

For instance, this proof:

Lemma addn0 n : n + 0 = 0 + n.
Proof. by elim: n => [|n /= ->]. Qed,

Takes 15 seconds in my machine vs instantaneous in the bytecode interpreter.

[ejgallego]

@gasche, I'm trying to understand js profiling tools at the moment, and see if I can map the slow parts back to Coq's code.

Unfortunately there's too much code involved in the slow paths for me to being able to narrow a useful portion now, but I'll try.

[ejgallego]

I was able to profile a non optimized Coq version, indeed, exception handling as pointed by @gasche seems to play a role in the profile, but it is still not clear to me what is going on.

Chromium profile availabe at: https://x80.org/rhino-coq/coqjs-profile-20150629.tar.bz2

[ejgallego]

Indeed, it seems that Chrome/v8 disables the optimizer for try/catch enclosed exceptions, this could be hurting Coq big time as @gasche pointed out.

I tried Firefox and the performance is much much better, to the point that is comparable with the bytecode version! Yay!

[braibant]

IIRC, the tactics machinery spends a lot of time raising/catching exceptions. This is coherent with the fact that Qed is fast, while building the proof term is really slow. Btw, I am not sure what is the state of hasconsing in the branch of Coq you are working with, but there might be another performance issue coming from that in the long run.

[ejgallego]

Initial post updated.

Thanks for the comments, we are using Coq trunk so not sure about the hashconsing.

js_of_ocaml supports bytecode debug_event, I'll try to nail down the concrete hotspot.

[ejgallego]

Any help with debugging/creating backtraces for bytecode stack overflows would be appreciated.

[vouillon]

I have stack overflow issues with Google Chrome (version 42.0.2311.135) as well when loading ssreflect. I tried to put a breakpoint where the JavaScript stack overflow error is turned into an OCaml exception, but then I got no stack overflow...

I can't reproduce your performance issues. Both your examples feel instantaneous to me.

[ejgallego]

Hi Jérôme, thanks for your help.

chromium-browser --js-flags="--stack-size=65536" should remedy the overflow issues.

Is the below script instantaneous in your setup?: (Please remove the Require Import Coq.Init.Prelude added by default):

Require Import Ssreflect.ssreflect.
Lemma addn0 n : n + 0 = 0 + n.
Proof.
by elim: n => [|n /= ->].
Qed.

It takes around 15secs in my machine, not counting ssreflect compilation time (Chromium 43.0.2357.81 Ubuntu 15.04 (64-bit))

[ejgallego]

I couldn't find the 42.0.2311 version, but with Chrome-dev and the right options I got everything to work reasonably fast. It was good to know that it was running well on other Chrome versions, currently 43.0 seems quite bad.

Still compiling large cma files is too slow, it would be great to figure out precompilation.

[vouillon]

Indeed, this seems to be a performance bug in Chrome 43.

[vouillon]

Do you know how they are loaded by Coq? Would it be enough to redefine the #load directive to load a precompiled cma file (by putting an appropriate function in Toploop.directive_table)?