Sebastian Ertel (Aug 12 2024 at 06:37): Sebastian Ertel (Aug 12 2024 at 06:37):Dear @Lasse Letager Hansen and @Bas Spitters ,
Can you please comment on the status of the Jasmin integration in the SSProve repo?
I would like to use Hax with the SSProve backend but
ssprove_backend_lib branch in the Hax repo was not yet merged into the main andssprove_backend_lib branch seems to depend on the jasmin branch in SSProve repo (read here) which is also not up-to-date. Lasse Letager Hansen (Aug 21 2024 at 14:39):The ssprove_backend_lib depends very slightly on jasmin, as we are only using the Jasmin words. Most of the jasmin code has thus been (temporarily) removed from that branch. The jasmin branch has been waiting on jasmin to merge suuport for Mathcomp 2.0, which is now done. So we should be able to update the jasmin branch and possibly merge both the jasmin branch and the ssprove_backend_lib branch into main. However, I am not very experinced with jasmin, so I have not tried that hard on updating the jasmin branch.
Karl Palmskog (Aug 21 2024 at 14:53):do the Jasmin people have any opam packaging plans for their Coq side? Otherwise, it may not be possible to package coq-ssprove anymore if Jasmin is a hard dependency.
Bas Spitters (Aug 21 2024 at 15:04):It's here: https://github.com/jasmin-lang/coqword
Bas Spitters (Aug 21 2024 at 15:06):It's in the opam package index: https://coq.inria.fr/coq-package-index
@Lasse Letager Hansen I don't see it here: https://github.com/SSProve/ssprove/blob/main/ssprove.opam
but it may be dragged in by one of the other dependencies...
Karl Palmskog (Aug 21 2024 at 15:09):but coq-mathcomp-word has been available for MathComp 2 since about a year
Karl Palmskog (Aug 21 2024 at 15:10):MathComp 2 support in Jasmin proper was only merged in July, so I assume this is what was talked about: https://github.com/jasmin-lang/jasmin/commit/9abca78c125835871ab158057b5c4f1553f7a280
Lasse Letager Hansen (Aug 21 2024 at 15:14):The dependecy for what we are doing in Hax, is more or less just this file: https://github.com/SSProve/ssprove/blob/jasmin-coq.8.18.0/theories/Jasmin/word.v
However, for the SSProve jasmin branch we were waiting on: https://github.com/jasmin-lang/jasmin/pull/560
Last updated: Oct 13 2024 at 01:02 UTC