FYI, we observed the following failure with a PR on infotheo where the CI fails because of a mathcomp-analysis error due to hb https://github.com/affeldt-aist/infotheo/pull/16 @Jacques Garrigue
NB: I am sharing the information before having taken time to look at it carefully, I'll report asap
Hum, we don't have MCA in our CI so we did not notice. It is a name collision
Yes, it looks like a name collision. I will take a closer look now.
Here are mathcomp-analysis CI outputs from this morning: https://github.com/math-comp/analysis/pull/294, https://github.com/math-comp/analysis/pull/224
The problem is in mathcomp analysis
we redefine measurableT
In HB 1.1.0 we export operations from mixins in the top module instead of a submodule
hence the error
Last updated: May 28 2023 at 18:29 UTC