affeldt-aist

> @hoheinzollern I have updated PR #516 so that we should be able to rebase and only keep the `Section cvg_random_variable`. This might be still worth doing it, though after...

I don't get the CI failures, it works on my computer. What about yours?

I guess that's because we do not see the indices but I can't reproduce on my machine (Coq 8.16.1, MathComp 1.16.0, analysis 0.6.1, infotheo 0.5.1)

Oh! That is likely to be of interest to HB developers indeed.

@gares Note that the CI was happy with `master` until recently (last commit https://github.com/affeldt-aist/monae/commit/9695399f61848133b25ec2827a12f4c70c5c34bb) but now the CI fails with the same commit: https://github.com/affeldt-aist/monae/pull/123 It looks like something has changed...

We realized that there is another issue that affects MathComp-Analysis: coq-elpi 1.17 + HB 1.6.0 -> analysis fails in functions.v coq-elpi 1.17 + HB 1.5.0 -> analysis compiles coq-elpi 1.18...

However, that still leaves the issue with monae: coq-elpi 1.18 + HB 1.6.0 + infotheo 0.5.2 -> monae 0.5 fails with the Type monae 0.5 compiles

I plan to put monae in nixpkgs so that it can go to the nixconfig of HB but this will take some time

@gares @t6s Just an update about Monae and Hierarchy-builder. So in the end I didn't complete the bisect between HB 1.5.0 and 1.6.0 I promised. I did try for a...

iiuc, we need to keep the current `order_morphism` under a different name?