I am fascinated by the possibility of using Coq in the browser, in particular, for education - thanks for building jsCoq.
Is there a way to build and host one's own instance of jsCoq, with more libraries (I am particularly interested in UniMath) and custom commandline options (such as -noinit
)? I would be very grateful for any pointers.
Hi Benedikt. AFAIK the answer to your questions are yes. We have built and hosted the HoTT library using jscoq in the past (so that means -noinit). The examples from the README.md for jscoq contains various project setups: https://github.com/jscoq/jscoq#examples
Here is the HoTT library for example: https://x80.org/rhino-hott/
I am not sure of the details of setting these up however so you will have to wait for more knowledgeable people to chime in.
cc @Emilio Jesús Gallego Arias
"build and host one's own instance of jsCoq" <- I've been doing it with a Docker image https://github.com/jscoq/jscoq/blob/v8.14/etc/docker/Dockerfile
Using docker is your best bet for now. We need to improve the build setup a bit better tho, if you have cycles to help we'd be very happy to help. There is an upcoming dune hackathon that should solve the most pressing issue of building soundly multiple theories.
The way I see the jsCoq distro tho is inspired by the system Shachar implemented w.r.t. lazy loading. It should be possible just to have jsCoq load lazily a lot of libs. One little problem tho is how to handle versioning, we don't have anything in the build system to support multiple versions.
@Benedikt Ahrens note that these days HoTT doesn't require a special build anymore, so with a bit of work we should be able to have it standard in the jsCoq distribution.
Emilio Jesús Gallego Arias said:
Benedikt Ahrens note that these days HoTT doesn't require a special build anymore, so with a bit of work we should be able to have it standard in the jsCoq distribution.
That would be fantastic. Note that I am interested in UniMath, not in HoTT. However, the situation is similar; in particular, both are part of the Coq Platform.
Great @Benedikt Ahrens ; I think packaging unimath should be simple, main problem may be the documentation of how to do it.
So I suggest we try together and fixup the jscoq docs on the way.
@Emilio Jesús Gallego Arias Yes, that would be great. I don't have any knowledge how to use docker, but I am happy to spend time on learning it.
@Benedikt Ahrens docker knowledge should not really required, we use docker to build as a way to provide a common VM for all users, but the build script is just a few calls to the makefiles. Coq doesn't have an ABI so Docker provides a reproducible enviroment for everyone.
I guess I would just start from some of the addons in https://github.com/jscoq/ and do unitmath that way
Thanks, I'll take a look!
Last updated: Jan 31 2023 at 10:01 UTC