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.
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]
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>?
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.
Releasing to opam without the test-suite working seems difficult
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?
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
Indeed for the "genarg" problem, the test-suite is not complete
we add a test case for each breakage :(
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
so the problem appears when we process a file with that particular piece of syntax
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.
Hm, it sounds like we could create an internal package for now?
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
I think I will release 8.13 this week
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?
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.
But indeed we should think of something, I'm sure 8.13 / 8.14 will be fine, but beyond that we lack a plan
so it is good we start wider discussion
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?
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
It is my opinion, with both hats on :)
We will make a plan for 8.14 indeed, I suggest not to open the issue yet tho.
That sounds like a workable solution from my end :~)
Are we still on track for an 8.13 package release this week?
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: Mar 02 2024 at 16:01 UTC