WasmCert-Coq
WasmCert-Coq copied to clipboard
WasmCert
Moving to Coq-community?
@raoxiaojia and others, with @jeanpichon we are discussing how to host the work on certicoq-wasm with @womeier for posterity. We're considering Coq community as, personally, I have very good experiences with it in the corn and math-classes libraries. https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md#proposing-a-new-package
It is a great way to prevent mature work from bit-rotting and it helps both visibility and availability for the community. Would this also be relevant for wasmcert-Coq?
This is for sure a good idea for the long term, especially if at some point in the future I'd no longer be able to maintain this library -- that being said, this likely doesn't require too much maintenance anyway if being pinned to Wasm 1.0 at least.
I've taken a look at their community standard and thought I'd like to go for it after finishing and merging in my current batch of new work, which also implemented a lot of refactorings to maintain a sensible structure (at which point I'll probably release a version under a new git tag).
@spitters I described one blocker in #29. Your best bet might be to ask the author of Parseque to relicense to weak copyleft or more permissive.
Since we have resolved #29, feel free to open an issue about moving the project when you are ready.
I'd like to emphasize that a move to Coq-community does not necessarily mean letting go of the project - the maintainers can be the same as before, only with more options w.r.t. automation and future co-maintenance.
Since we have resolved #29, feel free to open an issue about moving the project when you are ready.
I'd like to emphasize that a move to Coq-community does not necessarily mean letting go of the project - the maintainers can be the same as before, only with more options w.r.t. automation and future co-maintenance.
Great! Also, many thanks for your help in dealing with licenses in the opam package as well! I should probably also merge that commit back here. Another note to myself to look at trimming the dependencies -- I'll open a PR to remind myself of this.
As previously mentioned, I'll probably open a PR as soon as I've finished and merged some of my current work. The only reason for that is to merge in some of my refactoring which performed some slight changes to a few base definitions: I've made some decisions which are almost surely better in the long term (more genuine representation of the Wasm spec, and saving code at the same time) -- but I just wanted to make certain.
I've read the community manifesto and reckon that I'll have to care a lot about backward compatibility after submitting anything there, so I thought it makes sense to submit a version without an impending refactor.
I've read the community manifesto and reckon that I'll have to care a lot about backward compatibility after submitting anything there, so I thought it makes sense to submit a version without an impending refactor.
While we encourage backwards compatibility when it makes sense, we generally advise maintainers to ensure compatibility with the latest released version of Coq (currently 8.18.0). Thanks to Coq's version compatibility policy, it's always possible to be compatible with two subsequent major versions - so both 8.18.0 and 8.17.1 right now. Going beyond this is in my view considered icing on the cake.
This doesn't mean work to make the project more maintainable across Coq versions is wasteful, and you may want to consider proposing adding the project to Coq's CI or the Coq Platform in the future, which entails more stringent requirements.
I've read the community manifesto and reckon that I'll have to care a lot about backward compatibility after submitting anything there, so I thought it makes sense to submit a version without an impending refactor.
While we encourage backwards compatibility when it makes sense, we generally advise maintainers to ensure compatibility with the latest released version of Coq (currently 8.18.0). Thanks to Coq's version compatibility policy, it's always possible to be compatible with two subsequent major versions - so both 8.18.0 and 8.17.1 right now. Going beyond this is in my view considered icing on the cake.
This doesn't mean work to make the project more maintainable across Coq versions is wasteful, and you may want to consider proposing adding the project to Coq's CI or the Coq Platform in the future, which entails more stringent requirements.
I might have misinterpreted the wording for backward compatibility then -- I understood it more as a backwards compatibility with the previous versions of the codebase itself, instead of with the previous Coq versions.
Note that name/scope of some of the numeric functions are being updated in Coq 8.17 -- while the old ones are still supported (marked as deprecates), I presume they would have been removed in 8.18. Does @womeier still depend on the 8.16 build as mentioned previously? If not, then I can upgrade those to 8.18 as well.
You might be talking about the following sentence from the Coq-community manifesto:
These changes must, nonetheless, always be done with consideration for compatibility as soon as the package is a library, plugin or tool that has users.
The context here is that some projects are widely used libraries. If a maintainer changes a lot in a library, then users will have to do a lot of work to adapt to those changes. We simply encourage maintainers to consider intra-library-version compatibility if they have users. To my knowledge, WasmCert-Coq is currently only used by @womeier and @spitters (for CertiCoq), so considering their requirements would be enough at the moment.
I've read the community manifesto and reckon that I'll have to care a lot about backward compatibility after submitting anything there, so I thought it makes sense to submit a version without an impending refactor.
While we encourage backwards compatibility when it makes sense, we generally advise maintainers to ensure compatibility with the latest released version of Coq (currently 8.18.0). Thanks to Coq's version compatibility policy, it's always possible to be compatible with two subsequent major versions - so both 8.18.0 and 8.17.1 right now. Going beyond this is in my view considered icing on the cake. This doesn't mean work to make the project more maintainable across Coq versions is wasteful, and you may want to consider proposing adding the project to Coq's CI or the Coq Platform in the future, which entails more stringent requirements.
I might have misinterpreted the wording for backward compatibility then -- I understood it more as a backwards compatibility with the previous versions of the codebase itself, instead of with the previous Coq versions.
Note that name/scope of some of the numeric functions are being updated in Coq 8.17 -- while the old ones are still supported (marked as deprecates), I presume they would have been removed in 8.18. Does @womeier still depend on the 8.16 build as mentioned previously? If not, then I can upgrade those to 8.18 as well.
No, I just updated to 8.17 this week. Thanks for keeping 8.16 around for some more time!
@womeier do you still need 8.16 ?
No, I'm on 8.17 now and don't need 8.16 anymore. Thanks for keeping it around some more time @raoxiaojia.
@raoxiaojia with https://github.com/WasmCert/WasmCert-Coq/pull/31 merged, what are your plans going forward, would moving to coq-community be advantageous?
@raoxiaojia with #31 merged, what are your plans going forward, would moving to coq-community be advantageous?
It surely is the plan! I haven't really been working on anything much recently though, as I was just back to London after travelling home for ~4 weeks.
I saw your CertiCoq-Wasm talk in the schedule at CoqPL -- it would be great to meet any of you attending physically!
Yes, I'll be there. Let's try and meet. The abstract is here: https://www.cl.cam.ac.uk/~jp622/certicoq-wasm.pdf
@raoxiaojia it was nice to meet in London. What do you think about this one? (One or more of: Platform, Coq CI, coq-community, ... )
By keeping the Coq devs involved, then can help us to keep this working when newer versions of Coq come out.
@raoxiaojia it was nice to meet in London. What do you think about this one? (One or more of: Platform, Coq CI, coq-community, ... )
By keeping the Coq devs involved, then can help us to keep this working when newer versions of Coq come out.
I'll think harder on this after I finish the current various update. Submitting to Coq CI seems to be easy enough which doesn't add much extra downstream obligations, and makes sense when I'm still actively around so I can be the point of contact. Will consider others more seriously when I can be sure that there's no further large refactoring..