@Emilio Jesús Gallego Arias : currently coq-serapi fails in the Coq Platform .dev build. I don't quite understand what the difference to the Coq CI build is - both should use master from Coq and SerAPI.
One question: what is the recommended way to do an opam based .dev build. The opam file in the serapi repo restricts the Coq version unless I pin serapi (if I understand this right). There is also no coq-serapi.dev package in extra-dev, so I am currently using a local package.
@Michael Soegtrop indeed it seems to be building fine in Coq master, where can we see the build failure log?
@Emilio Jesús Gallego Arias : the start of the serapi log is (https://github.com/coq/platform/actions/runs/3390707284/jobs/5635143823#step:5:3031) - the failure is (https://github.com/coq/platform/actions/runs/3390707284/jobs/5635143823#step:5:3039)
7 File "serlib/ser_ppextend.mli", line 36, characters 29-59:
8 36 | type extra_unparsing_rules = Ppextend.extra_unparsing_rules
9 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
10 Error: Unbound type constructor Ppextend.extra_unparsing_rules
The local opam file I am using is (https://github.com/coq/platform/blob/main/opam/opam-coq-archive/extra-dev/packages/coq-serapi/coq-serapi.dev/opam) - it is reasonably close to the opam file in ther serapi repo, but allows dev coq.
@Michael Soegtrop Isn't the issue that you do not specify a branch name in https://github.com/coq/platform/blob/main/opam/opam-coq-archive/extra-dev/packages/coq-serapi/coq-serapi.dev/opam? If you use the default branch it will not work, since it is v8.16
.
For Coq dev, you should use https://github.com/ejgallego/coq-serapi/tree/main
right, the default branch is usually changed for every major Coq release
but even if repo pinning for main branch works, a coq-serapi.dev
package would be welcome in the opam repo extra-dev
.
Yup, that's due to the wrong branch. We had a branch for each Coq version as we didn't support Coq master, now that has changed, so it could make sense for us to setup the default branch to main
Last updated: Jun 09 2023 at 04:01 UTC