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.
@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)?
Only thing you need to use regular
.vo files in jscoq is matching OCaml / Coq deps
So for example OPAM tends not to work
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
the rest is routine
so indeed we may provide a docker image so you can run
dune build my-lib.coq-pkg and that is compatible
with the npm version
Last updated: Jun 03 2023 at 03:01 UTC