Stream: math-comp users

Topic: should we expect mc2.0 any time soon?


view this post on Zulip walker (Jan 18 2023 at 15:01):

I am mostly interested in HB integration for the basic canonical structures in mc, so I wounder if that is something that may be released in the next few weeks or if there is a current road blocker.

view this post on Zulip Pierre Roux (Jan 18 2023 at 15:15):

There is already an alpha release https://github.com/math-comp/math-comp/releases/tag/mathcomp-2.0%2Balpha1 if you want to try it out. It's mostly finished (with lot of reverse dependencies already ported, c.f. overlays in the PR https://github.com/math-comp/math-comp/pull/733) but it still lacks proper documentation. So final release might rather be a matter of a few months than a few weeks (but that's just a wild guess).

view this post on Zulip Ricardo (Jan 19 2023 at 04:50):

Will finmap be integrated into mathcomp 2.0?

view this post on Zulip Pierre Roux (Jan 19 2023 at 07:40):

There will be a compatible version.

view this post on Zulip Bas Spitters (Jan 19 2023 at 09:51):

@Pierre Roux Could you say more about the plans with finmap?
In SSProve we are depending on extructures. I know there are plans of merging them.
Should we migrate to finmap at some point?

view this post on Zulip Karl Palmskog (Jan 19 2023 at 10:04):

I thought the general plan with MC 2.0 was that everything stays the same in terms of packages, but some packages that are in MathComp's CI get help to provide releases compatible with coq-mathcomp-ssreflect.2.0 and friends. So the ecosystem is largely unchanged, although some people might not bother to be compatible with 2.0 anytime soon.

view this post on Zulip Bas Spitters (Jan 19 2023 at 10:39):

Is extructures in the CI?

view this post on Zulip Pierre Roux (Jan 19 2023 at 12:39):

You can see the state of the CI there: https://github.com/math-comp/math-comp/pull/733
Extructures depends on deriving which is the only thing not ported yet in the CI because it uses polymorphic universes which (at least until recently, this may have changed) are not supported by Hierarchy Builder.


Last updated: Jul 25 2024 at 15:02 UTC