Stream: Coq users

Topic: Is STM a dag or a tree?


view this post on Zulip Shea Levy (Sep 01 2020 at 15:27):

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?

view this post on Zulip Enrico Tassi (Sep 01 2020 at 17:00):

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.

view this post on Zulip Shea Levy (Sep 01 2020 at 17:05):

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?

view this post on Zulip Enrico Tassi (Sep 01 2020 at 17:14):

Oh, in the XML protocol the message is called "goals" IIRC

view this post on Zulip Enrico Tassi (Sep 01 2020 at 17:15):

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

view this post on Zulip Enrico Tassi (Sep 01 2020 at 17:16):

The XML protocol is an adaptation of the pre-STM protocol... this is why the two APIs don't quite match.

view this post on Zulip Shea Levy (Sep 01 2020 at 17:35):

Is there a way to directly use the STM protocol without linking ocaml?

view this post on Zulip Shea Levy (Sep 01 2020 at 17:36):

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?

view this post on Zulip Shea Levy (Sep 01 2020 at 17:37):

(seems odd to have machine generated metacode when I can just do machine generated code, but maybe that's the wrong thinking)

view this post on Zulip Théo Zimmermann (Sep 01 2020 at 17:45):

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.

view this post on Zulip Shea Levy (Sep 01 2020 at 17:48):

Ah, thanks!

view this post on Zulip Enrico Tassi (Sep 01 2020 at 18:09):

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?

view this post on Zulip Shea Levy (Sep 01 2020 at 18:13):

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:

view this post on Zulip Enrico Tassi (Sep 02 2020 at 08:02):

The ML APIs are not very nice/polished. As far as I understand generating text is not too bad for you.

view this post on Zulip Enrico Tassi (Sep 02 2020 at 08:04):

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