Skip to content

Conversation

@hhugo
Copy link
Member

@hhugo hhugo commented Sep 10, 2024

should fix #1668
@ejgallego can you confirm ?

@ejgallego
Copy link
Contributor

Thanks a lot @hhugo , this makes the Marshall error disappear, however there seems to be some other issue with 4.1.0 and dynlink (investigating that); but this patch seems to be good for the first problem.

@hhugo hhugo merged commit b2f3bae into master Sep 11, 2024
@hhugo hhugo deleted the fix-chan-marshal branch September 11, 2024 09:08
@ejgallego
Copy link
Contributor

ejgallego commented Sep 11, 2024

Did some more testing on 4.1.0-dev + this patch. I have found that:

Once I patch 78ba544 with this patch, I now get:

Uncaught exception TypeError: e.set is not a function.

when calling Sys_js.read_file "ltac_plugin.cma.js".

So maybe the patch is not compatible with 4.1.0-dev, even if it applies. Going to master, I get a different error:

"Uncaught exception TypeError: h is undefined."

This is when calling

    Js.Unsafe.((eval_string js_code : < .. > Js.t -> unit) global);

for the compiled code of ltac_plugin.cma (using --wrap-with-fun)

But likely, it seems like the above code is not the right way to load plugins in JSOO 5.8.

I dunno how to proceed further, I guess I could try to do a variation of this patch on top of 78ba544 so that things work?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

[BUG] Marshalling problems in > 4.0.0 (jsCoq / coq-lsp)

3 participants