Add MMaps to Coq Platform

[palmskog]

MMaps is a library that contains several implementations of finite maps over arbitrary ordered types using Coq functors. This is an updated version of Coq Stdlib's FMaps. It is meant to complement the MSet library in Stdlib. One noteworthy advantage over the legacy FMaps is that MMaps has a fast red-black tree based finite map.

MMaps is currently maintained in Coq-community by myself and @letouzey and just had its 1.0 release. I propose that MMaps is added to the Coq Platform, so as to let FMap users migrate to it.

[ybertot]

Justification of usage here is associated to the efficiency gain when migrating. I would suggest that this should be better advertised on the MMaps main page.

Also, the MMaps main page contains a caveat about unstable interfaces that might deter potential users from migrating. Is this caveat pragmatically important?

[palmskog]

@ybertot there are in my view two main arguments for people to migrate from FMaps or use this package from scratch:

• a modernized interface to maps aligned with MSets, that contains functionality not present in FSets, see here for an example
• a wider selection of modules that implement the map interface, among which are red-black trees that are expected to perform well and not require (unbounded) integers at runtime

The caveat about interface stability is to my knowledge a remnant from when the library was under heavy development by Pierre. I would say the core interface is stable (and we can change the README to reflect this), but there could be additional utility results added over time, such as what Andrew did here.

[ybertot]

I agree, I only suggest you should remove the remnant.

[palmskog]

OK, I will address this in the next few days.

[palmskog]

For the record, the README issue was addressed in https://github.com/coq-community/coq-mmaps/pull/15

[ybertot]

The inclusion of this contribution has been approved by the editorial board. The issue will not be closed until proper action has been taken.