Emilio Jesús Gallego Arias (Mar 05 2021 at 19:00): Emilio Jesús Gallego Arias (Mar 05 2021 at 19:00):Hi all (cc @Jasper Haag ), this is an update on the 8.13 release.
There is already a branch tracking 8.13 which is functional, however the test-suite fails due to some changes in generic arguments, which is a painful manual process to do in SerAPI, even so, it is fairly easy to fix so I'd expect it to be over soon. Would be great if we could improve this, there is issue already posted: https://github.com/ejgallego/coq-serapi/issues/82
I am not sure how hard this would be, I think not much but I didn't think about it, but indeed, Coq's "unregulated" extensibility is usually a big problem for SerAPI. There has been some discussion about how to make porting to new Coq versions easier, IMHO this is the first step.
Emilio Jesús Gallego Arias (Mar 05 2021 at 19:05):So if you checkout the 8.13 branch and run the test suite you will see failure, then a new handler for the missing genarg case has to be installed [in the right plugin]
Jasper Haag (Mar 05 2021 at 20:14):Fwiw, building the v8.13 branch locally allows our Alectryon project to successfully build once again :~) However, I would much prefer to configure our CI s.t. it installs an opam package rather than pinning a particular branch of the repository. Would it be possible for you to release a "bleeding edge" 8.13 package for SerAPI based on the current state of this PR <https://github.com/ejgallego/coq-serapi/pull/232>?
Emilio Jesús Gallego Arias (Mar 05 2021 at 20:17):Fixing the test suite shouldn't take long, then we can do a full release, the problem is that I'm really short on time this week.
Emilio Jesús Gallego Arias (Mar 05 2021 at 20:17):Releasing to opam without the test-suite working seems difficult
Jasper Haag (Mar 05 2021 at 20:19):I was under the impression that there might be issues which wouldn't crop up until a client of SerAPI uses a (potentially new) feature which isn't included in the test suite. Is that actually the case, or am I mistaken?
Jasper Haag (Mar 05 2021 at 20:20):If the current battery of tests that SerAPI has is sufficient for catching all of the breakages that crop up, it seems like it would make even more sense to include SerAPI within Coq's CI
Emilio Jesús Gallego Arias (Mar 05 2021 at 20:21):Indeed for the "genarg" problem, the test-suite is not complete
Emilio Jesús Gallego Arias (Mar 05 2021 at 20:21):we add a test case for each breakage :(
Emilio Jesús Gallego Arias (Mar 05 2021 at 20:22):This problem is as follows: plugins / Coq do extend Coq syntax in a way that we cannot check we have installed a serializer for it
Emilio Jesús Gallego Arias (Mar 05 2021 at 20:22):so the problem appears when we process a file with that particular piece of syntax
Jasper Haag (Mar 05 2021 at 20:30):It seems like the stability and availability of SerAPI w.r.t new versions of Coq are somewhat orthogonal. Based on what you've said, the process for updating SerAPI s.t. it builds and the tests pass is relatively mechanical (and thus something that Coq devs may be able to (should?) handle). However, these new versions of SerAPI will likely be quite unstable due to the "unregulated" extension of the syntax, and resolving this problem will require more coordination with the Coq team.
As a client of SerAPI who must upgrade Coq due to performance requirements (but who doesn't run SerAPI over "cutting edge" features very often), I would really like to see a solution to the availability problem ASAP, and the stability problem is relatively less important.
Emilio Jesús Gallego Arias (Mar 05 2021 at 22:13):Indeed.
Paolo Giarrusso (Mar 06 2021 at 12:06):Hm, it sounds like we could create an internal package for now?
Jasper Haag (Mar 08 2021 at 14:41):Unless @Emilio Jesús Gallego Arias has time to fix the remaining broken tests and cut a new public package this week, I think that I will go ahead with creating an internal package for the time being
Emilio Jesús Gallego Arias (Mar 08 2021 at 16:24):I think I will release 8.13 this week
Jasper Haag (Mar 08 2021 at 16:30):Have you further considered adding SerAPI to Coq's CI once you get the 8.13 branch to pass all of its tests once again?
Emilio Jesús Gallego Arias (Mar 08 2021 at 16:32):Not sure about it yet, it seems to me that it would be too much work for the developers for little gain, and it would still not solve the problem of registration of generic arguments which is IMO the main one.
Emilio Jesús Gallego Arias (Mar 08 2021 at 16:37):But indeed we should think of something, I'm sure 8.13 / 8.14 will be fine, but beyond that we lack a plan
Emilio Jesús Gallego Arias (Mar 08 2021 at 16:37):so it is good we start wider discussion
Jasper Haag (Mar 08 2021 at 17:16):Is it also the opinion of the Coq team that "[adding SerAPI to Coq's CI] would be too much work for the developers for little gain", or is this your assessment?
Jasper Haag (Mar 08 2021 at 17:17):I don't see any harm in opening an issue in Coq to integrate SerAPI into Coq's CI if they haven't chimed in definitively yet
Emilio Jesús Gallego Arias (Mar 08 2021 at 18:24):It is my opinion, with both hats on :)
Emilio Jesús Gallego Arias (Mar 08 2021 at 18:25):We will make a plan for 8.14 indeed, I suggest not to open the issue yet tho.
Jasper Haag (Mar 08 2021 at 18:32):That sounds like a workable solution from my end :~)
Jasper Haag (Mar 11 2021 at 21:04):Are we still on track for an 8.13 package release this week?
Emilio Jesús Gallego Arias (Mar 12 2021 at 15:52):https://github.com/ocaml/opam-repository/pull/18325
Jasper Haag (Mar 12 2021 at 16:06):Awesome! Thanks for releasing the package; we're looking forward to getting our Alectryon/SerAPI documentation back up and running with all of its bells and whistles :~)
Last updated: Jun 10 2023 at 06:31 UTC