Congyan (Cruise) Song (Nov 28 2023 at 15:12): 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.
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
Reynald Affeldt (Nov 28 2023 at 22:38):If you have not been creating your own hierarchies, it should be almost painless
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
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...
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?
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 )
Cyril Cohen (Nov 30 2023 at 16:23):See also https://nixos.org/manual/nixpkgs/stable/#sec-language-coq
Last updated: Oct 13 2024 at 01:02 UTC