Emilio Jesús Gallego Arias (Aug 06 2020 at 17:17): 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.
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)?
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
Emilio Jesús Gallego Arias (Aug 06 2020 at 18:08):So for example OPAM tends not to work
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
Emilio Jesús Gallego Arias (Aug 06 2020 at 18:09):the rest is routine
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
Emilio Jesús Gallego Arias (Aug 06 2020 at 18:09):with the npm version
Last updated: Apr 20 2024 at 04:02 UTC