search

coq-community / manifesto

Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.
Other
68 stars 6 forks source link

Proposal to move Velisarios to Coq-community #59

Open palmskog opened 5 years ago

palmskog commented 5 years ago

Move a project to coq-community

Project name: Velisarios

Initial author(s): Vincent Rahli, Ivana Vukotic, Marcus Völp, and Paulo Esteves-Verissimo

Current URL: https://github.com/vrahli/Velisarios

Kind: Coq library and extractable program

License: GPL-3.0-or-later

Description: Velisarios is a framework for verification of Byzantine fault-tolerant distributed systems, which contains an executable implementation of the PBFT algorithm.

Status: maintained (but current version on GitHub needs update for Coq 8.9)

New maintainers: Vincent Rahli (@vrahli) and Karl Palmskog (@palmskog)

PBFT is an important Coq case study. The main purpose of moving Velisarios to Coq-community (while keeping initial authors as maintainers) is to ease long-term maintenance via CI and other automation. In particular, Dune will be helpful for the executable PBFT implementation. I also suggest that Velisarios should join Coq's CI.

palmskog commented 5 years ago

@vrahli can you confirm here that everything looks good with the above, and that you're OK with moving the original repository to the Coq-community organization? Feel free to propose more maintainers from your team.

@Zimmi48 can you invite @vrahli to the organization so he gets full access?

Note that my main motivation as co-maintainer would be to ensure working builds for Coq 8.9 and beyond to enable proof engineering research on the project. I'm fine with any other further evolution of the project.

spitters commented 5 years ago

Interesting. Perhaps you can expand the readme a bit. Is there a connected paper? The coq-tools directory seems like material that perhaps should be moved to a more central place.

Zimmi48 commented 5 years ago

@spitters It seems like this is the corresponding paper: https://link.springer.com/chapter/10.1007/978-3-319-89884-1_22

@palmskog Sure I've invited @vrahli to the organization.

vrahli commented 5 years ago

Here's a copy of the paper: https://vrahli.github.io/articles/velisarios.pdf

Zimmi48 commented 5 years ago

@vrahli Since you have joined the organization, you should now be able to transfer your two repositories. Let me know if that's not the case or if you need help.

Zimmi48 commented 5 years ago

@vrahli Do you still intend to transfer this project and NuprlInCoq to coq-community? If yes, let me know if you need help with the transfer operation. If not, we should close this issue.