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: Apr 21 2024 at 01:02 UTC