Rocq (Coq) are now widely used in various fields, including software verification and mathematical proofs. When proving a new theorem, users often need to search and apply proven theorems to assist the current proof process. However, the current search command is limited to the environment of imported modules and cannot search for theorems outside of this scope. Furthermore, tool developers and researchers may want to obtain detailed information about theorems, such as theorem's names, statements, and dependencies. But there are currently no user-friendly and efficient tools available for extracting comprehensive information from Rocq projects. We introduce a Rocq theorem extraction and analysis tool, TheoremExtr, which is capable of analyzing theorem composition and extracting theorems, dependencies, and definitions from both parsing phase and runtime. We extracted 71,795 theorems and their dependencies from 32 open-source projects from the Rocq community. In addition, we extracted 27,481 definitions and their types among these projects. We also developed a website that supports cross-project similarity search for theorems and definitions. The tool is available at https://github.com/Rw1nd/TheoremExtr, and the search website is available at https://lemmasearch.com.

翻译：Rocq（Coq）目前已广泛应用于软件验证与数学证明等多个领域。在证明新定理时，用户通常需要搜索并应用已证定理来辅助当前证明过程。然而，当前搜索命令仅限于已导入模块的环境，无法搜索该范围之外的定理。此外，工具开发者和研究人员可能希望获取定理的详细信息，例如定理名称、陈述及其依赖关系。但目前尚缺乏用户友好且高效的工具来从Rocq项目中提取完整信息。我们提出了一种Rocq定理提取与分析工具TheoremExtr，它能够分析定理构成，并从解析阶段和运行时阶段提取定理、依赖关系及定义。我们从Rocq社区的32个开源项目中提取了71,795个定理及其依赖关系。此外，我们还从这些项目中提取了27,481个定义及其类型。我们还开发了一个支持跨项目定理与定义相似性搜索的网站。该工具可于https://github.com/Rw1nd/TheoremExtr获取，搜索网站可于https://lemmasearch.com访问。