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?)

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.

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

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

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

@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.

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

I will open a PR to the OPAM repo.

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).

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

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

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.

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

Ah, extructures 0.4.0 is indeed good.

- Quickchik: compiles perfectly fine on MC2, it's just a silly (reverse) dependency thing with CI target http-something and different versions of menhir that sticks it on MC1 in Coq CI
- mathcomp-abel port is ready for a while https://github.com/math-comp/Abel/pull/75 but I guess this got forgotten (ping @Cyril Cohen)
- mathcomp-analysis has a maintained
`hierarchy-builder`

branch compiling on MC2, merge is currently expected by the end of the year or early next year - math-classes, corn and mtac2 don't seem related to MC2

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

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?

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

@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

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

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

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

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

- all the basic ones:
`ssreflect`

,`fingroup`

,`algebra`

,`solvable`

,`field`

,`character`

(and now`hierarchy-builder`

/`elpi`

in MC2) - utility:
`mathcomp-zify`

,`algebra-tactics`

,`finmap`

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

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.

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)

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

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

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

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

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