  Naming conventions are an important concern in large verification projects
using proof assistants, such as Coq. In particular, lemma names are used by
proof engineers to effectively understand and modify Coq code. However,
providing accurate and informative lemma names is a complex task, which is
currently often carried out manually. Even when lemma naming is automated using
rule-based tools, generated names may fail to adhere to important conventions
not specified explicitly. We demonstrate a toolchain, dubbed Roosterize, which
automatically suggests lemma names in Coq projects. Roosterize leverages a
neural network model trained on existing Coq code, thus avoiding manual
specification of naming conventions. To allow proof engineers to conveniently
access suggestions from Roosterize during Coq project development, we
integrated the toolchain into the popular Visual Studio Code editor. Our
evaluation shows that Roosterize substantially outperforms strong baselines for
suggesting lemma names and is useful in practice. The demo video for Roosterize
can be viewed at: https://youtu.be/HZ5ac7Q14rc.
