Coq Call 2024 12 17 - rocq-prover/rocq GitHub Wiki

Notes

  • Coq/Rocq and social networks (Matthieu, 10min)

    Some members of the development team have proposed to leave Twitter/X. Discussion has moved to Bluesky and Mastodon. It is possible to use preferentially bluesky or mastodon, but staying on Twitter/X is a good way to provide easy information to people asking. Several voices are favorable to staying. In particular, there is a risk that taking the decision to leave is understood as a political statement, which we do not really want to emit. Also, exiting at the moment of changing the name is not necessarily a good thing, as we would prefer the attention to be drawn on the latter aspect of our communication.

  • rocq cli (Gaëtan, 15min)

    Gaëtan discusses a table explaining what commands are changing names and how each command gets called by others. A point that is slightly surprising is that the rocq binary will have statically linked in it a variety of code that has little in common : coqwc coq_makefile etc. Anyway, it should be understood that the rocq binary does not depend on the kernel, and calls other programs that do depend on it. These programs are placed in a sub-directory that rocqis aware of, but which is not in the path. It is decided in this meeting to stop providing coqtop.byte (which whas only useful for people using Drop to debug their own code). But it seems that using the ocaml debugger is more practical that the ancient approach using Drop.

The discussion then drifts on other aspects of developing: documentation of debugging facilities, proposal to support only recent versions of Ocaml (4.14).

Roles

  • Chairman: Matthieu Sozeau
  • Secretary: Yves Bertot
  • Audience: Enrico Tassi, Emilio Gallego Arias, Pierre-Marie Pédrot, Gaëtan Gilbert, Pierre Roux