Karl Palmskog (Apr 17 2023 at 10:58): Karl Palmskog (Apr 17 2023 at 10:58):any update on packaging/releases for the Platform? Background: https://github.com/coq/platform/issues/177
Bas Spitters (Apr 18 2023 at 06:57):We're waiting for the jasmin proofs to be available in opam/coq platform. I understand they are there in coq CI. I believe this is a man power issue on the jasmin side.
Sebastian Ertel (Mar 07 2024 at 09:16):Dear SSProvers,
I would like to help getting SSProve on the mathcomp Nix-based CI.
But in order to do so, I need that packaging information.
Could we potentially agree on a version 0.1.0 for the current state and a version 0.2.0 for the port to mathcomp 2.1.0?
The PR for the mathcomp 2.1.0 port reports a successful CI and probably only needs a review to be merged.
Once this is done, I would go ahead and add SSProve to the mathcomp CI. No need to wait for Jasmin support for these two versions.
Bas Spitters (Mar 08 2024 at 10:22):Sounds good to me!
@Philipp G. Haselwarter or @Théo Winterhalter will likely agree...
The jasmin port is waiting for HB. @Pierre Roux and @Enrico Tassi are looking into this.
https://github.com/jasmin-lang/jasmin/pull/560
Théo Winterhalter (Mar 08 2024 at 10:22):Of course no objection!
Philipp G. Haselwarter (Mar 08 2024 at 11:19)::thumbs_up:
Sebastian Ertel (May 02 2024 at 14:02):Dear SSProvers,
I created 2 PRs.
The first PR makes SSProve available on nixpkgs.
The second PR adds SSProve to the CI.
The first PR needs a maintainer that takes care of the SSProve entry in nixpkgs.
Does anybody of you would like to do so?
If not, would it be ok for you if I do that?
Théo Winterhalter (May 02 2024 at 14:03):Hi. Thanks for doing that. I'm not a nix user so I don't think I could, but I have no objection for you to do it if you so wish. :smile:
Sebastian Ertel (May 03 2024 at 08:25):Hi @Théo Winterhalter ,
you're welcome. Then I'm happy to maintain the nixpkgs entry for SSProve.
Karl Palmskog (May 03 2024 at 08:49):please consider submitting releases as opam packages to the Coq opam archive, since very few Coq users use Nix: https://github.com/coq/opam
Sebastian Ertel (May 06 2024 at 11:40):I'm not an opam user and would not want to take this duty.
Sebastian Ertel (May 06 2024 at 11:42):In any case, both PRs have been merged. That is, SSProve is now part of the nix-based CI.
I'm also preparing a PR for SSProve to give the local SSProve the regression that is also running as part of the nix-based CI.
Bas Spitters (May 06 2024 at 17:59):Thanks @Sebastian Ertel !
Sebastian Ertel (May 06 2024 at 18:44):You're welcome.
Karl Palmskog (Jul 13 2024 at 12:53):are there any plans for a new release now that https://github.com/SSProve/ssprove/pull/41 has been merged? The problem is that everyone who installs the coq-ssprove.0.2.0 package (whether using Nix or opam) will put a bunch of files under [coq-lib]/user-contribs/Crypt, etc., which in the future might conflict with other files (there was already a near clash with Fiat-Crypto that is using Crypto)
Bas Spitters (Jul 13 2024 at 13:00):Yes, I think @Eske Nielsen is planning on doing that.
Karl Palmskog (Jul 13 2024 at 13:03):for the record, you can simplify this:
-Q theories/Mon SSProve.Mon
-Q theories/Relational SSProve.Relational
-Q theories/Crypt SSProve.Crypt
into the equivalent:
-Q theories SSProve
and if you have unique .v file names inside theories, you can tell your users to write:
From SSProve Require Import <Module>.
... regardless of the directory <Module>.v resides in under theories. This is what MathComp does and enables moving files between directories without breaking clients.
Sebastian Ertel (Aug 12 2024 at 06:26):Sebastian Ertel said:
In any case, both PRs have been merged. That is, SSProve is now part of the nix-based CI.
I'm also preparing a PR for SSProve to give the local SSProve the regression that is also running as part of the nix-based CI.
There is now a PR on this.
Last updated: Oct 13 2024 at 01:02 UTC