Hugo Herbelin (Jun 29 2023 at 14:59): Hugo Herbelin (Jun 29 2023 at 14:59):I made a wiki page about the general architecture of Coq user interfaces. It was useful for me to better understand the articulations between different approaches and I hope it will be useful for others. Don't hesitate to comment, amend, refine, ...
Doing this summary leads me to feel that we should eventually be able to arrive to a quite modular approach to user interfaces based on a standardized proof-assistant-oriented extension of LSP.
Karl Palmskog (Jun 29 2023 at 20:41):nice summary, but I'm missing the really low level interfaces like Serlib and PyCoq. For some interaction, just consuming/manipulating Coq data structures is essential (such as looking at token level to do formatting)
Hugo Herbelin (Jun 30 2023 at 12:08):Thanks for being supportive.
I'm missing the really low level interfaces like Serlib and PyCoq
I have no idea. I'll ask around to understand better where to put them (or maybe someone reading this knows).
Karl Palmskog (Jun 30 2023 at 12:13):maybe one way to think about it is that Coq has both "user" and "programming" interfaces, and many of them overlap in strange ways
Karl Palmskog (Jun 30 2023 at 12:15):for example coqtop is I guess a user interface of sorts, but arguably is used programmatically by ProofGeneral
Théo Zimmermann (Jun 30 2023 at 14:28):coq-lsp can also be used programmatically to achieve some of the same objectives as with SerAPI / PyCoq.
Théo Zimmermann (Jun 30 2023 at 14:33):@Pierre Courtieu: you added Ltac debugger to the list of PG features. Do you have any link to the documentation for this feature? How does it compare to the CoqIDE Ltac debugger? Should the latter be qualified as "Visual Ltac debugger" to distinguish?
Pierre Courtieu (Jun 30 2023 at 14:49):@Théo Zimmermann let me have a look at coqide debug mode before I answer :-)
Théo Zimmermann (Jun 30 2023 at 14:51):https://coq.inria.fr/refman/practical-tools/coqide.html#debugger
Pierre Courtieu (Jun 30 2023 at 14:51):and actually pg debugging mode seems currently broken...
Pierre Courtieu (Jun 30 2023 at 14:56):because of a change in debugger messaging.
OK let us remove "Ltac Debugger" for pg :-)
Théo Zimmermann (Jun 30 2023 at 14:58):Could it be related to the introduction of the visual debugger in CoqIDE in fact? Feel free to open an issue and to tag Jim.
Pierre Courtieu (Jun 30 2023 at 15:09):I don't know. I will investigate. Anyway the graphical breakpoints of coqide is much nicer.
Emilio Jesús Gallego Arias (Jun 30 2023 at 20:02):Théo Zimmermann said:
coq-lsp can also be used programmatically to achieve some of the same objectives as with SerAPI / PyCoq.
Indeed there is now a fcc compiler that will be in the upcoming release which removes the need to spawn a lsp client, also it is extensible in OCaml and Python (which covers a lot of use cases that required hacks to SerAPI
Emilio Jesús Gallego Arias (Jun 30 2023 at 20:02):)
Hugo Herbelin (Jul 01 2023 at 10:07):Could finally decode it: fcc = Flèche Coq Compiler, that is an executable to access most of the features of Flèche on the command line without having to communicate over LSP.
I did not get what it means to be "extensible in OCaml and Python" though.
Emilio Jesús Gallego Arias (Jul 03 2023 at 13:58):Happy to find a better name (see issue https://github.com/ejgallego/coq-lsp/issues/472 )
Extensible means that you can write plugins in both OCaml and Python, see example plugin at https://github.com/ejgallego/coq-lsp/tree/main/plugins/simple
A lot more work on documentation in required indeed
Théo Zimmermann (Jul 03 2023 at 14:34):IMHO you shouldn't care about the name before the question of the renaming of Coq itself is concluded.
Emilio Jesús Gallego Arias (Jul 03 2023 at 14:36):@Théo Zimmermann indeed that is one of the reasons I picked fcc for now as interim name, but SerAPI was also an interim name and it stuck (and not a very good one IMHO)
Last updated: Oct 13 2024 at 01:02 UTC