• ITP Jasmin and EasyCrypt, would like to join the OcamlTaskForce

    From Marcel =?utf-8?Q?Fourn=C3=A9?=@21:1/5 to All on Fri Jul 23 17:20:01 2021
    Hello!

    I maintain some packages for the Debian Haskell Group and I am beginning to package Jasmin and EasyCrypt, which are both implemented in Ocaml (and Coq), so I'd like to hear about your best practices, learn from them and put the packages under my own and
    team maintenance when they are done. I am only a Debian Maintainer, so I will need a sponsor if you deem the packages good enough.
    In general, I'd like to join the group to help maintaining the Debian Coq environment, since I'm interested in formal proofs and have started with Coq.

    Cheers

    --
    Marcel FOURNÉ

    Please note that I honour and respect boundaries around personal
    time, well-being, care-taking and the rest.
    Should you receive correspondence from me during a time that you're
    engaging in any of the above, please protect your time and wait to
    respond until you're next working or in front of a PC.
    Prioritize joy and not e-mail when and where you can.

    -----BEGIN PGP SIGNATURE-----

    iQIzBAEBCgAdFiEEXbhschEgOnT3vMD1i0eZP9NrHYAFAmD63fEACgkQi0eZP9Nr HYADQw//Xzb+0zs6IXC378gNWB3rS6VSzaNZqniR0ndSfDQTlpgKpGho8prQRG1q RhQF/yYPFP70HGZUXPuz4cmI6dvO0n7jeix4tZFU4RwZHXZjHBCF94xL4plRw0k/ MTIOgxrtbCVRkDFeAuIn+CzaxVijk1rtNPio41Qg/Y36vziGm8syVNWZheog8zfI Fvxt9+OhkhH3Z1/BqUmMVAHvvP0jKqKtXr5a9M5R8LKv6DG4Ggqq5lR/L83hJwL+ Y8yIjwlO0OrrrO79bDeAeRQoykLHXV6wfDxatrYxaHr+kCh//Injqh++jCrb+gvk AMq9aZ6VoAQeBeFukfUdATKUQlVt/vRxdhgtoFhzZCK7SzlbLpXQ8Cu9BMVIRUfC R56y2fgzBE84suvW9Eare2ZyDpFjoKhn+v6AKF0V6uuiMFY0K5ooIL7nk8r5avOM xliVRjWbi9Mz8Xu9JrQs7KVnw9kCNVh3p5Q0UwmvWwoDNsnwoCntc6DJ0PT9fF/0 /SteXy2uWq5hdbMrSmCICiVPUGwhD61GesMdjFHJt7bJzYuL1v3CdLPRUuAu+NRp 9++kYXq3vrCPbljfDrgtflm4JW9ahtEKxQ5SPguFeNwup72QDgOawtjGzcBkxKfS 2a4sRXouGI1ZZAF3B8TiQLp4yBnCf2BZewnd6k68jzFebX8+i30=
    =Aj7L
    -----END PGP SIGNATURE-----

    --- 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 Wed Sep 1 17:30:02 2021
    Dear Marcel,

    Le 23/07/2021 à 17:19, Marcel Fourné a écrit :
    I maintain some packages for the Debian Haskell Group and I am beginning to package Jasmin and EasyCrypt, which are both implemented in Ocaml (and Coq), so I'd like to hear about your best practices, learn from them and put the packages under my own
    and team maintenance when they are done. I am only a Debian Maintainer, so I will need a sponsor if you deem the packages good enough.
    In general, I'd like to join the group to help maintaining the Debian Coq environment, since I'm interested in formal proofs and have started with Coq.

    Thank you for your interest in contributing to Debian!

    Even though it is a bit outdated, you should start by reading our policy
    in the dh-ocaml package. It documents our practices before the advent of
    dune, and can help in understanding how OCaml-related Debian packages
    are structured.

    In general, for creating a new package, I would suggest looking at a
    similar existing package (in ocaml-team on salsa).

    For Coq theories, there are not many packages so practices specific to
    this area are yet to be defined :-) I am aware of ssreflect and
    coq-float (which is in bad shape).

    Feel free to ask more specific questions, or send your sponsoring
    requests to this mailing-list.


    Cheers,

    --
    Stéphane

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