Bug#1023712: why3 breaks frama-c (autopkgtest): missing versioned Breaks?

[Ralf Treinen <treinen@fdn.fr>]

Hi Paul,

On Wed, Dec 21, 2022 at 09:16:32PM +0100, Paul Gevers wrote:
> Control: reassign -1 frama-c
> 
> Dear maintainers,
> 
> On Tue, 8 Nov 2022 21:53:18 +0100 Paul Gevers <elbrus@debian.org> wrote:
> > [kernel] User Error: cannot load plug-in 'frama-c-wp': cannot load module
> >    Details: implementation mismatch on Why3
> > [kernel] User Error: Deferred error message was emitted during
> > execution. See above messages for more information.
> > [kernel] Frama-C aborted: invalid user input.
> > autopkgtest [20:18:19]: test eva
> 
> I'm now seeing the above error message in the frama-c test in testing, so it
> seems that the issue is rather that the autopkgtest of frama-c doesn't
> properly declare it's *versioned* test dependency on why3? Should the
> Recommends be versioned? (Not sure if that actually works as intended, but
> apparently the tested plug-in only works correctly with the right version of
> why3).

Sorry for not replying earlier, the last weeks have been very busy at
work.

The problem is that for some reason the package build of frama-c does
not pick up the versioned dependency on libwhy3-ocaml-dev (this should
be done by dh_ocaml). I'm looking into this now.

Cheers -Ralf.