Javascript Target

[ejgallego]

We want to compile SerApi to Javascript, Coq will run in a worker thread.

Thanks to jsCoq how to this is well understood. Once this is complete, jsCoq will just use SerAPI as its Coq implementation. For now, we will just communicate sending strings with the usual Sexp.

To do list is:

• [ ] Notifications for the library manager/redesign.
• [ ] Native JSON encoding of feedback.
• [x] Add js makefile target, SerTop Worker object.
• [x] Import library/fs manager.
• [x] Investigate size reduction strategy. SerTop is 3MiB larger than jsCoq. Core is adding 1.8MiB so it is a large price to pay.

[ejgallego]

Ok, basic support added, see a build is available at:

https://github.com/ejgallego/jscoq-builds/tree/serapi

an emulator is at:

https://x80.org/rhino-hawk/

[joelburget]

How much work would the JSON encoding be? That would be really nice to have.

[ejgallego]

It should not be a lot of work and in fact I was looking forward to try it soon. I am not sure the json serializer will be able to tackle the full of Coq however.

Note that an easier approach would be to convert s-expressions to JSON in a systematic way using Javascript. This is the approach that Peacoq used and I think it worked pretty well.

Encoding is fairly easy, a sexp (A B C) is translated to ["A", "B", "C"], and a sexp ((foo bar) (bar foo)) is translated to { "foo": "bar, "bar": "foo" }.

[ejgallego]

Flèche issue https://github.com/ejgallego/coq-lsp/issues/233