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