I'm playing with a Haskell library for talking to coqidetop, which has led me to digging into the XML protocol and corresponding ocaml interfaces. I've seen a few references to the full document model being a DAG (most notably the out-of-date reference linked from the coq source), but as far as I can tell you can only add a node with a single parent. Is this correct? Is there any way to tell coq "this new command X should not be run until Y and Z both finish" other than waiting for their status to change client-side?
It's not the client that draws the dag. The client should "add" as many sentences as possible before calling "observe" and it is up to the STM to build a dag. The STM classifies sentences, and create fork/join in correspondence of the beginning and end of proofs. In this way it can later skip over proofs.
I see. I also noticed "observe" is in the stm interface but the XML protocol doesn't have anything corresponding to it (and, indeed, there is only one call to "observe" in the codebase outside of the stm module itself). Do I still have to call it, or does coqidetop just process in the background as it goes?
Oh, in the XML protocol the message is called "goals" IIRC
observe lets you observe any node in the dag, while the XML protocol calls finish (which observes the tip of the dag) and then returns the goals, if any. Hence the name of the message
The XML protocol is an adaptation of the pre-STM protocol... this is why the two APIs don't quite match.
Is there a way to directly use the STM protocol without linking ocaml?
Also, my current plan is to just construct Gallina terms directly, not using proofs/tactics... In that case do I just lose out on async processing altogether?
(seems odd to have machine generated metacode when I can just do machine generated code, but maybe that's the wrong thinking)
This project https://github.com/ejgallego/coq-serapi provides a
sertop command to which you can talk using S-expressions and whose protocol matches more closely the one of the STM AFAIU.
Even with serapi I'm afraid you can't create terms as ASTs, only as strings IIRC.
Can you say a little more what your use case is and why the library must be in haskell?
Yeah was expecting it would need to be strings.
The library is a diagram manipulation GUI for playing around in category theory, I want to be able to export the proofs and constructions to coq to validate and to be able to define categories in coq and manipulate them (in a constrained way, of course) in the GUI. I could do it in ocaml if that's much better but I've never written ocaml :smile:
The ML APIs are not very nice/polished. As far as I understand generating text is not too bad for you.
The point is that generating nice text is hard, but generating a bare bone term with abundance of parentheses is quite trivial.
Last updated: Feb 09 2023 at 00:03 UTC