compcert
Datasets
All datasets matching “compcert”Coq-CompCert
Coq-CompCert
A structured dataset of formalizations from CompCert, the verified C compiler.
Source
Repository: https://github.com/AbsInt/CompCert
Commit: 0ef26dad76446c803da02d7368eb4f9d074c1401
Files: 222
License: other
Schema
Column
Type
Description
statement
string
Declaration signature/claim with the leading keyword removed (verbatim slice); the full declaration minus its proof
proof
string
Verbatim proof/body, empty if the… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Coq-CompCert.CompCert-eval
CompCert Proof-Engineering Eval
Proof-synthesis challenges mined from the git history of
AbsInt/CompCert, the formally verified C
compiler. Each challenge is a real proof-engineering edit that a human made in a
single commit: we take the repository state before the commit (the
challenge) and treat the state after the commit (the solution) as
ground truth. The model's job is to reconstruct the proof/spec work the human
did.
⚠️ License notice. CompCert is distributed under the… See the full description on the dataset page: https://huggingface.co/datasets/for-all-dev/CompCert-eval.compcert