Stream: Coq devs & plugin devs

Topic: SerApi: how to make an opam based dev build?


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Nov 04 2022 at 16:01):

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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Nov 04 2022 at 16:02):

For Coq dev, you should use https://github.com/ejgallego/coq-serapi/tree/main

view this post on Zulip Karl Palmskog (Nov 04 2022 at 16:08):

right, the default branch is usually changed for every major Coq release

view this post on Zulip 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.

view this post on Zulip 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: Feb 05 2023 at 19:29 UTC