Support for offline cmo/cma to javascript compilation

[ejgallego]

Dear jsoo devs,

is it possible to compile *.cma files with jsoo such that they can be later used by Dynlink.loadfile?

In jscoq, we must dynamically load pretty large cma plugins, which makes the user wait for a few minutes of bytecode to js compilation sometimes (see also #334, #307). Also, having to link the whole jsoo into the output js file is a bit heavyweight.

We have seen that jsoo accepts cma/cmo input files, however the naive approach of eval'ing this js at caml_reify_bytecode doesn't work.

I'm sorry if this is possible to do, but we were clueless on how to do it. Any help hint on how to solve this issue would be greatly appreciated.

I have setup a small repository with a dynamic loading example at:

https://github.com/ejgallego/jsoo-dl-test/

The output of jsoo command line is at:

https://github.com/ejgallego/jsoo-dl-test/blob/master/outputs/module.js

and the one from the jsoo browser embedded compiler is:

https://github.com/ejgallego/jsoo-dl-test/blob/master/outputs/module_from_browser.js

I'm not even sure how to try to load the first one.

Thanks,
Emilio

[ejgallego]

Just as a reference, caching the bytecode works, there's and example at the jscoq repository.

[ejgallego]

I am in the process of checking #480 works fine with jsCoq and will close this issue if so.

[hhugo]

Make sure you use the latest master

[hhugo]

there is https://github.com/zoggy/jsoo-dynload-test for a minimal example

[ejgallego]

Hi @hhugo, I've pushed a tree trying to compile Coq's plugins offline:
https://github.com/ejgallego/jscoq/tree/offline-plugin-compilation

However, I keep getting the message "Cannot read property 'jsoo_runtime' of undefined".

Here is where the js file is generated for Coq:
https://github.com/ejgallego/jscoq/blob/offline-plugin-compilation/coq-js/Makefile#L138

Here is where I compile the plugins:
https://github.com/ejgallego/jscoq/blob/offline-plugin-compilation/cma_comp.sh#L22

I'm passing the --dynlink flag, however I seen in the jsoo examples folder the --noruntime and --runtime-only flags also exists.

Before I continue experimenting blindly, I thought I could be a good idea to ask.

What do you think the proper link sequence should be for jsCoq?

Thanks!
Emilio

[hhugo]

plugin file should look like this:

(function(joo_global_object)
   {"use strict";
    var runtime=joo_global_object.jsoo_runtime;
    ..........
    runtime.caml_register_global(11,Plugin,"Plugin");
    return}
  (function(){return this}()));

I believe that you're using eval to load the plugin ; (function(){return this}()) does not refer the global object in that case.

• option 0 - try option --disable strict when compiling the main binary
• option 1 - you should be able to load the plugin by inserting the proper <script> tag in the document.
• option 2 - can you try manually removing the (function(){return this}()) part of the plugin and load them by apply the function (that you get from eval) with the global_object ? (Js.eval_string plugin_content : < .. > Js.t -> unit) (Js.Unsafe.global)

[ejgallego]

Option 2 works like a charm! Thanks to you jsCoq is half size than before!
I didn't try option 1, I don't want to mess with the DOM in that way; option 0 fails at link time with:

Cannot read property 'length' of undefined

Note that I don't use --dynlink as it seems included in --toplevel (also linkall is needed for Coq itself) I never understood all these flags properly, I hope I'm doing the right thing here.

Thanks a lot !!!! With this jsCoq phase 1 is completed, the only missing bit for 1.0 release is moving to a Worker, but I don't expect any significant problem with that.

I'd like to specially thank you for all your prompt help, without it jsCoq wouldn't exist!

[hhugo]

AWESOME, I'll add (yet another) flag for option 2.

--dynlink is a subset of --toplevel, just using --toplevel is fine.