Michael Soegtrop (Nov 04 2022 at 13:01): Michael Soegtrop (Nov 04 2022 at 13:01):@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.
Emilio Jesús Gallego Arias (Nov 04 2022 at 15:08):@Michael Soegtrop indeed it seems to be building fine in Coq master, where can we see the build failure log?
Michael Soegtrop (Nov 04 2022 at 15:59):@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.
Théo Zimmermann (Nov 04 2022 at 16:01):@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.
Théo Zimmermann (Nov 04 2022 at 16:02):For Coq dev, you should use https://github.com/ejgallego/coq-serapi/tree/main
Karl Palmskog (Nov 04 2022 at 16:08):right, the default branch is usually changed for every major Coq release
Karl Palmskog (Nov 04 2022 at 16:09):but even if repo pinning for main branch works, a coq-serapi.dev package would be welcome in the opam repo extra-dev.
Emilio Jesús Gallego Arias (Nov 04 2022 at 19:59):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