Yves Bertot (Feb 14 2022 at 12:05): Yves Bertot (Feb 14 2022 at 12:05):In my experience, Search is an order of magnitude or two slower than in other iteractive development environments. Is it known why? Is there a plan to avoid this?
Emilio Jesús Gallego Arias (Feb 14 2022 at 13:16):Hi @Yves Bertot , indeed , as we briefly discussed I've been toying with a kind Coq DB that I'd like to improve current Search with, but the timeframe for that is "before the summer"
In the short term, do you have an example we could test on? We currently have two backends, and there could be significant differences as the current Search in Coq is doing a full traversal of the libobject enviroment, so indeed it is almost worst case for a search algorithm IMO.
I think that using @Shachar Itzhaky 's WASM backend could improve that a lot, so if you open an issue we'd be very happy to test and look at it; we could also patch search locally so it runs faster in the regular js_of_ocaml backend
Emilio Jesús Gallego Arias (Feb 14 2022 at 13:16):You can try the WASMCoq backend yourself here
Yves Bertot (Feb 14 2022 at 13:19):You actually did not give the link for the WASMCoq backend.
Emilio Jesús Gallego Arias (Feb 14 2022 at 13:21): Emilio Jesús Gallego Arias (Feb 14 2022 at 13:21):sorry my Inria DNS are flaky today :S
Emilio Jesús Gallego Arias (Feb 14 2022 at 13:22):so I get connection cuts
Emilio Jesús Gallego Arias (Feb 14 2022 at 13:23):[actually it seems I'm having serious hardware problems, but that's offtopic]
Yves Bertot (Feb 14 2022 at 13:24):In https://coq.vercel.app/scratchpad.html
Require Import ZArith Arith List Bool.
Time Search (Pos.iter _ _ (_ + _)).
replies that the request took 33 seconds on my machine. Anything above 1 or 2 seconds is unpractical.
Pierre-Marie Pédrot (Feb 14 2022 at 13:27):it takes 9s for me on my really not beefy machine, this is bad but not as bad as you
Pierre-Marie Pédrot (Feb 14 2022 at 13:27):what browser are you using?
Emilio Jesús Gallego Arias (Feb 14 2022 at 13:46):https://coq.vercel.app/wa/scratchpad.html seems to perform much better, indeed the problem is poor algorithm in Coq plus js_of_ocaml poor tail call optimization
Emilio Jesús Gallego Arias (Feb 14 2022 at 13:46):@Yves Bertot are you sure you didn't count the time for the imports too?
Emilio Jesús Gallego Arias (Feb 14 2022 at 13:47):loading of zarith is lazy so a few megabytes have to be downloaded and processed by the worker, it still surprises me it works at all
Yves Bertot (Feb 14 2022 at 13:50):No, I was performing proofs, and all of a sudden I need to find a theorem, I call Search and it takes time, but all other operations have been reasonably fast until then. The loading of all modules has already happened. Performing the Search command twice in a row has the same cost for both of them.
Yves Bertot (Feb 14 2022 at 13:54):And you are right, instance at https://coq.vercel.app/wa/scratchpad.html is much more practical (4.3 seconds), fast enough for my teaching purposes.
Yves Bertot (Feb 14 2022 at 13:55):I can't wait till you make the wa version the default one.
Emilio Jesús Gallego Arias (Feb 14 2022 at 14:10):@Yves Bertot it is actually deployed now by default with stuff such as software foundations etc...
Emilio Jesús Gallego Arias (Feb 14 2022 at 14:10):we just need to merge a few differences from the wacoq branch to main, but to all practical purposes it is usable and can be installed
Emilio Jesús Gallego Arias (Feb 14 2022 at 14:10):I think if you are installing jscoq using node, you have the wacoq package, but @Shachar Itzhaky can confirm
Emilio Jesús Gallego Arias (Feb 14 2022 at 14:10):TTBOMK it is a drop-in replacement
Emilio Jesús Gallego Arias (Feb 14 2022 at 14:11):we hope to make progress in the Hackathon
Yves Bertot (Feb 14 2022 at 14:19):Why isn't https://coq.vercel.app/scractchpad.html directly the wa version?
Emilio Jesús Gallego Arias (Feb 14 2022 at 14:26):Yves Bertot said:
Why isn't https://coq.vercel.app/scractchpad.html directly the wa version?
I guess because no one had time to do it, but let's wait to hear from @Shachar Itzhaky .
I understand there are other places where JSOO is faster, so it may be the case that it is not a net win, but anyways when we merge the branches to select the backend should be as easy as to press a button
Emilio Jesús Gallego Arias (Feb 14 2022 at 14:26):Would be great actually if someone could add a ui element for this, our configuration panel is still very primitive; hopefully incoming eng resources may help with polishing this much more
Shachar Itzhaky (Feb 14 2022 at 16:10):Hya guys, sorry I was a bit busy preparing an exam :D
Shachar Itzhaky (Feb 14 2022 at 16:16):I have been planning on making the WASM version the default but so far have been a bit reluctant because the WASM version is in fact slightly slower than the JS one w.r.t. regular ltac execution. Did not run controlled benchmarks but compare e.g. https://coq.vercel.app/fun/coqoban.html with a corresponding development in the WASM scratchpad e.g. https://coq.vercel.app/wa/scratchpad.html?share=hb-eqomigimux. It is more apparent in Firefox and on larger boards.
Shachar Itzhaky (Feb 14 2022 at 16:21):Also having a button to switch between JS and WASM is not necessarily blocked by merging the backend codebases (which would be welcome but quite tedious). The WASM backend is already its own package, and the frontend can interface with both. Some twiddling with the Dune build might be required but it's within reach IMO.
Shachar Itzhaky (Feb 14 2022 at 16:23):The only thing is because we build two backends, we also need to build two Coq stdlibs and also all the addons have to be duplicated. That can in principle be avoided as well: we can have a build that generates two coq-core's and one coq-stdlib. But that is definitely beyond my Dune Mojo.
Emilio Jesús Gallego Arias (Feb 14 2022 at 18:40):Thanks for the feedback @Shachar Itzhaky , I added your comments to my internal TODO, it should be possible
Emilio Jesús Gallego Arias (Feb 14 2022 at 18:40):actually we can work fine with a single build
Emilio Jesús Gallego Arias (Feb 14 2022 at 18:40):jsoo takes the bytecode and transforms it into Javascript
Emilio Jesús Gallego Arias (Feb 14 2022 at 18:41):so only thing is to have the right runtime logic but I'm sure that can be done with a bit of first-class functors plus wrapping
Emilio Jesús Gallego Arias (Feb 14 2022 at 18:41):would be really surprised if it couldn't
Last updated: May 31 2023 at 04:01 UTC