Reynald Affeldt (Apr 01 2021 at 02:36): Reynald Affeldt (Apr 01 2021 at 02:36):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
Reynald Affeldt (Apr 01 2021 at 02:40):NB: I am sharing the information before having taken time to look at it carefully, I'll report asap
Enrico Tassi (Apr 01 2021 at 06:58):Hum, we don't have MCA in our CI so we did not notice. It is a name collision
Reynald Affeldt (Apr 01 2021 at 07:08):Yes, it looks like a name collision. I will take a closer look now.
Reynald Affeldt (Apr 01 2021 at 07:12):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
Cyril Cohen (Apr 01 2021 at 07:30):The problem is in mathcomp analysis
Cyril Cohen (Apr 01 2021 at 07:30):we redefine measurableT
Cyril Cohen (Apr 01 2021 at 07:30):In HB 1.1.0 we export operations from mixins in the top module instead of a submodule
Cyril Cohen (Apr 01 2021 at 07:31):hence the error
Cyril Cohen (Apr 01 2021 at 07:38):Last updated: May 28 2023 at 18:29 UTC