Stream: math-comp users

Topic: mathcomp 2.0 status?


view this post on Zulip Jason Gross (Aug 22 2023 at 19:16):

It seems that coq-mathcomp-analysis and coq-mathcomp-algebra-tactics don't build with mathcomp 2. Is this in the works? (Should I be looking to downgrade to 1.17, or can I get away with helping with the port or waiting a bit?)

view this post on Zulip Karl Palmskog (Aug 22 2023 at 19:41):

long discussion about roadblocks for algebra-tactics in 2.0 here: https://github.com/math-comp/algebra-tactics/pull/71

I guess Kazuhiko and/or Pierre will figure it out eventually.

view this post on Zulip Karl Palmskog (Aug 22 2023 at 19:42):

here is the analysis PR: https://github.com/math-comp/analysis/pull/951

view this post on Zulip Karl Palmskog (Aug 22 2023 at 19:45):

you may want to ping in the actual PRs about status and need for help (but recall this is French vacation time), compare this topic

view this post on Zulip Jason Gross (Aug 22 2023 at 22:46):

Thanks! It looks like both of those branches build, and I can in fact just use those branches for my development for the time being

view this post on Zulip Karl Palmskog (Sep 21 2023 at 12:15):

@Kazuhiko Sakaguchi @Pierre Roux is there any light in the tunnel for the Algebra Tactics HB PR? Unless I'm mistaken, this is the last high impact utility package that hasn't seen a MC 2.0 release (maybe Analysis could be viewed as a utility too, but it's more a world of its own). Would be happy to help with packaging if anything like that is needed.

view this post on Zulip Kazuhiko Sakaguchi (Sep 28 2023 at 13:28):

Done: https://github.com/math-comp/algebra-tactics/releases/tag/1.2.0

view this post on Zulip Kazuhiko Sakaguchi (Sep 28 2023 at 13:29):

I will open a PR to the OPAM repo.

view this post on Zulip Julien Puydt (Sep 29 2023 at 08:21):

In Debian, the status of Coq 8.18 and MC 2 is that the following package are still problematic: coq-math-classes, coq-mtac2, coq-corn, coq-quickchick, coq-extructures, mathcomp-analysis and mathcomp-abel (notice that coq-stdpp only compiles with a dirty patch, so it might count here too).

view this post on Zulip Karl Palmskog (Sep 29 2023 at 08:22):

I asked about stdpp release here, seemingly not going to happen for a while

view this post on Zulip Karl Palmskog (Sep 29 2023 at 08:23):

@Julien Puydt https://github.com/coq/opam/blob/master/released/packages/coq-extructures/coq-extructures.0.4.0/opam#L18

view this post on Zulip Karl Palmskog (Sep 29 2023 at 08:26):

we know analysis for MC2 is in pipeline. The Abel PR for MC2 looks ready, so I do a gentle ping of @Cyril Cohen and @Pierre Roux to see what their plans are. The other packages are not related to MC2.

view this post on Zulip Julien Puydt (Sep 29 2023 at 08:29):

Yes, I'm doing a dual Coq+MC transition so not everything is on-topic indeed

view this post on Zulip Julien Puydt (Sep 29 2023 at 08:30):

Ah, extructures 0.4.0 is indeed good.

view this post on Zulip Pierre Roux (Sep 29 2023 at 08:33):

view this post on Zulip Julien Puydt (Sep 29 2023 at 08:40):

Well, quickchick doesn't compile here - but it might be more due to Coq 8.18 than MC 2...

view this post on Zulip Pierre Roux (Sep 29 2023 at 08:48):

It's a plugin so indeed you likely need some kind of 8.18 tag/branch. Maybe @Yishuai Li would know what are upstream plans?

view this post on Zulip Karl Palmskog (Sep 29 2023 at 08:54):

https://github.com/coq/opam/pull/2742 to adjust bound for quickchick 2.0.0

view this post on Zulip Karl Palmskog (Sep 29 2023 at 09:00):

@Julien Puydt do you package algebra tactics for MC2? If not, this is a very useful package to add: https://github.com/coq/opam/blob/master/released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.2.0/opam#L29

view this post on Zulip Julien Puydt (Sep 29 2023 at 09:01):

Here is what is currently in Debian - and I'm trying to update the whole to C8.18+MC2

view this post on Zulip Enrico Tassi (Sep 29 2023 at 09:02):

Note that there has been a release of the platform, there is a .csv for 8.17 as well

view this post on Zulip Kazuhiko Sakaguchi (Sep 29 2023 at 09:03):

Sorry but I found a bug in Algebra Tactics 1.2.0 and have to do a minor release today.

view this post on Zulip Karl Palmskog (Sep 29 2023 at 09:03):

as I have argued elsewhere, the default MC environment (for any "serious" work) should consist at least of

view this post on Zulip Karl Palmskog (Sep 29 2023 at 09:09):

then one can branch off into (arguably) more domain-specific stuff like classic, analysis, real-closed, reglang, graph-theory, multinomials, CoqEAL,...

view this post on Zulip Kazuhiko Sakaguchi (Sep 29 2023 at 10:00):

To be honest, maintaining Algebra Tactics (particularly porting it to MC2) is a lot of work. Please don't expect it to be always compatible with the latest version of Coq, MathComp, etc.

view this post on Zulip Karl Palmskog (Sep 29 2023 at 10:05):

I think most people will be happy to live with the baseline of a release for the Platform, for the version of MC that is in that Platform (this should give several months from Coq/MC releases to adapt)

view this post on Zulip Kazuhiko Sakaguchi (Sep 29 2023 at 10:10):

Well, but we finished porting Algebra Tactics to MC2 more than 4 months after the release of MC2.

view this post on Zulip Kazuhiko Sakaguchi (Sep 29 2023 at 10:11):

(Then I still discover a bug because of my silly mistake.)

view this post on Zulip Karl Palmskog (Sep 29 2023 at 10:17):

but probably the future will see less radical stuff from now on in the MC universe, right?

view this post on Zulip Karl Palmskog (Sep 29 2023 at 10:20):

there wasn't any selection of MC version for the next Platform yet. But it looks now like all but possibly 1-3 packages related to MC2 are in place, so I'd personally favor MC2 for 8.18 Platform, maybe with a special separate MC1 collection

view this post on Zulip Kazuhiko Sakaguchi (Sep 29 2023 at 11:48):

Karl Palmskog said:

but probably the future will see less radical stuff from now on in the MC universe, right?

I hope so. However, for example, inserting a new structure in the middle of the hierarchy can significantly break Algebra Tactics because we have to work on a lower level.


Last updated: Jul 15 2024 at 21:02 UTC