Coq Call 2023 04 25

• 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, 20min)
• About choosing a GUI toolkit for a remake of CoqIDE (Sylvain/Frigory33, 10min)
• Syntax highlighting of Coq code (Sylvain, 15min)
• Bringing some internationalization to Coq (Sylvain, 15min)

Roles

• Chairman: Nicolas Tabareau
• Secretary: X

Notes

CEP

• Theo: There is a new CEP clearing up the plan with CoqIDE.

• Karl: Coq team is giving the oppurtunity 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 mainters 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 when moving immediately

• Fixing deadline for CEP merging. Theo: one week

• 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, dependentcy 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

• PMP: GTK sourceview 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 and 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.

Localization for Coq

• For CoqIDE upto 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