Coq Call 2023 04 04

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

Schedule

• The future of CoqIDE (Sylvain/Frigory33): 30min 1h
• Internationalization (Sylvain/Frigory33): 10min (postponed)
• Generating proof trees from Coq (Sylvain/Frigory33): 10min (postponed)

Topics

• The future of CoqIDE (Sylvain/Frigory33, 30min 1h)
  • CoqIDE vs VsCoq (LSP server)
  • Moving it to its own repository
  • Status of lablgtk3 and GUI with OCaml, using another language
  • What GUIs CoqIDE could demonstrate (ribbon, specialized fancy controls)
  • Help me finalize my recent work (mostly affecting the preferences GUI)
  • coq.lang and coq-ssreflect.lang: collaborate with GtkSourceView
• Internationalization: CoqIDE GUI, docs, something else? (Sylvain, 10min)
• Generating proof trees from Coq: be better than Coq2latex (Sylvain, 10min)

Chairman & Secretary

• Nicolas Tabareau will be chairman.
• Secretary is Ali

Notes

Points raised during the roundtable:

• We have CoqIDE, VsCoq, VsCoq2 and coq-lsp
• Core Coq developers generally don't have enough time for CoqIDE
• There is a friction between CoqIDE maintenance and general Coq maintenance
• In the current process, Coq releases require packaging CoqIDE to Coq opam archive and nixpkgs as well.
• There are other interfaces for compatibility considerations: coqtail (uses coqidetop), ProofGeneral
  • Usually anything in CI is maintained, but difficult to test exhaustively
• CoqIDE inside the Coq repo somewhat hinders its maintenance
• PMP: CoqIDE should only be moved when VsCoq2 is released
• Using CoqIDE in internal Coq dev is important, so this should be a requirement
• Where does STM stand with CoqIDE? With CoqIDE or core Coq?
  • Moving STM out is technically difficult
  • coqidetop is used by vscoq(1) and coqtail etc.
• Tension between editor and interface for Coq
• CoqIDE has some features like the debugger
• Moving CoqIDE out of Coq repository allows for volunteer maintainers to better contribute to it
  • contrary to the separation of bignums which had no maintainers
  • make CoqIDE version-independent
  • better / more flexible release cycle for CoqIDE
• When the other user interfaces like VsCoq2 and coq-lsp are ready, other interfaces PG, coqtail and CoqIDE should be migrated to use the LSP protocol rather than coqidetop
• CoqIDE is the default UI for learning settings; the alternative interfaces need to be better explained and more usable
• Maxime: Separating STM and coqidetop now is not easy
  • Separating the UI CoqIDE now is reasonable; as long as things are organized properly and not left hanging
• Karl: moving CoqIDE UI out will make it easier to separately maintain CoqIDE more finely
• CoqIDE is plagued by the choice of technology: lablgtk, OCaml etc. It could be rewritten in a different language (but is this a priority?).
• Maxime: In general Coq development, getting a major time is difficult
  • Lack of resources, organization
  • Structure of Coq is difficult to understand.
  • Understanding how the STM interacts with changes is very difficult
  • Lowering the reliance of UIs on internal details is a good thing
• Emilio: UI development needs to be more agile than the core language; STM hasn't really been improved in 10 years
• Splitting the UI makes development more agile which will be very advantageous

• Conclusion:
  • Moving the UI externally can be done
  • Everybody can contribute
  • Separate version
  • Who will work on the separation?
  • Release process
  • Who will maintain?

(jfehrle comments) I thought the plan was to solicit maintainers for an independent CoqIDE. If there isn't sufficient interest, then it doesn't make sense. (I concur with PMP that making CoqIDE a separate project has a high chance of killing it.) I'm interested in working on new/improved user-visible features and bug fixes. IMO separating out CoqIDE adds work upfront (e.g. move documentation, (?) still install CoqIDE in the Coq Platform, get CoqIDE to talk to different versions of Coq) and to run an ongoing release process that I'm not interested in taking on. I don't feel a need for more or faster releases of CoqIDE (or being "more agile"), nor am I interested in tasks such as converting CoqIDE to use LSP.