search

math-comp / hierarchy-builder

High level commands to declare a hierarchy based on packed classes
MIT License
95 stars 20 forks source link

fix #386 #423

Open gares opened 2 months ago

gares commented 2 months ago

fix #386

proux01 commented 2 months ago

@gares could you try https://github.com/proux01/hierarchy-builder/commit/bc02eab0d5f2be71f46855f97a7d292bb7afdf47

gares commented 2 months ago

done, but I think there was a "race"

proux01 commented 2 months ago

Indeed, my bad, I rebased the branch, relaunching should now work.

gares commented 2 months ago

Now it works, but the OOthm fails (as in Coq's CI for your PR). So it is good enough to bench mathcomp

proux01 commented 2 months ago

Bench is a bit disappointing, the last commit use primproj for class->mixin builders actually makes things a bit slower:

CohenCyril commented 2 months ago

I suspect a proper use of universe polymorphism will have a better impact.