Bug#1023763: mathcomp-algebra-tactics: autopkgtest regression: interface mismatch on Elpi__BuiltinFindlib

[Paul Gevers]

Source: mathcomp-algebra-tactics
Version: 1.0.0-7
Severity: serious
User: debian...@lists.debian.org
Usertags: regression

Dear maintainer(s),



                       pass            fail
mathcomp-algebra-tactics from testing    1.0.0-7
versioned deps [0]     from testing    from unstable
all others             from testing    from testing

I copied some of the output at the bottom of this report.



More information about this bug and the reason for filing it can be found on
https://wiki.debian.org/ContinuousIntegration/RegressionEmailInformation

Paul


[1] https://qa.debian.org/excuses.php?package=mathcomp-algebra-tactics

https://ci.debian.net/data/autopkgtest/testing/amd64/m/mathcomp-algebra-tactics/28060854/log.gz

Error:
Dynlink error: interface mismatch on Elpi__BuiltinFindlib paths:
/usr/lib/ocaml/coq/../coq-core/plugins/ltac
/usr/lib/ocaml/coq/../coq-core/plugins/ssreflect
/usr/lib/ocaml/coq/../coq-core/plugins/ring
/usr/lib/ocaml/coq/../coq-core/plugins/ssrmatching
/usr/lib/ocaml/coq/../coq-core/plugins/nsatz
/usr/lib/ocaml/coq/../coq-core/plugins/ltac2
/usr/lib/ocaml/coq/../coq-core/plugins/number_string_notation
/usr/lib/ocaml/coq/../coq-core/plugins/cc
/usr/lib/ocaml/coq/../coq-core/plugins/firstorder
/usr/lib/ocaml/coq/../coq-core/plugins/tauto
/usr/lib/ocaml/coq/../coq-core/plugins/rtauto
/usr/lib/ocaml/coq/../coq-core/plugins/extraction
/usr/lib/ocaml/coq/../coq-core/plugins/zify
/usr/lib/ocaml/coq/../coq-core/plugins/funind
/usr/lib/ocaml/coq/../coq-core/plugins/micromega
/usr/lib/ocaml/coq/../coq-core/plugins/derive
/usr/lib/ocaml/coq/../coq-core/plugins/btauto
/usr/lib/ocaml/coq/../coq-core/..
/usr/lib/ocaml/coq/user-contrib/Ltac2
/usr/lib/ocaml/coq/user-contrib/elpi
/usr/lib/ocaml/coq/user-contrib/elpi/apps
/usr/lib/ocaml/coq/user-contrib/elpi/apps/eltac
/usr/lib/ocaml/coq/user-contrib/elpi/apps/derive
/usr/lib/ocaml/coq/user-contrib/mathcomp
/usr/lib/ocaml/coq/user-contrib/mathcomp/algebra
/usr/lib/ocaml/coq/user-contrib/mathcomp/ssreflect
/usr/lib/ocaml/coq/user-contrib/mathcomp/algebra_tactics
/usr/lib/ocaml/coq/user-contrib/mathcomp/zify
/usr/lib/ocaml/coq/user-contrib/mathcomp/fingroup
/usr/local/lib/ocaml/4.13.1
/usr/lib/ocaml
/usr/lib/ocaml/METAS


autopkgtest [19:17:45]: test command1

With a recent upload of mathcomp-algebra-tactics the autopkgtest of mathcomp-algebra-tactics fails in testing when that autopkgtest is run with the binary packages of mathcomp-algebra-tactics from unstable. It passes when run with only packages from testing. In tabular form: Currently this regression is blocking the migration to testing [1]. Can you please investigate the situation and fix it? [0] You can see what packages were added from the second line of the log file quoted below. The migration software adds source package from unstable to the list if they are needed to install packages from mathcomp-algebra-tactics/1.0.0-7. I.e. due to versioned dependencies or breaks/conflicts.

OpenPGP_signature
Description: OpenPGP digital signature