Bas Spitters (Jul 14 2022 at 12:08): Bas Spitters (Jul 14 2022 at 12:08):Given the discussion here about Word libraries in Coq. Would it make sense to add MC/jasmin Word to the platform?
Both jasmin and SSProve depend on it. Any better ways to avoid duplication?
Karl Palmskog (Jul 14 2022 at 12:36):@Bas Spitters you can always propose adding Jasmin's word library to the Platform using an issue like this one.
As with many things Coq, the pressure to "canonicalize" things is quite low. But since you already have SSProve in the pipeline to join the Platform, the word library is already a dependency there and adding it would be less controversial when SSProve+Jasmin-word are added together.
Karl Palmskog (Jul 14 2022 at 12:36):still, it will need approval+coordination with Jasmin devs
Karl Palmskog (Jul 14 2022 at 12:39):I did some investigations of popularity like GitHub stars, etc., and then bbv seemed a bit more popular. But popularity is not always the main concern for the Platform
Bas Spitters (Jul 15 2022 at 14:13):Jasmin word uses the MC style, for better or for worse.
I've raised the issue with the jasmin devs. So far, little enthusiasm for the platform, it seems...
Karl Palmskog (Jul 15 2022 at 14:18):perhaps we can ping in @Vincent Laporte on this side for possible comment. The basic requirement for being added to the Platform is essentially that the project will be maintained going forward and have a Git tag or tarball for every major Coq version. Platform/opam maintainers can help out with the rest, such as adding opam packages.
Karl Palmskog (Jul 15 2022 at 14:23):since Jasmin is seemingly already well maintained, a tag for its dependency https://github.com/jasmin-lang/coqword now and then may be reasonable?
Vincent Laporte (Jul 18 2022 at 15:31):Adding the mathcomp-word library to the Coq Platform sounds like a good idea, indeed. Let me know if I can help.
Karl Palmskog (Jul 18 2022 at 15:33):@Vincent Laporte great, so we can open an issue in the Platform repo about it and ping people in? I think the main maintainers are you and Pierre-Yves?
Vincent Laporte (Jul 18 2022 at 15:34):That’s right.
Karl Palmskog (Jul 18 2022 at 15:45):https://github.com/coq/platform/issues/271
Karl Palmskog (Jul 19 2022 at 15:38):@Bas Spitters now you should be able to get that SSProve opam package out: https://github.com/coq/opam-coq-archive/blob/master/released/packages/coq-mathcomp-word/coq-mathcomp-word.1.1/opam
Bas Spitters (Jul 19 2022 at 19:12):We're currently working on integrating jasmin, so we'd need a package for that too. @Vincent Laporte Since there has been a release adding it to platform makes sense, doesn't it?
Karl Palmskog (Jul 19 2022 at 19:13):it might be a better idea to separate the "library" part of SSProve from any compilation part, that may have more dependencies
Karl Palmskog (Jul 19 2022 at 19:13):at least I was under the impression that Jasmin consumers did not typically use the Coq formalization
Vincent Laporte (Jul 19 2022 at 19:40):What part of Jasmin would you like to see in the Coq Platform? Who will use it and how?
Karl Palmskog (Jul 19 2022 at 19:48):Bas is saying SSProve will soon use Jasmin in some way: https://github.com/SSProve/ssprove
... but perhaps he can clarify the workflow there (Coq-level integration or not?)
Bas Spitters (Jul 21 2022 at 10:57):@Vincent Laporte we are working on using SSProve to reason about jasmin programs (and hacspec programs), somewhat in the same way as easycrypt is currently used to reason about jasmin programs. Details and, more motivation, to come.
Karl Palmskog (Jul 21 2022 at 11:44):in the interest of timeliness of Platform inclusion, I'd still advise adding the non-Jasmin-related parts of SSProve to the Platform, and then figuring out Jasmin stuff later
Last updated: Apr 19 2024 at 10:02 UTC