Stream: SerAPI

Topic: Coq 8.13, serapi and Alectryon


view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 19:31):

We were trying to upgrade to 8.13, but serapi fails to compile (even when ignoring version bounds), and we guess we need it for Alectryon — or is it now part of Coq (as the serapi readme seems to hint)?

As usual, I'm sorry for nagging, but I'm curious on the upgrade plans

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 19:46):

forgot: cc @Clément Pit-Claudel and @Emilio Jesús Gallego Arias

view this post on Zulip Clément Pit-Claudel (Jan 15 2021 at 20:04):

I haven't heard of SerAPI becoming part of Coq 8.13, so I think it needs to be updated. @Emilio Jesús Gallego Arias is usually very quick to do this :)

view this post on Zulip Gaëtan Gilbert (Jan 15 2021 at 20:05):

is it now part of Coq

no

view this post on Zulip Notification Bot (Jan 15 2021 at 20:08):

This topic was moved here from #Coq users > Coq 8.13, serapi and Alectryon by Théo Zimmermann

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 23:24):

Ah, misunderstood https://github.com/ejgallego/coq-serapi#roadmap. Thanks for the estimate. And you did tell me Alectryon is likely to just keep working :-)!

Coq Protocol Playground with Se(xp)rialization of Internal Structures. - ejgallego/coq-serapi

view this post on Zulip Tej Chajed (Jan 22 2021 at 18:06):

@Emilio Jesús Gallego Arias I started porting coq-serapi to Coq 8.13 here: https://github.com/ejgallego/coq-serapi/compare/v8.12...tchajed:coq-8.13-compat?expand=1

Coq Protocol Playground with Se(xp)rialization of Internal Structures. - ejgallego/coq-serapi

view this post on Zulip Tej Chajed (Jan 22 2021 at 18:06):

I'd also love to see it updated so Alectryon keeps working with new versions of Coq

view this post on Zulip Karl Palmskog (Jan 22 2021 at 18:18):

unfortunately, porting SerAPI between Coq versions without a deep understanding of both Coq internals and the serialization libraries [i.e., you are not Emilio] is very difficult. The best solution would be if SerAPI joins Coq's CI, the Coq Platform, or becomes part of Coq itself: https://github.com/coq/platform/issues/13

SerAPI is an OCaml project which contains: a library and a set of tools for large-scale (de)serialization of Coq code to and from JSON and S-expressions, and a structured protocol for machine-to-ma...

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2021 at 10:08):

Actually is not so tricky, would we had a better system to manipulate the OCaml source it would be mostly automatic.But indeed the core parts of serialization could be incorporated into Coq proper with a bit of engineering.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2021 at 10:08):

There are two parts: serialization, which is easy; and core API changes, which indeed may be more complex.

Will update to 8.13 this week

view this post on Zulip Karl Palmskog (Jan 26 2021 at 10:18):

let's say Coq introduces a new datatype that must be serialized. I would argue that without knowing PPX basics, it's not easy to add the correct declaration/directive, even if it's conceptually straightforward

view this post on Zulip Enrico Tassi (Jan 26 2021 at 10:20):

IMO the problem is what to do when a serialized data type changes. If you do nothing, you break serapi clients.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2021 at 10:28):

Karl Palmskog said:

let's say Coq introduces a new datatype that must be serialized. I would argue that without knowing PPX basics, it's not easy to add the correct declaration/directive, even if it's conceptually straightforward

Indeed the solution for this is to have the serialization done directly in Coq, toolchain has advanced quite a bit so this is IMO feasible in the short-term without pain to developers, tho some questions do remain upstream.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2021 at 10:30):

Enrico Tassi said:

IMO the problem is what to do when a serialized data type changes. If you do nothing, you break serapi clients.

Yeah that is not different from the usual interface compat, some interfaces are more stable, some others are not. So if the client chooses to deal with a low-level, unstable interface, it can break between versions. For the protocol itself, we are quite conservative.

view this post on Zulip Karl Palmskog (Jan 26 2021 at 10:49):

I think it's fair that people who serialize Coq internals will have to deal with datatype updates, seems almost similar to advanced plugin development


Last updated: Feb 06 2023 at 05:03 UTC