Paolo Giarrusso (Jan 15 2021 at 19:31): 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
Paolo Giarrusso (Jan 15 2021 at 19:46):forgot: cc @Clément Pit-Claudel and @Emilio Jesús Gallego Arias
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 :)
Gaëtan Gilbert (Jan 15 2021 at 20:05):is it now part of Coq
no
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
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 :-)!
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
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
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
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.
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
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
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.
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.
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.
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: May 31 2023 at 02:31 UTC