Dear Coq users and developers,
We are happy to announce the initial release of Roosterize, a tool for suggesting lemma names in Coq verification projects.
Roosterize learns and suggests lemma names using neural networks that take serialized Coq lemma statements and elaborated terms as input. The technique is described in a research paper published in the proceedings of IJCAR 2020, where it was evaluated on a large dataset of Coq code from the Mathematical Components family of projects, with promising results.
The initial release supports Coq 8.10.2 and is based on using machine-readable representations of Coq code provided by SerAPI. See the README for detailed instructions on installing Roosterize and its dependencies, such as the machine learning framework PyTorch.
Roosterize is released under the MIT license, so please don’t hesitate to report issues and contribute on GitHub.
Karl and all contributors to the project