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 <sramac...@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
