[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Question about a package mixing Coq and OCaml



Dear OCaml maintainers,

I am one of the developers of the Jasmin compiler (https://github.com/jasmin-lang/jasmin) written both in Coq and OCaml. The compilation procedure is in two steps: first, extract the Coq code into OCaml code ; second, compile the OCaml code. We already provide an opam package (https://opam.ocaml.org/packages/jasmin/), and, since we do not want the user to have to install Coq, the source we distribute is the OCaml code produced by the first step I have just described.

We are considering building a debian package for Jasmin. As a first step, we just want to produce a .deb we will distribute ourselves (there is an parallel attempt to integrate Jasmin in debian (https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=991435), but I do not know what its status is, I asked its author). The interrogation I have is: can we use as a source the extracted code, like we do for the opam package, or do we have to use the "real" Coq/OCaml source? I mean, while we distribute the package ourselves, we can do more or less whatever we want, I guess, but it would be better to do it in the debian spirit from the beginning.

Best regards,

Jean-Christophe Léchenet


Reply to: