Coq Call 2023 04 25 - coq/coq GitHub Wiki

• April 25th 2023, 4pm UTC+2 (Paris time zone offset)
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• Presentation of the CEP on the future of CoqIDE (https://github.com/coq/ceps/pull/68) (Karl and Théo, 30min)
• About choosing a GUI toolkit for a remake of CoqIDE (Sylvain/Frigory33, 5min)
• Syntax highlighting of Coq code (Sylvain, 15min)
• Bringing some internationalization to Coq (Sylvain, 10min)

Roles

• Chairman: Nicolas Tabareau
• Secretary: Ali (again)

Notes

CEP

• Theo: There is a new CEP clearing up the plan with CoqIDE.
• Karl: Coq team is giving the opportunity for CoqIDE development to be given to the community.
• Karl: There might be some technicalities with transferring the CoqIDE project outside of the repo.
• Theo: CoqIDE is no longer going to be an official project.
• There might be a need for interviews if we are not familiar with the potential maintainers.
• Theo: Technical process
  • Move to Coq organization for issue transfer
• Karl: allow the maintainers to make a roadmap.
• Timing will be after 8.18 branch.
• Ali: CoqIDE shim can also be moved.
• Ali: CoqIDE doesn't have to be deleted immediately after being moved.
• Fixing deadline for CEP merging. Theo: one week.
• Hugo in chat: I don't have strong opinion on the question of how CoqIDE is maintained, but I think it is important to clarify what kind of work it means to develop a GUI. I don't think this can be reduced to the protocol it uses. I feel (but I also like to be proved wrong) that the main need for work is not in implementing a standardized communication (this is well-documented how to do) but in implementing the underlying features (e.g. how to provide custom presentations of expressions, with notations, implicit, graphical, dependency computation, cached computation, etc., etc.).
• PMP: Underlying tech of CoqIDE limits future features.
• Emilio: More important priorities for roadmap. What happens when we want to break the STM?
• Theo: STM has dim future. Use a better protocol.
• Emilio: Previous plans to remove CoqIDE had pushback.
  • We need to agree on features of a language server.
• Jim: A roadmap is a good idea; really a collection of use cases.

CoqIDE GUI toolkit

• PMP: GtkSourceView is bad.
• Replacing the GUI framework is not realistic.

Syntax highlighting

• CoqIDE has a manual highlighter.
• PMP: Coq is an extensible language so full highlighting is theoretically difficult.
• Other languages syntax highlighting is not great.
• Server-side highlighting is perhaps an option.
• Conclusion: server-side syntax highlighting is perhaps a good idea.
  • It is easy to do in LSP.
  • Maintaining multiple grammars doc, editors, etc.
  • Server-side highlighting will be delayed.
• Jim: Client-side highlighting that covers some aspects (e.g. command/tactic names) is straightforward to do. Not sure doing it perfectly on the server adds enough value to justify the effort.

Localization for Coq

• For CoqIDE: up to future maintainers.
• For Doc: it is difficult to keep consistent so unlikely but ok for tutorial doc.
• Jim: There are no mechanisms in the core team for managing that.
• Coq survey demonstrate that perhaps some other languages could be considered

Next week the CEP should be merged after feedback.