Stream: jsCoq

Topic: Removing Put / Get?


view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 16:13):

Hi @Shachar Itzhaky , turns out that Put / Get are only used by jsoo

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 16:13):

So if we have jsoo use the server-side package manager

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 16:14):

they get unused.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 16:14):

I'm unsure if we should get rid of them (for now); it is clear that we need a server-side FS API for the git backend, but my impression is that we may need to think about it from scracth, WDTY?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 16:19):

In particular I think stuff like the git js mode

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 16:19):

assume their own fs implementation

view this post on Zulip Shachar Itzhaky (Oct 18 2022 at 16:36):

yeah well I was also using Get/Put for compiling in the browser

view this post on Zulip Shachar Itzhaky (Oct 18 2022 at 16:36):

but perhaps that's not the right way either

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 17:24):

Well for sure we need an API to manage the FS of the worker

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 19:52):

I guess the main question is if the API will have to transfer files from client / server

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 19:52):

or will just request the server to download/upload urls

view this post on Zulip Shachar Itzhaky (Oct 18 2022 at 19:58):

at least compiled .vo files have to be sent from the server to the client. But perhaps we can send all of the compiled files in one bundle instead of having the Get each one; same for passing the sources from the client to the server.

view this post on Zulip Shachar Itzhaky (Oct 18 2022 at 19:59):

for pkgs yeah it seems that only the url needs to be passed

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:00):

When do the .vo files go back to the client?

view this post on Zulip Shachar Itzhaky (Oct 18 2022 at 20:02):

the previous way I did it was a mess: the server would send a ["Compiled", "out.vo"] to the client, then the client would ["Get", "out.vo"].

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:09):

why does the client need the .vo file?

view this post on Zulip Shachar Itzhaky (Oct 18 2022 at 20:11):

good point actually; for checking documents that use the .vo the files might as well just stay in the server; tho I found that it is better to launch a separate Worker for batch compilation, so at least the files need to transfer between the "compile" worker and the "interactive" worker.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:11):

that's a very good point

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:12):

Would be nice if the FS would be actually be a sharedmemory worker or something like that

view this post on Zulip Shachar Itzhaky (Oct 18 2022 at 20:12):

funny you should mention that, I actually implemented one for WASM. but it's not very stable and kinda slow.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:13):

This kind of stuff makes sense IMHO as for example once we get the core stable

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:13):

I'd much like to have a worker that is contionously fed by the main worker

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:14):

and whose job is to run search all the time to present suggestions to the user :D


Last updated: Jan 30 2023 at 17:03 UTC