Skip to content

[FEATURE REQUEST] Pre-compiled Dynlink for .cma files without linking compiler-libs/js_of_ocaml-compiler #1675

@ejgallego

Description

@ejgallego

Is your feature request related to a problem? Please describe.

jsCoq usually requires to Dynlink.loadfile of some heavy .cma files (plugins in Coq terminology to work.

Loading such files with JSOO Dynlink.loadfile support works fine, but it is usually quite slow, and moreover increases the output .js file by almost 3 MiB (50%) as it will link js_of_ocaml-compiler.

Describe the solution you'd like

I'd be great if we could precompile the .cma files to .js files, and load them without having to link the compiler.

Describe alternatives you've considered

For jsCoq and JSOO 4.0.0 , this used to work. Updating to JSOO 5.8.3 is done here https://github.com/jscoq/jscoq/pull/372/files#diff-89191e3161815dcdaf5594e6d98bfaa5ab81f742ccbeb9f5a657655c27504cdcR16, that also works, however it increases the binary size by almost 50% as we need to link the compiler.

I tried to provide my own version of toplevelReloc , which seems to be the only missing primitive for this to work, but without success.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions