replace fsdist_convA by its generic version convA0

[t6s]

proba_monad_model.v uses another form of convA that is also specific to fsdist: fsdist_convA.
This PR replaces it by its generic version convA0.
I intend to remove fsdist_convA from infotheo as its only use seems to be here.

[affeldt-aist]

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

[t6s]

It compiles on my machine with coq-8.17.0, mathcomp-1.17.0, analysis-0.6.3, infotheo-0.5.2.

[t6s]

Type <= Type being a missing universe constraint looks very weird

[affeldt-aist]

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)

[t6s]

let me temporarily Set Printing All just before the erroneous Equations line

[t6s]

  Error: - Error: Missing universe constraint declared for inductive type:
  - Type@{max(Set,mathcomp.ssreflect.tuple.380,MonadAlt.axioms_.u0,monae.fail_lib.5368)} <= 
  - Type@{max(Set,MonadAlt.axioms_.u0,monae.fail_lib.5368)}
  - Type@{max(Set,mathcomp.ssreflect.tuple.380,MonadAlt.axioms_.u0,monae.fail_lib.5368)} <= 
  - Type@{max(Set,MonadAlt.axioms_.u0,monae.fail_lib.5368)}

HB is broken? My local HB is 1.4.0 and the CI is using 1.6.0.

[affeldt-aist]

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

[t6s]

Confirmed locally that it fails with coq-8.17.1, elpi-1.18.0, and HB-1.6.0.
Trying to check further with coq-8.18, elpi-1.19, HB-1.6.0.

elpi versions may matter; I have just noticed elpi-1.17.1 + HB-1.6.0 fails to compile mathcomp-classical-0.6.4 while elpi-1.18 + HB-1.6.0 succeeds.

[t6s]

The same error with coq-8.18.0 + elpi-1.19.0 + HB-1.6.0.
(btw, infotheo compiled without a problem with these)

[gares]

I'm a bit lost with versions.

Confirmed locally that it fails with coq-8.17.1, elpi-1.18.0, and HB-1.6.0. Trying to check further with coq-8.18, elpi-1.19, HB-1.6.0.

elpi versions may matter; I have just noticed elpi-1.17.1 + HB-1.6.0 fails to compile mathcomp-classical-0.6.4 while elpi-1.18 + HB-1.6.0 succeeds.

I believe Coq-Elpi 1.18 and 1.19 are very similar w.r.t. universes. The message above is unclear to me, is 1.18 working or not? Can you help me reproduce the problem?

It seems to me that Equations does not add a constraint, and that maybe the constraint was previously added by Coq-Elpi, possibly hiding the bug (and maybe the constraint is not needed per se in the term synthesized by Coq-Elpi/HB).

One way to tell would be to give by hand the term generated by Equations, and see if the bug is still there. If I'm right, one could alternatively add by hand the missing constraint between u0 and the universe of tuples (by adding a dummy definition before the call to equations, a definition that forces that constraint) to work around the bug.

[t6s]

HB 1.4.0 succeeds to compile monae master and HB-1.6.0 fails, regardless of the versions of elpi used.

HB 1.6.0 + elpi 1.18 succeeds to compile mathcomp-analysis 0.6.4 and HB 1.6.0 + elpi 1.17.1 fails.

I'll try your suggestion to feed a term directly.

[t6s]

Oh I have just noticed coq-elpi and elpi are different packages. The versions so far I wrote about elpi was of coq-elpi.

[gares]

That is fine, elpi should not impact at all this.

[gares]

If I'm right, then adding/removing a call to the type checker (in coq-elpi or HB) is sufficient to trigger/avoid a bug in equations.

If you have all version around, then checking if/when the constraint between the u0 (or Set) and tuple universe is added can help clarify. I suspect that in the versions where things work, it is added by some HB command.

[affeldt-aist]

@gares Note that the CI was happy with master until recently
(last commit 9695399)
but now the CI fails with the same commit:
#123
It looks like something has changed below our feet

[affeldt-aist]

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 + HB 1.5.0 -> analysis compiles
coq-elpi 1.18 + HB 1.6.0 -> analysis compiles

[affeldt-aist]

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 <= Type error we have been discussing
coq-elpi 1.18 + HB 1.5.0 + infotheo 0.5.2 -> monae 0.5 compiles

[affeldt-aist]

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

[affeldt-aist]

@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 while but I was getting lost because of the too-many, long re-compilations.
Also, we haven't yet investigated workarounds to get compilation through with 1.6.0
but this is rather by lack of time, it is still on the table.
We finally chose to fix Hierarchy-builder to its version 1.5.0 which is the one for which everything compiles for us.
(By the way, the github page of HB advertises version 1.5.0 as the latest, this is maybe an error.)

Let us add that we are really happy with HB: we managed to use it to add another, fairly complicated monad
to our hierarchy, and build two models for it, using monad transformers themselves built with HB.
When defining monad morphisms, we realized that HB does not yet support carriers of type forall A, f A -> g A
but yet we could find our way using factories so the model seems quite robust.

[affeldt-aist]

@t6s I have rebased this branch on master.
Can you confirm that the results is fine?
If yes, I'll merge after the CI has passed.

[t6s]

LGTM

[affeldt-aist]

Then I release.