Stream: Coq users

Topic: Initial release of Roosterize tool for Coq lemma generation

Karl Palmskog (Jun 05 2020 at 06:36):

We have released our machine learning based tool for lemma name generation in Coq 8.10: https://github.com/EngineeringSoftware/roosterize

While the underlying technique is project-agnostic, the initial release is bundled with a model trained on projects from Mathematical Components. Hence, it is mainly aimed at MathComp users, but we welcome feedback on future trained models. Our arXiv paper has more about the technique, and there will be a webinar-style presentation at IJCAR 2020 around early July.

Karl Palmskog (Jun 05 2020 at 06:40):

At this point, we would also be grateful for any feedback on installation / documentation and basic functionality of the tool, e.g., if it works as expected on Coq projects "in the wild".

Emilio Jesús Gallego Arias (Jun 05 2020 at 10:18):

Very cool! I have a few developments that try to follow math-comp's style pretty closely, I'll try the tool.

Last updated: Oct 08 2024 at 14:01 UTC