Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Javascript Target #18

Closed
3 of 5 tasks
ejgallego opened this issue Jun 24, 2016 · 4 comments · Fixed by #318
Closed
3 of 5 tasks

Javascript Target #18

ejgallego opened this issue Jun 24, 2016 · 4 comments · Fixed by #318
Assignees
@ejgallego
Labels
fixed by: flèche in-progress wontfix

Comments

@ejgallego
Copy link
Collaborator

ejgallego commented Jun 24, 2016 •
edited
Loading

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.
  • Add js makefile target, SerTop Worker object.
  • Import library/fs manager.
  • Investigate size reduction strategy. SerTop is 3MiB larger than jsCoq. Core is adding 1.8MiB so it is a large price to pay.
@ejgallego ejgallego self-assigned this Jun 24, 2016
@ejgallego ejgallego added this to the 0.2 milestone Jun 24, 2016
ejgallego added a commit that referenced this issue Jun 24, 2016
@ejgallego
[js] Add javascript version of SerTop
fb6d01f 
Refs #18. This is still experimental, but we can now use sertop from the
browser as a Worker.

The jsCoq filesystem is not ported yet so you are limited to no prelude.
Asynchronous support is also not available in this version.
ejgallego added a commit that referenced this issue Jun 24, 2016
@ejgallego
[js] Add javascript version of SerTop
c2ecead 
Refs #18. This is still experimental, but we can now use sertop from the
browser as a Worker.

The jsCoq filesystem is not ported yet so you are limited to no prelude.
Asynchronous support is also not available in this version.
@ejgallego
Copy link
Collaborator Author

ejgallego commented Jun 24, 2016 •
edited
Loading

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/

ejgallego added a commit that referenced this issue Jun 25, 2016
@ejgallego
[js] Remove Core_kernel dependency.
2f5943a 
We optimize the size of the generated bytecode by not including Core_kernel.

Still, the price we pay for Sexplib + serialization seems too high wrt
to the standard jsCoq version (+ ~2MiB).

Refs #18.
ejgallego added a commit that referenced this issue Jun 25, 2016
@ejgallego
[js] Remove Core_kernel dependency.
d51fc03 
We optimize the size of the generated bytecode by not including Core_kernel.

Still, the price we pay for Sexplib + serialization seems too high wrt
to the standard jsCoq version (+ ~2MiB).

Refs #18.
ejgallego added a commit that referenced this issue Jun 25, 2016
@ejgallego
[build] Finer linking flags, some size savings.
9008867 
This indeed seems to save 1.8 MiB of bytecode! Refs #18.
Ptival pushed a commit to Ptival/coq-serapi that referenced this issue Jul 14, 2017
@ejgallego @Ptival
[js] Add javascript version of SerTop
83d91a7 
Refs rocq-archive#18. This is still experimental, but we can now use sertop from the
browser as a Worker.

The jsCoq filesystem is not ported yet so you are limited to no prelude.
Asynchronous support is also not available in this version.
Ptival pushed a commit to Ptival/coq-serapi that referenced this issue Jul 14, 2017
@ejgallego @Ptival
[js] Remove Core_kernel dependency.
2664a92 
We optimize the size of the generated bytecode by not including Core_kernel.

Still, the price we pay for Sexplib + serialization seems too high wrt
to the standard jsCoq version (+ ~2MiB).

Refs rocq-archive#18.
Ptival pushed a commit to Ptival/coq-serapi that referenced this issue Jul 14, 2017
@ejgallego @Ptival
[build] Finer linking flags, some size savings.
ce64469 
This indeed seems to save 1.8 MiB of bytecode! Refs rocq-archive#18.
@joelburget
Copy link

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

@ejgallego
Copy link
Collaborator Author

ejgallego commented Mar 20, 2018 •
edited
Loading

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 ejgallego modified the milestones: 0.2, 0.6.0 Sep 20, 2018
@ejgallego ejgallego modified the milestones: 0.6.0, 0.6.1 Feb 4, 2019
@ejgallego ejgallego modified the milestones: 0.6.1, 0.7.0 Mar 27, 2019
@ejgallego ejgallego mentioned this issue May 18, 2019
Closed
@ejgallego ejgallego modified the milestones: 0.7.0, 0.7.1 Nov 4, 2019
@ejgallego ejgallego modified the milestones: 0.7.1, 0.11.0 Jan 24, 2020
@ejgallego ejgallego modified the milestones: 0.11.0, 0.11.1 May 13, 2020
@ejgallego ejgallego modified the milestones: 0.11.1, 0.11.2 Jun 2, 2020
@ejgallego ejgallego removed this from the 0.11.2 milestone Aug 26, 2020
@ejgallego ejgallego added this to the 0.12.2 milestone Aug 26, 2020
@ejgallego ejgallego modified the milestones: 0.12.2, 0.13.1 Mar 12, 2021
@ejgallego ejgallego modified the milestones: 0.13.1, 0.14.0 Sep 21, 2021
@ejgallego ejgallego modified the milestones: 0.14.0, 0.16.0 Jun 15, 2022
@ejgallego ejgallego removed this from the 0.16.0 milestone Sep 8, 2022
ejgallego added a commit that referenced this issue Feb 14, 2023
@ejgallego
[meta] Put SerAPI in maintenance mode.
7224c22 
Thanks to everyone that helped and used this project for almost 7
years!

The following issues are solved by coq-lsp:

closes #252, closes #261, closes #234, closes #202, closes #117,
closes #49, closes #32, closes #26, closes #24, closes #21,
closes #18, closes #13
@ejgallego
Copy link
Collaborator Author

Flèche issue ejgallego/coq-lsp#233

@ejgallego ejgallego mentioned this issue Feb 14, 2023
Merged
ejgallego added a commit that referenced this issue Feb 14, 2023
@ejgallego
[meta] Put SerAPI in maintenance mode.
946211b 
Thanks to everyone that helped and used this project for almost 7
years!

The following issues are solved by coq-lsp:

closes #252, closes #261, closes #234, closes #202, closes #117,
closes #49, closes #32, closes #26, closes #24, closes #21,
closes #18, closes #13
ejgallego added a commit that referenced this issue Feb 14, 2023
@ejgallego
[meta] Put SerAPI in maintenance mode.
436a0e4 
Thanks to everyone that helped and used this project for almost 7
years!

The following issues are solved by coq-lsp:

closes #252, closes #261, closes #234, closes #202, closes #117,
closes #49, closes #32, closes #26, closes #24, closes #21,
closes #18, closes #17, closes #13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@ejgallego ejgallego

Labels
fixed by: flèche in-progress wontfix
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

[meta] Put SerAPI in maintenance mode. rocq-archive/coq-serapi
2 participants
@joelburget @ejgallego