1. Forum
  2. Usenet
  3. LINUX.DEBIAN.MAINT.OCAML.

  • Question about a package mixing Coq and OCaml

    From =?UTF-8?Q?Jean-Christophe_L=c3=a9ch@21:1/5 to All on Thu Mar 2 13:20:01 2023
    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

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From julien.puydt@gmail.com@21:1/5 to All on Thu Mar 2 13:50:02 2023
    Hi,

    Le jeudi 02 mars 2023 à 12:00 +0000, Jean-Christophe Léchenet a écrit :
     The interrogation I have
    is: can we use as a source the extracted code,

    No: the source code is what the developers work on.

    If it's pre-processed, it's not source anymore.

    Cheers,

    J.Puydt

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From =?UTF-8?Q?St=c3=a9phane_Glondu?=@21:1/5 to All on Thu Mar 2 13:50:02 2023
    Dear Jean-Christophe,

    Le 02/03/2023 à 13:00, Jean-Christophe Léchenet a écrit :
    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.

    In Debian (main), everything must be built from source which, in your
    case, is the "real" Coq/OCaml source. The idea is that if the source is modified, one must be able to rebuild the package. The Debian "source"
    package must be self-contained and, ideally, it should not contain
    prebuilt stuff.


    Cheers,

    --
    Stéphane

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)