Coq Call 2025 01 07 - rocq-prover/rocq GitHub Wiki

• 2025-01-07, 4pm UTC+2 (Paris time zone offset)
• https://rendez-vous.renater.fr/coq-call

Topics

• A kind word from your RM (10 minutes)
• Adding vsrocq-language-server to the rocq metapackage? (Pierre Roux, 15 minutes)
• Discuss RFC #103: social media presence for the Rocq Prover (Théo Zimmermann, 30 minutes)
• Opam packages CI plans / dune subst bug (Matthieu Sozeau, Erik Martin-Dorel, 10 minutes) (not urgent)

Roles

• Chairman: Nicolas Tabareau
• Secretary: Matthieu Sozeau
• Audience: M. Sozeau, N. Tabareau, EJG Arias, G. Gilbert, PMP, P. Roux, P. Rousselin, T. Winterhalter, T. Zimmermann, G. Melquiond, E. Tassi

Notes

• Rocq 9.0: Branching January 14th, rc1 on the 24th.

  • Emilio has two PRs that should be mergeable by the 13th.
  • Still some environment variable names mentioning COQ to fix

• Adding vsrocq-language-server to the rocq metapackage. An alternative like in debian (coqide or vsrocq or whatever is installed) would be nice, but no support from opam to do that.

  • Would require recommending to opam developers to use rocq-runtime or rocq-stdlib as dependency
  • rocq-runtime, rocq-core (with prelude) and rocq-stdlib are the new rocq packages.
  • Then rocq would be a metapackage including vsrocq-language-server

  But changes dependencies widely (pulls janestreet libraries,...), so let's be cautious. We leave this idea to the future.

• Social Network presence.

  • Reflection on opening the social network teams; various options: asking for help from Inria, open call for users to join a social media team. It's delicate to do an open call to represent the Rocq team at large, issues of legitimacy, double checking the communication? At the same time, little time from rocq-core devs to do the communication themselves.
  • Targeting different social networks? Mastodon or bluesky could be good alternatives. The RocqProver Mastodon account will become our main social network account.