Replace ssrlia with mczify

added 1 commit

84bb46e5 - Replace ssrlia with mczify

Compare with previous version

added 1 commit

0fb1a3ca - Replace ssrlia with mczify

Compare with previous version

added 1 commit

55a79a38 - Replace ssrlia with mczify

Compare with previous version

Hi Pierre, thanks for the MR.

I have a question about CI. Is it generally a good idea to re-install packages on each CI build, or would it be better to create custom Docker images that include this dependency? Of course, creating the images and keeping them up-to-date is tedious and creates some maintenance hassle.

added 1 commit

ebf848f1 - CI: don't remove dependencies of coq-mathcomp-zify

Compare with previous version

BTW, @Mbodin I don't know how to update the esy package, could you have a look? (you can take inspiration on the coq-prosa.opam file changes) Side question: how does esy compare to Nix which seems more commonly used in the Coq community?

added 1 commit

11a96574 - update documentation to mention the mczify dependency

Compare with previous version

added 13 commits

11a96574...be40b98b - 10 commits from branch master
e5305cf7 - Replace ssrlia with mczify
7e65d6c8 - CI: don't remove dependencies of coq-mathcomp-zify
e8d0c3c9 - update documentation to mention the mczify dependency

Compare with previous version

Pierre, I see that you left the old ssrlia only in classic/analysis/uni/basic/tdma_wcrt_analysis.v, while replacing it everywhere else. Is there a reason for that or just something that I should take care of?