Benedikt Ahrens (Apr 26 2022 at 09:22): Benedikt Ahrens (Apr 26 2022 at 09:22):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.
Ali Caglayan (Apr 26 2022 at 09:47):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
Ali Caglayan (Apr 26 2022 at 09:47):Here is the HoTT library for example: https://x80.org/rhino-hott/
Ali Caglayan (Apr 26 2022 at 09:48):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.
Ali Caglayan (Apr 26 2022 at 09:49):cc @Emilio Jesús Gallego Arias
Hanneli Tavante (Apr 26 2022 at 14:30):"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
Emilio Jesús Gallego Arias (Apr 26 2022 at 16:54):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.
Emilio Jesús Gallego Arias (Apr 26 2022 at 16:56):@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.
Benedikt Ahrens (Apr 26 2022 at 17:34):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.
Emilio Jesús Gallego Arias (Apr 26 2022 at 17:40):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.
Benedikt Ahrens (Apr 27 2022 at 11:25):@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.
Emilio Jesús Gallego Arias (Apr 27 2022 at 11:29):@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.
Emilio Jesús Gallego Arias (Apr 27 2022 at 11:29):I guess I would just start from some of the addons in https://github.com/jscoq/ and do unitmath that way
Benedikt Ahrens (Apr 27 2022 at 16:39):Thanks, I'll take a look!
Last updated: Jan 31 2023 at 10:01 UTC