Extructures

[spitters]

arthuraa/extructures#4

In the future one would probably like to encourage a merge of the three alternatives to this package stated at the bottom of:
https://github.com/arthuraa/extructures

[palmskog]

@spitters I don't think it makes any sense to include a library (extructures) in the platform that significantly overlaps in functionality and purpose with an already included library (mathcomp-finmap). If you want them to be merged, this is best discussed with the respective maintainers.

[Zimmi48]

I don't think it makes any sense to include a library (extructures) in the platform that significantly overlaps in functionality and purpose with an already included library

It depends on how much this library is used. The platform is not the place to pick sides between two depended-upon libraries with overlapping purpose. For instance, both coq-ext-lib and stdpp will be eventually included.

[spitters]

We're using extructures in a project. There's a plan to merge finmap with extructures, but this has not happened yet.

…

On Fri, Jan 15, 2021 at 8:58 PM Théo Zimmermann ***@***.***> wrote: I don't think it makes any sense to include a library (extructures) in the platform that significantly overlaps in functionality and purpose with an already included library It depends on how much this library is used. The platform is not the place to pick sides between two depended-upon libraries with overlapping purpose. For instance, both coq-ext-lib and stdpp will be eventually included. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#61 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AABTNTXPSYZJIUG2K7Q362LS2CM7FANCNFSM4V7COMWQ> .

[palmskog]

I don't think coq-ext-lib vs. stdpp is comparable. Both of those have unique definitions/results that the other does not have, and both are general-purpose libraries. However, mathcomp-finmap and exstructures are special-purpose and I believe they overlap so closely (notations, definitions, results) it will likely lead to increased community fracturing to include both in the platform.

[spitters]

I summon @arthuraa and @CohenCyril.

[arthuraa]

I have discussed this matter with @CohenCyril a while ago. My understanding is that there is a big ongoing restructuring of MathComp's finmap, and that it would be better to wait until it is finished before we start incorporating features from extructures there.

@spitters Are there any specific features that you would like to see incorporated into finmap? Here is my understanding of the main differences between the two libraries:

1. Finmap relies on the choice interface to pick a canonical ordering for the keys of a map. In extructures, the keys are sorted according to a total order attached to the keys. This means that extructures maps can be extracted directly (though the performance would be mediocre, to be honest), and that we get some definitional equalities for some functions that can be used for small-scale reflection (e.g. x \in fset0 reduces to false). The downside is that extructures needs a more complex class hierarchy.

2. Extructures includes permutations over an arbitrary ordered type, which is absent from finmap. Finmap includes multisets, which are absent from extructures.

[CohenCyril]

Additionally, math-comp/finmap objects piggyback on ssreflect ones: any A : {fset T} is a fintype which val projection lands in T, and any finmap f : {fmap T1 -> T2} is a {ffun domf f -> T2} by coercion and conversely by canonical inference, and most operations can be optionally locked to prevent divergences in term comparison.

[spitters]

@arthuraa I see I did not answer this. Our work is now available.
https://github.com/SSProve

@TheoWinterhalter you can probably answer this quicker than I can. What do we need precisely?
arthuraa/extructures#9

[MSoegtropIMC]

Since I am working on a new pick (and there will soon be the pick for 8.14) may I ask for a - possibly preliminary - conclusion?

[spitters]

@CohenCyril @arthuraa any update on the restructuring of MC finmap?

[MSoegtropIMC]

I postponed this package inclusion to the next release which will likely happen in November (for Coq 8.14)

[spitters]

Any updates on this? We'd also like to get SSProve into platform.

[MSoegtropIMC]

The Coq Platform is expected to provide a stable "API". I am not sure how this can be guaranteed if extructures is expected to merge with finmap some time in the future. The API will most likely change considerably then. But in my opinion it would be OK to add it to the extended level - with a corresponding note - as intermediate solution.

Also the package has version 0.3, which is another soft indication that the extended level would be appropriate.

Still I would need an explicit agreement from @arthuraa.

@arthuraa : packages are included into the Coq Platform only if the author(s) explicitly agree to this and confirm that they will maintain the package in the foreseeable future according to the spirit of the Coq Platform charter. For the extended level this is a bit more relaxed - but you still need to confirm here that you want the inclusion in Coq Platform and agree to the charter.

[Zimmi48]

Indeed, it seems that the extended level is a good fit.

[MSoegtropIMC]

@arthuraa : I am currently doing the picks for 2022.03 and I could still take this in, but I would need a statement from you that you want this and are planning to maintain it according to the Coq Platform charter

[arthuraa]

@MSoegtropIMC Yes, including extructures in the extended level would be a good idea. The package has been pretty stable over the last releases, and I plan to continuing maintaining it in the foreseable future. In the long run, it would be desirable to consolidate the package with finmap, but while this does not happen I think it makes sense to have both packages.