Stream: jsCoq

Topic: Removing Put / Get?

Emilio Jesús Gallego Arias (Oct 18 2022 at 16:13):

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

Emilio Jesús Gallego Arias (Oct 18 2022 at 16:13):

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

Emilio Jesús Gallego Arias (Oct 18 2022 at 16:14):

they get unused.

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?

Emilio Jesús Gallego Arias (Oct 18 2022 at 16:19):

In particular I think stuff like the git js mode

Emilio Jesús Gallego Arias (Oct 18 2022 at 16:19):

assume their own fs implementation

Shachar Itzhaky (Oct 18 2022 at 16:36):

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

Shachar Itzhaky (Oct 18 2022 at 16:36):

but perhaps that's not the right way either

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

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

Emilio Jesús Gallego Arias (Oct 18 2022 at 19:52):

or will just request the server to download/upload urls

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.

Shachar Itzhaky (Oct 18 2022 at 19:59):

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

Emilio Jesús Gallego Arias (Oct 18 2022 at 20:00):

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

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"].

Emilio Jesús Gallego Arias (Oct 18 2022 at 20:09):

why does the client need the .vo file?

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.

Emilio Jesús Gallego Arias (Oct 18 2022 at 20:11):

that's a very good point

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

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.

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

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

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: May 31 2023 at 03:30 UTC