Stream: math-comp analysis

Topic: Classical sets in mathcomp 2


view this post on Zulip Florent Hivert (Nov 22 2023 at 10:07):

Hi there. I'm currently learning hierarchy builder ! This is a tremendous improvement ! Congrats ! As an exercise I'm trying to update what I wrote on formal power series. The problem is that I need to use classical reasoning. I'm importing boolp and classical_sets. Opam says that those are not released for mathcomp 2. I guess it takes time to port the whole analysis. By chance, Is there a port somewhere of those two files I can use in the mean time ?

view this post on Zulip Kazuhiko Sakaguchi (Nov 22 2023 at 10:08):

@Florent Hivert I think what you need can be found here: https://github.com/math-comp/analysis/pull/951

view this post on Zulip Pierre Roux (Nov 22 2023 at 10:17):

Indeed there is a perfectly working branch of Analysis with mathcomp2 (linked above) that we keep up to date with Analysis master but no release yet. We hope the release to happen in the coming months (hopefully January).

view this post on Zulip Florent Hivert (Nov 22 2023 at 10:54):

I understand that there are two parts : classical reasoning and analysis (two opam files). Would it make sense to release the first one even if the second is not ready ?

view this post on Zulip Pierre Roux (Nov 22 2023 at 11:58):

Could be, let's ask @Reynald Affeldt

view this post on Zulip Karl Palmskog (Nov 22 2023 at 11:59):

since it's a monorepo, releasing one would implicitly entail releasing the other (same archive)

view this post on Zulip Karl Palmskog (Nov 22 2023 at 12:00):

with that said a "beta release" of Analysis for MC2 would probably be useful for porting projects (I have a few that use Analysis and can't be ported to MC2 yet since I want to test in CI)

view this post on Zulip Pierre Roux (Nov 22 2023 at 12:00):

We could still publish only a single opam file but that would indeed be pretty strange.

view this post on Zulip Karl Palmskog (Nov 22 2023 at 12:04):

you could for example use the opam feature for betas: avoid-version

view this post on Zulip Florent Hivert (Nov 22 2023 at 14:18):

@Kazuhiko Sakaguchi Explained me in a private communication that after cloning the Git repo, I can make a opam install ./coq-mathcomp-classical.opam This completely fits my need (porting an old project). Of course I'll need to wait for the official MCA release before releasing my own project. Thanks for all the answers.

view this post on Zulip Reynald Affeldt (Nov 22 2023 at 15:03):

Thank you very much for sharing! We put this information on the wiki: https://github.com/math-comp/analysis/wiki#new-compatibility-of-mathcomp-analysis-with-mathcomp-2


Last updated: Jun 22 2024 at 15:01 UTC