Coq Call 2023 04 25
- April 25th 2023, 4pm UTC+2 (Paris time zone offset)
- https://rdv2.rendez-vous.renater.fr/coq-call
- 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)
- Chairman: Nicolas Tabareau
- Secretary: Ali (again)
- 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.
- PMP: GtkSourceView is bad.
- Replacing the GUI framework is not realistic.
- 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.
- 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.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.