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 ?
@Florent Hivert I think what you need can be found here: https://github.com/math-comp/analysis/pull/951
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).
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 ?
Could be, let's ask @Reynald Affeldt
since it's a monorepo, releasing one would implicitly entail releasing the other (same archive)
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)
We could still publish only a single opam file but that would indeed be pretty strange.
you could for example use the opam feature for betas: avoid-version
@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.
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: Oct 13 2024 at 01:02 UTC