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.

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

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

Last updated: May 18 2024 at 08:40 UTC