Rocq Call 2026 06 16 - rocq-prover/rocq GitHub Wiki

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?