Stream: math-comp users

Topic: Mathcomp 2.0 vs 1.18


view this post on Zulip Congyan (Cruise) Song (Nov 28 2023 at 15:12):

Hi, my group are interested to port our project (quite large) developed in MC 1.17 into newer MC, preferably 2.0. But since the analysis are currently missing for 2.0, we are hesitant about whether we should wait for 2.0 's development or precede with porting to 1.18 first? Basically, we are no sure of how difficult it would be to later port 1.18 into 2.0 (whenever its compatible analysis releases), since 2.0 is our ultimate goal.

Any input and advice are welcome! Thank you.

view this post on Zulip Reynald Affeldt (Nov 28 2023 at 22:37):

The difficulty for porting to mathcomp 2 depends on your projet, there are some insights in https://hal.science/hal-04225130v1/document

view this post on Zulip Reynald Affeldt (Nov 28 2023 at 22:38):

If you have not been creating your own hierarchies, it should be almost painless

view this post on Zulip Reynald Affeldt (Nov 28 2023 at 22:40):

As for mathcomp 1.18 it grows out of backports from mathcomp 2, so it can only get you closer

view this post on Zulip Bas Spitters (Nov 29 2023 at 10:09):

@Cruise Song is your project in the MC CI? It's often a good way to help others help you...

view this post on Zulip Cruise Song (Nov 29 2023 at 22:05):

Bas Spitters said:

Cruise Song is your project in the MC CI? It's often a good way to help others help you...

Thanks for your advice, but I am not very familiar with CI, is there any suggestion for how to put our project in the MC CI?

view this post on Zulip Pierre Roux (Nov 30 2023 at 16:06):

The first step for addition in CI is creating a Nix package (see e.g. https://github.com/NixOS/nixpkgs/pull/231077 )

view this post on Zulip Cyril Cohen (Nov 30 2023 at 16:23):

See also https://nixos.org/manual/nixpkgs/stable/#sec-language-coq


Last updated: Jul 15 2024 at 19:01 UTC