Stream: jsCoq

Topic: wacoq backend consolidation


view this post on Zulip Emilio Jesús Gallego Arias (Sep 21 2021 at 15:45):

Hi @Shachar Itzhaky , I was not aware that we had diverged so much in terms of the backend, sorry I guess I was too busy as of late.

As far as I can see, we should be able to unify the OCaml backends between the two of them; I opened an issue, but I guess first we just have to cross-port the several module structure refactorings.

Is there any critical point that we should be aware of?

view this post on Zulip Shachar Itzhaky (Sep 21 2021 at 17:43):

I already pretty-much unified the module structure because the frontend uses that as well (esp. for dynamic module loading). One critical difference is that the wacoq-bin worker uses JS code (TypeScript) to load packages, so it has a JS main and WASM library functions (the main must be JS for Web Workers anyway). The jscoq worker has an OCaml main that is compiled to JS and it uses an escape to invoke XMLHttpRequest. Also, the wacoq-bin worker accepts a URI, where jscoq accepts a package name and constructs the URI internally.

view this post on Zulip Shachar Itzhaky (Sep 21 2021 at 17:44):

But actually your jscoq_interp refactoring brings them much closer together. Perhaps we can unify jscoq_interp and icoq first.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 21 2021 at 18:03):

Sounds good; thanks for the description, indeed, I think we should be able to abstract the package load interface, dune can know when we are building in each mode and select files appropiatedly.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 21 2021 at 18:03):

I will work a bit on that this week.


Last updated: Jan 30 2023 at 18:04 UTC