Rocq Call 2026 06 16

• 16:00 Paris time (currently CEST or UTC+2:00)
• https://rendez-vous.renater.fr/rocq-call

Topics

• Exposing documentation for code editors (#22044, @shilangyu, 30min)
• future of jscoq (Gaëtan, 20min)

Roles

• Chairman: Matthieu Sozeau
• Secretary: Pierre Roux
• Attending: Sylvain Borgogno, Jim Fehrle, Gaëtan Gilbert, Thomas Lamiaux, Yann Leray, Matthieu Sozeau, Nicolas Tabareau, Marcin Wojnarowski

Notes

• Exposing documentation for code editors (#22044)

  • goal: being able to get autocomplete in editor for Corelib, Stdlib,... for lemmas, Ltac1 defs,...
  • c.f. PR #22044
  • remember former discussion on doc attribute
  • the current PR loses much formatting
  • LSP requires either plain text or markdown (PR currently uses plain text)
  • getting links should be easier than extracting documentation text (that looks pretty bad in current PR)
  • extracting things from refman seems reasonable but we won't get things from external plugins
  • currently company-coq has some (old) thing hardcoded
  • an automatic thing may show tactcis that are not to be used by users (old things only there for historical reasons for instance (and because Ltac1 has a very primitive binding meachanism leading to too much globabl things))
  • in the long run, for Ltac2, doc should come from some docstring, not the refman
  • indices could be generated by CI but not sure it's useful, and no documentation package currently to distribute it

• future of jscoq

  • currently used by platform docs (to provide interactive Rocq on webpage for tutorials)
  • stuck on very old 8.17, is there a plan to update it?
  • two backends: old one and wasm, nobody seem to know more details? maybe ask Enrico or Ali?
  • platform doc would probably already be fine with a well working vsrocq, having interactive use in browser is nice but maybe not absolutely mandatory
  • maybe Alectryon could be used on platform docs?