Bug#1019239: transition: coq (41 packages involved)
On 2022-09-10 13:24:56 +0200, Sebastian Ramacher wrote:
> On 2022-09-10 12:59:12 +0200, Julien Puydt wrote:
> > Hi
> >
> > Le sam. 10 sept. 2022 à 12:12, Sebastian Ramacher <sramacher@debian.org> a
> > écrit :
> >
> > >
> > > The rebuild are now done, but there are some autopkgtest regressions.
> > > They all look like
> > >
> > > https://ci.debian.net/data/autopkgtest/testing/amd64/c/coq-iris/25883605/log.gz
> > > .
> > > Are there some packages that lack the proper dependencies?
> > >
> >
> >
> > The fact that the coq-iris package isn't a version 4.0.0-1+b1 isn't normal
> > - I guess my wanna-build script was buggy and didn't give every needed nmu
> > line. (I rewrote it since... the new one should be better...)
> >
> > I'll need to check the failing packages - probably monday.
>
> coq-iris also currently FTBFS:
>
>
> COQC iris/prelude/options.v
> COQC iris/prelude/prelude.v
> File "./iris/prelude/prelude.v", line 2, characters 0-34:
> Error: File /usr/lib/ocaml/coq/user-contrib/stdpp/prelude.vo has bad version
> number 81500 (expected 81600). It is corrupted or was compiled with another
> version of Coq.
>
> make[4]: *** [Makefile.coq:793: iris/prelude/prelude.vo] Error 1
> make[3]: *** [Makefile.coq:409: all] Error 2
>
> I guess there are more packages coq-* that are currently installable
> although that shouldn't be. Otherwise they would turn up red on the
> transition tracker.
coq-stdpp can be installed with any coq version. That will need fixing.
Cheers
--
Sebastian Ramacher
Reply to: