Re: Wrong package version is installed
Hi Paul,
thanks a lot for your quick and helpful response!
On 9/22/20 10:03 PM, Paul Gevers wrote:
> On 22-09-2020 14:29, Fabian Wolff wrote:
>> This is a problem because the cvc4 update caused a regression for why3
>> in unstable, but now the z3 package also can't migrate to testing
>> because there's an apparent regression for why3, which is actually due
>> to the wrong version of cvc4 being used in the CI test.
>
> Not the wrong version. There is only one version to pick, but it only
> lives in unstable *and* you have skip-not-installable enabled.
Ah, of course, because the old cvc4 version wasn't built on arm64. I
had completely forgotten about that, sorry! I just saw that the
correct version was installed in the amd64 log, but not in the arm64
one, and couldn't understand why (I would have expected an error in
this case, but thanks for your explanation for why this happens
below).
>> How should I proceed here?
>
> Contact the Release Team would be appropriate, but as I am member of
> that too, so let's not bother. I was about to add a hint, however, your
> z3 test definition says that only z3 < 4.8.7 is good enough (which is
> only available in stable). So I suggest you make the test work with the
> z3 in unstable, or drop the test (for now):
>
> Broken autopkgtest-satdep:arm64 Depends on z3:arm64 < none | 4.8.9-1 @un
> uH > (< 4.8.7)
> Removing autopkgtest-satdep:arm64 because I can't find z3:arm64
>
> Once this new why3 migrates, the "problem" is gone.
I see. I will contact the maintainer of why3 to discuss this. From my
understanding of the situation, just disabling the z3 test won't work,
because the cvc4 one would still fail, but I think we can fix both at
the same time.
>> And is this a bug in debci/autopkgtest/...?
>
> It's an artifact of using skip-not-installable. In a pure testing
> environment, the test with cvc4 is skipped because cvc4 isn't
> installable, but with testing enabled, cvc4 is installable (albeit from
> unstable), but the whole tool chain britney -> debci -> autopkgtest ->
> apt -> dpkg isn't smart enough (with acceptable settings) to actually
> convey that. What we would want to have is to tell apt to only install
> packages from unstable if explicitly mentioned and use testing for all
> the rest, but for that we need a resolver that's non-default. So,
> consider this a wontfix bug in the infrastructure.
That's what confused me about the situation. I *expected* the tests
for why3 to fail with the cvc4 version from unstable, and so seeing
the tests triggered by z3 fail because of cvc4 from unstable made me
think that there must be a problem with the infrastructure.
So, thank you very much for your explanation of the situation, and
sorry again for bothering you with this non-bug!
Best regards,
Fabian
Reply to: