Proposal to move Velisarios to Coq-community

[palmskog]

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]

@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]

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]

@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]

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

[Zimmi48]

@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]

@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.