improve HB.instance

[gares]

• toposort using gref specific data structures
• fast fail for sub-classes of a class that failed to be inferred

[CohenCyril]

The real bench is mca, I just added it, and I'm running it on my computer this afternoon (MCA takes about 20min if I recall correctly)

[proux01]

@CohenCyril rocq-community/coq-nix-toolbox#224 merged, could you please update the toolbox and rerun CI here

[proux01]

CI green, this looks good to be (squashed and) merged

[gares]

I still don't get why XS and elements {make-set XS} make any difference for ssrnum, but I guess I'll have to live with that.

There was a hack in ssrnum, maybe @CohenCyril recalls it? I don't think it should impact here though.

[proux01]

The failure was about SemiGroup and Monoids, didn't felt like related to the hack (but maybe remotely who knows).

[proux01]

FTR

• mathcomp
  • before: 15:21, 1708708 kb
  • after: 13:36, 1681224 kb (-11%, -2%)
• analysis
  • before: 16:29, 1926688 kb
  • after: 13:56, 1808196 kb (-15%, -6%)

[gares]

We could also try with the version of toposort by @Tragicus but we need elpi 1.19.2 for an efficient coq.gref.set.fold