phanerozoic/Omnia

Omnia数据集是一个跨领域的Coq声明集合，来自Omnia形式化语料库及多个库项目。该数据集统一了所有备份源仓库中带有.v文件的声明，涵盖了法律、医学、工程、历史、数学、网络、文化系统等多个领域。每个条目都是从机器检查的源仓库中提取的Coq声明。数据集包含71,021个声明，来自119个源仓库，715个.v文件，20个子库。声明类型包括定义、引理、定理等，且27%的声明带有文档字符串。数据集采用确定性Python提取器生成，确保每次生成的行顺序一致。

Omnia is a cross-domain collection of Coq declarations from the Omnia formalization corpus, plus several library projects. It unifies declarations from every backed-up source repository with .v files, spanning domains such as law, medicine, engineering, history, mathematics, networking, and cultural systems. Each entry is a Coq declaration extracted from a machine-checked source repository. The dataset contains 71,021 declarations from 119 source repos, 715 .v files, and 20 sub-libraries. Declaration types include Definition, Lemma, Theorem, etc., with 27% having docstrings. The dataset is produced by a deterministic Python extractor, ensuring consistent row order across regenerations.