search

imdea-software / fcsl-pcm

Partial Commutative Monoids
Apache License 2.0
25 stars 12 forks source link

WIP Port to MC2 #43

Closed proux01 closed 1 month ago

proux01 commented 1 month ago

Mathcomp 2 has been released more than a year ago and this is the last thing not yet proted in Coq's CI. Here is a large part of the port but I don't have time to complete it myself. Could you please have a look (I can help with the Hierarchy-Builder details).

aleksnanevski commented 1 month ago

I have been working on a port myself (of this, and other stuff of mine). Should all be done by the end of the summer. Not sure if it makes sense to merge this now as I'm quite close to finishing.

proux01 commented 1 month ago

No, this doesn't entirely compile so definitely not mergeable.

aleksnanevski commented 1 month ago

Is it then OK for you guys to wait on me a bit longer?

proux01 commented 1 month ago

Sure, end of summer is definitely fine, and feel free to ask if you encounter any difficulty.

aleksnanevski commented 1 month ago

Great, thanks! No real difficulties really. It has taken long time because I decided to completely change all the code (not just to get a port to mathcomp2, but also to change the organization of the math underneath). In the meantime, I should say, I have grown to quite like HB.