Stream: Coq Platform devs & users

Topic: jscoq in platform


view this post on Zulip Emilio Jesús Gallego Arias (Aug 06 2020 at 17:17):

Karl Palmskog said:

jsCoq would be nice, but I have no idea of how it can/should be packaged. To my knowledge, there is as yet no workflow ordinary mortals can use to produce the static files required.

Actually there are two documented workflows, not ideal tho but there are certainly usable by non-experts.

Most tricky part is getting to compile extra .vo files; there is an upcoming much simpler workflow based on docker + dune which should help producing the files.

view this post on Zulip Karl Palmskog (Aug 06 2020 at 17:25):

@Emilio Jesús Gallego Arias so then I guess the question in this thread reduces to: if the Coq Platform was delivered as a Docker image including files for jsCoq, would one be able to use that Docker image to produce jsCoqified code? It seems like you are implying the answer "yes" (with careful setup inside the image)?

view this post on Zulip Emilio Jesús Gallego Arias (Aug 06 2020 at 18:08):

Only thing you need to use regular .vo files in jscoq is matching OCaml / Coq deps

view this post on Zulip Emilio Jesús Gallego Arias (Aug 06 2020 at 18:08):

So for example OPAM tends not to work

view this post on Zulip Emilio Jesús Gallego Arias (Aug 06 2020 at 18:09):

I mean matching in that jscoq has to be compiled with the same OCaml toolchain that was used to compile coqc which generates the .vo files

view this post on Zulip Emilio Jesús Gallego Arias (Aug 06 2020 at 18:09):

the rest is routine

view this post on Zulip Emilio Jesús Gallego Arias (Aug 06 2020 at 18:09):

so indeed we may provide a docker image so you can run dune build my-lib.coq-pkg and that is compatible

view this post on Zulip Emilio Jesús Gallego Arias (Aug 06 2020 at 18:09):

with the npm version


Last updated: Jan 30 2023 at 11:03 UTC