theostos/pile-of-rocq

---
configs:
- config_name: coq-actuary-sources
data_files:
- split: train
path: coq-actuary/sources.parquet
- config_name: coq-actuary-toc_nodes
data_files:
- split: train
path: coq-actuary/toc_nodes.parquet
- config_name: coq-actuary-proofs
data_files:
- split: train
path: coq-actuary/proofs.parquet
- config_name: coq-actuary-proof_steps
data_files:
- split: train
path: coq-actuary/proof_steps.parquet
- config_name: coq-actuary-step_deps
data_files:
- split: train
path: coq-actuary/step_deps.parquet
- config_name: coq-actuary-proof_axioms
data_files:
- split: train
path: coq-actuary/proof_axioms.parquet
- config_name: coq-actuary-env_toc
data_files:
- split: train
path: coq-actuary/env_toc.parquet
- config_name: coq-actuary-env_metadata
data_files:
- split: train
path: coq-actuary/env_metadata.parquet
- config_name: coq-atbr-sources
data_files:
- split: train
path: coq-atbr/sources.parquet
- config_name: coq-atbr-toc_nodes
data_files:
- split: train
path: coq-atbr/toc_nodes.parquet
- config_name: coq-atbr-proofs
data_files:
- split: train
path: coq-atbr/proofs.parquet
- config_name: coq-atbr-proof_steps
data_files:
- split: train
path: coq-atbr/proof_steps.parquet
- config_name: coq-atbr-step_deps
data_files:
- split: train
path: coq-atbr/step_deps.parquet
- config_name: coq-atbr-proof_axioms
data_files:
- split: train
path: coq-atbr/proof_axioms.parquet
- config_name: coq-atbr-env_toc
data_files:
- split: train
path: coq-atbr/env_toc.parquet
- config_name: coq-atbr-env_metadata
data_files:
- split: train
path: coq-atbr/env_metadata.parquet
- config_name: coq-color-sources
data_files:
- split: train
path: coq-color/sources.parquet
- config_name: coq-color-toc_nodes
data_files:
- split: train
path: coq-color/toc_nodes.parquet
- config_name: coq-color-proofs
data_files:
- split: train
path: coq-color/proofs.parquet
- config_name: coq-color-proof_steps
data_files:
- split: train
path: coq-color/proof_steps.parquet
- config_name: coq-color-step_deps
data_files:
- split: train
path: coq-color/step_deps.parquet
- config_name: coq-color-proof_axioms
data_files:
- split: train
path: coq-color/proof_axioms.parquet
- config_name: coq-color-env_toc
data_files:
- split: train
path: coq-color/env_toc.parquet
- config_name: coq-color-env_metadata
data_files:
- split: train
path: coq-color/env_metadata.parquet
- config_name: coq-compcert-sources
data_files:
- split: train
path: coq-compcert/sources.parquet
- config_name: coq-compcert-toc_nodes
data_files:
- split: train
path: coq-compcert/toc_nodes.parquet
- config_name: coq-compcert-proofs
data_files:
- split: train
path: coq-compcert/proofs.parquet
- config_name: coq-compcert-proof_steps
data_files:
- split: train
path: coq-compcert/proof_steps.parquet
- config_name: coq-compcert-step_deps
data_files:
- split: train
path: coq-compcert/step_deps.parquet
- config_name: coq-compcert-proof_axioms
data_files:
- split: train
path: coq-compcert/proof_axioms.parquet
- config_name: coq-compcert-env_toc
data_files:
- split: train
path: coq-compcert/env_toc.parquet
- config_name: coq-compcert-env_metadata
data_files:
- split: train
path: coq-compcert/env_metadata.parquet
- config_name: coq-coqeal-sources
data_files:
- split: train
path: coq-coqeal/sources.parquet
- config_name: coq-coqeal-toc_nodes
data_files:
- split: train
path: coq-coqeal/toc_nodes.parquet
- config_name: coq-coqeal-proofs
data_files:
- split: train
path: coq-coqeal/proofs.parquet
- config_name: coq-coqeal-proof_steps
data_files:
- split: train
path: coq-coqeal/proof_steps.parquet
- config_name: coq-coqeal-step_deps
data_files:
- split: train
path: coq-coqeal/step_deps.parquet
- config_name: coq-coqeal-proof_axioms
data_files:
- split: train
path: coq-coqeal/proof_axioms.parquet
- config_name: coq-coqeal-env_toc
data_files:
- split: train
path: coq-coqeal/env_toc.parquet
- config_name: coq-coqeal-env_metadata
data_files:
- split: train
path: coq-coqeal/env_metadata.parquet
- config_name: coq-coqprime-sources
data_files:
- split: train
path: coq-coqprime/sources.parquet
- config_name: coq-coqprime-toc_nodes
data_files:
- split: train
path: coq-coqprime/toc_nodes.parquet
- config_name: coq-coqprime-proofs
data_files:
- split: train
path: coq-coqprime/proofs.parquet
- config_name: coq-coqprime-proof_steps
data_files:
- split: train
path: coq-coqprime/proof_steps.parquet
- config_name: coq-coqprime-step_deps
data_files:
- split: train
path: coq-coqprime/step_deps.parquet
- config_name: coq-coqprime-proof_axioms
data_files:
- split: train
path: coq-coqprime/proof_axioms.parquet
- config_name: coq-coqprime-env_toc
data_files:
- split: train
path: coq-coqprime/env_toc.parquet
- config_name: coq-coqprime-env_metadata
data_files:
- split: train
path: coq-coqprime/env_metadata.parquet
- config_name: coq-coqtail-sources
data_files:
- split: train
path: coq-coqtail/sources.parquet
- config_name: coq-coqtail-toc_nodes
data_files:
- split: train
path: coq-coqtail/toc_nodes.parquet
- config_name: coq-coqtail-proofs
data_files:
- split: train
path: coq-coqtail/proofs.parquet
- config_name: coq-coqtail-proof_steps
data_files:
- split: train
path: coq-coqtail/proof_steps.parquet
- config_name: coq-coqtail-step_deps
data_files:
- split: train
path: coq-coqtail/step_deps.parquet
- config_name: coq-coqtail-proof_axioms
data_files:
- split: train
path: coq-coqtail/proof_axioms.parquet
- config_name: coq-coqtail-env_toc
data_files:
- split: train
path: coq-coqtail/env_toc.parquet
- config_name: coq-coqtail-env_metadata
data_files:
- split: train
path: coq-coqtail/env_metadata.parquet
- config_name: coq-coquelicot-sources
data_files:
- split: train
path: coq-coquelicot/sources.parquet
- config_name: coq-coquelicot-toc_nodes
data_files:
- split: train
path: coq-coquelicot/toc_nodes.parquet
- config_name: coq-coquelicot-proofs
data_files:
- split: train
path: coq-coquelicot/proofs.parquet
- config_name: coq-coquelicot-proof_steps
data_files:
- split: train
path: coq-coquelicot/proof_steps.parquet
- config_name: coq-coquelicot-step_deps
data_files:
- split: train
path: coq-coquelicot/step_deps.parquet
- config_name: coq-coquelicot-proof_axioms
data_files:
- split: train
path: coq-coquelicot/proof_axioms.parquet
- config_name: coq-coquelicot-env_toc
data_files:
- split: train
path: coq-coquelicot/env_toc.parquet
- config_name: coq-coquelicot-env_metadata
data_files:
- split: train
path: coq-coquelicot/env_metadata.parquet
- config_name: coq-corn-sources
data_files:
- split: train
path: coq-corn/sources.parquet
- config_name: coq-corn-toc_nodes
data_files:
- split: train
path: coq-corn/toc_nodes.parquet
- config_name: coq-corn-proofs
data_files:
- split: train
path: coq-corn/proofs.parquet
- config_name: coq-corn-proof_steps
data_files:
- split: train
path: coq-corn/proof_steps.parquet
- config_name: coq-corn-step_deps
data_files:
- split: train
path: coq-corn/step_deps.parquet
- config_name: coq-corn-proof_axioms
data_files:
- split: train
path: coq-corn/proof_axioms.parquet
- config_name: coq-corn-env_toc
data_files:
- split: train
path: coq-corn/env_toc.parquet
- config_name: coq-corn-env_metadata
data_files:
- split: train
path: coq-corn/env_metadata.parquet
- config_name: coq-ext-lib-sources
data_files:
- split: train
path: coq-ext-lib/sources.parquet
- config_name: coq-ext-lib-toc_nodes
data_files:
- split: train
path: coq-ext-lib/toc_nodes.parquet
- config_name: coq-ext-lib-proofs
data_files:
- split: train
path: coq-ext-lib/proofs.parquet
- config_name: coq-ext-lib-proof_steps
data_files:
- split: train
path: coq-ext-lib/proof_steps.parquet
- config_name: coq-ext-lib-step_deps
data_files:
- split: train
path: coq-ext-lib/step_deps.parquet
- config_name: coq-ext-lib-proof_axioms
data_files:
- split: train
path: coq-ext-lib/proof_axioms.parquet
- config_name: coq-ext-lib-env_toc
data_files:
- split: train
path: coq-ext-lib/env_toc.parquet
- config_name: coq-ext-lib-env_metadata
data_files:
- split: train
path: coq-ext-lib/env_metadata.parquet
- config_name: coq-extructures-sources
data_files:
- split: train
path: coq-extructures/sources.parquet
- config_name: coq-extructures-toc_nodes
data_files:
- split: train
path: coq-extructures/toc_nodes.parquet
- config_name: coq-extructures-proofs
data_files:
- split: train
path: coq-extructures/proofs.parquet
- config_name: coq-extructures-proof_steps
data_files:
- split: train
path: coq-extructures/proof_steps.parquet
- config_name: coq-extructures-step_deps
data_files:
- split: train
path: coq-extructures/step_deps.parquet
- config_name: coq-extructures-proof_axioms
data_files:
- split: train
path: coq-extructures/proof_axioms.parquet
- config_name: coq-extructures-env_toc
data_files:
- split: train
path: coq-extructures/env_toc.parquet
- config_name: coq-extructures-env_metadata
data_files:
- split: train
path: coq-extructures/env_metadata.parquet
- config_name: coq-fcsl-pcm-sources
data_files:
- split: train
path: coq-fcsl-pcm/sources.parquet
- config_name: coq-fcsl-pcm-toc_nodes
data_files:
- split: train
path: coq-fcsl-pcm/toc_nodes.parquet
- config_name: coq-fcsl-pcm-proofs
data_files:
- split: train
path: coq-fcsl-pcm/proofs.parquet
- config_name: coq-fcsl-pcm-proof_steps
data_files:
- split: train
path: coq-fcsl-pcm/proof_steps.parquet
- config_name: coq-fcsl-pcm-step_deps
data_files:
- split: train
path: coq-fcsl-pcm/step_deps.parquet
- config_name: coq-fcsl-pcm-proof_axioms
data_files:
- split: train
path: coq-fcsl-pcm/proof_axioms.parquet
- config_name: coq-fcsl-pcm-env_toc
data_files:
- split: train
path: coq-fcsl-pcm/env_toc.parquet
- config_name: coq-fcsl-pcm-env_metadata
data_files:
- split: train
path: coq-fcsl-pcm/env_metadata.parquet
- config_name: coq-flocq-sources
data_files:
- split: train
path: coq-flocq/sources.parquet
- config_name: coq-flocq-toc_nodes
data_files:
- split: train
path: coq-flocq/toc_nodes.parquet
- config_name: coq-flocq-proofs
data_files:
- split: train
path: coq-flocq/proofs.parquet
- config_name: coq-flocq-proof_steps
data_files:
- split: train
path: coq-flocq/proof_steps.parquet
- config_name: coq-flocq-step_deps
data_files:
- split: train
path: coq-flocq/step_deps.parquet
- config_name: coq-flocq-proof_axioms
data_files:
- split: train
path: coq-flocq/proof_axioms.parquet
- config_name: coq-flocq-env_toc
data_files:
- split: train
path: coq-flocq/env_toc.parquet
- config_name: coq-flocq-env_metadata
data_files:
- split: train
path: coq-flocq/env_metadata.parquet
- config_name: coq-fourcolor-sources
data_files:
- split: train
path: coq-fourcolor/sources.parquet
- config_name: coq-fourcolor-toc_nodes
data_files:
- split: train
path: coq-fourcolor/toc_nodes.parquet
- config_name: coq-fourcolor-proofs
data_files:
- split: train
path: coq-fourcolor/proofs.parquet
- config_name: coq-fourcolor-proof_steps
data_files:
- split: train
path: coq-fourcolor/proof_steps.parquet
- config_name: coq-fourcolor-step_deps
data_files:
- split: train
path: coq-fourcolor/step_deps.parquet
- config_name: coq-fourcolor-proof_axioms
data_files:
- split: train
path: coq-fourcolor/proof_axioms.parquet
- config_name: coq-fourcolor-env_toc
data_files:
- split: train
path: coq-fourcolor/env_toc.parquet
- config_name: coq-fourcolor-env_metadata
data_files:
- split: train
path: coq-fourcolor/env_metadata.parquet
- config_name: coq-geocoq-sources
data_files:
- split: train
path: coq-geocoq/sources.parquet
- config_name: coq-geocoq-toc_nodes
data_files:
- split: train
path: coq-geocoq/toc_nodes.parquet
- config_name: coq-geocoq-proofs
data_files:
- split: train
path: coq-geocoq/proofs.parquet
- config_name: coq-geocoq-proof_steps
data_files:
- split: train
path: coq-geocoq/proof_steps.parquet
- config_name: coq-geocoq-step_deps
data_files:
- split: train
path: coq-geocoq/step_deps.parquet
- config_name: coq-geocoq-proof_axioms
data_files:
- split: train
path: coq-geocoq/proof_axioms.parquet
- config_name: coq-geocoq-env_toc
data_files:
- split: train
path: coq-geocoq/env_toc.parquet
- config_name: coq-geocoq-env_metadata
data_files:
- split: train
path: coq-geocoq/env_metadata.parquet
- config_name: coq-graph-theory-sources
data_files:
- split: train
path: coq-graph-theory/sources.parquet
- config_name: coq-graph-theory-toc_nodes
data_files:
- split: train
path: coq-graph-theory/toc_nodes.parquet
- config_name: coq-graph-theory-proofs
data_files:
- split: train
path: coq-graph-theory/proofs.parquet
- config_name: coq-graph-theory-proof_steps
data_files:
- split: train
path: coq-graph-theory/proof_steps.parquet
- config_name: coq-graph-theory-step_deps
data_files:
- split: train
path: coq-graph-theory/step_deps.parquet
- config_name: coq-graph-theory-proof_axioms
data_files:
- split: train
path: coq-graph-theory/proof_axioms.parquet
- config_name: coq-graph-theory-env_toc
data_files:
- split: train
path: coq-graph-theory/env_toc.parquet
- config_name: coq-graph-theory-env_metadata
data_files:
- split: train
path: coq-graph-theory/env_metadata.parquet
- config_name: coq-high-school-geometry-sources
data_files:
- split: train
path: coq-high-school-geometry/sources.parquet
- config_name: coq-high-school-geometry-toc_nodes
data_files:
- split: train
path: coq-high-school-geometry/toc_nodes.parquet
- config_name: coq-high-school-geometry-proofs
data_files:
- split: train
path: coq-high-school-geometry/proofs.parquet
- config_name: coq-high-school-geometry-proof_steps
data_files:
- split: train
path: coq-high-school-geometry/proof_steps.parquet
- config_name: coq-high-school-geometry-step_deps
data_files:
- split: train
path: coq-high-school-geometry/step_deps.parquet
- config_name: coq-high-school-geometry-proof_axioms
data_files:
- split: train
path: coq-high-school-geometry/proof_axioms.parquet
- config_name: coq-high-school-geometry-env_toc
data_files:
- split: train
path: coq-high-school-geometry/env_toc.parquet
- config_name: coq-high-school-geometry-env_metadata
data_files:
- split: train
path: coq-high-school-geometry/env_metadata.parquet
- config_name: coq-hott-sources
data_files:
- split: train
path: coq-hott/sources.parquet
- config_name: coq-hott-toc_nodes
data_files:
- split: train
path: coq-hott/toc_nodes.parquet
- config_name: coq-hott-proofs
data_files:
- split: train
path: coq-hott/proofs.parquet
- config_name: coq-hott-proof_steps
data_files:
- split: train
path: coq-hott/proof_steps.parquet
- config_name: coq-hott-step_deps
data_files:
- split: train
path: coq-hott/step_deps.parquet
- config_name: coq-hott-proof_axioms
data_files:
- split: train
path: coq-hott/proof_axioms.parquet
- config_name: coq-hott-env_toc
data_files:
- split: train
path: coq-hott/env_toc.parquet
- config_name: coq-hott-env_metadata
data_files:
- split: train
path: coq-hott/env_metadata.parquet
- config_name: coq-infotheo-sources
data_files:
- split: train
path: coq-infotheo/sources.parquet
- config_name: coq-infotheo-toc_nodes
data_files:
- split: train
path: coq-infotheo/toc_nodes.parquet
- config_name: coq-infotheo-proofs
data_files:
- split: train
path: coq-infotheo/proofs.parquet
- config_name: coq-infotheo-proof_steps
data_files:
- split: train
path: coq-infotheo/proof_steps.parquet
- config_name: coq-infotheo-step_deps
data_files:
- split: train
path: coq-infotheo/step_deps.parquet
- config_name: coq-infotheo-proof_axioms
data_files:
- split: train
path: coq-infotheo/proof_axioms.parquet
- config_name: coq-infotheo-env_toc
data_files:
- split: train
path: coq-infotheo/env_toc.parquet
- config_name: coq-infotheo-env_metadata
data_files:
- split: train
path: coq-infotheo/env_metadata.parquet
- config_name: coq-iris-sources
data_files:
- split: train
path: coq-iris/sources.parquet
- config_name: coq-iris-toc_nodes
data_files:
- split: train
path: coq-iris/toc_nodes.parquet
- config_name: coq-iris-proofs
data_files:
- split: train
path: coq-iris/proofs.parquet
- config_name: coq-iris-proof_steps
data_files:
- split: train
path: coq-iris/proof_steps.parquet
- config_name: coq-iris-step_deps
data_files:
- split: train
path: coq-iris/step_deps.parquet
- config_name: coq-iris-proof_axioms
data_files:
- split: train
path: coq-iris/proof_axioms.parquet
- config_name: coq-iris-env_toc
data_files:
- split: train
path: coq-iris/env_toc.parquet
- config_name: coq-iris-env_metadata
data_files:
- split: train
path: coq-iris/env_metadata.parquet
- config_name: coq-itree-sources
data_files:
- split: train
path: coq-itree/sources.parquet
- config_name: coq-itree-toc_nodes
data_files:
- split: train
path: coq-itree/toc_nodes.parquet
- config_name: coq-itree-proofs
data_files:
- split: train
path: coq-itree/proofs.parquet
- config_name: coq-itree-proof_steps
data_files:
- split: train
path: coq-itree/proof_steps.parquet
- config_name: coq-itree-step_deps
data_files:
- split: train
path: coq-itree/step_deps.parquet
- config_name: coq-itree-proof_axioms
data_files:
- split: train
path: coq-itree/proof_axioms.parquet
- config_name: coq-itree-env_toc
data_files:
- split: train
path: coq-itree/env_toc.parquet
- config_name: coq-itree-env_metadata
data_files:
- split: train
path: coq-itree/env_metadata.parquet
- config_name: coq-karp-miller-sources
data_files:
- split: train
path: coq-karp-miller/sources.parquet
- config_name: coq-karp-miller-toc_nodes
data_files:
- split: train
path: coq-karp-miller/toc_nodes.parquet
- config_name: coq-karp-miller-proofs
data_files:
- split: train
path: coq-karp-miller/proofs.parquet
- config_name: coq-karp-miller-proof_steps
data_files:
- split: train
path: coq-karp-miller/proof_steps.parquet
- config_name: coq-karp-miller-step_deps
data_files:
- split: train
path: coq-karp-miller/step_deps.parquet
- config_name: coq-karp-miller-proof_axioms
data_files:
- split: train
path: coq-karp-miller/proof_axioms.parquet
- config_name: coq-karp-miller-env_toc
data_files:
- split: train
path: coq-karp-miller/env_toc.parquet
- config_name: coq-karp-miller-env_metadata
data_files:
- split: train
path: coq-karp-miller/env_metadata.parquet
- config_name: coq-kruskal-sources
data_files:
- split: train
path: coq-kruskal/sources.parquet
- config_name: coq-kruskal-toc_nodes
data_files:
- split: train
path: coq-kruskal/toc_nodes.parquet
- config_name: coq-kruskal-proofs
data_files:
- split: train
path: coq-kruskal/proofs.parquet
- config_name: coq-kruskal-proof_steps
data_files:
- split: train
path: coq-kruskal/proof_steps.parquet
- config_name: coq-kruskal-step_deps
data_files:
- split: train
path: coq-kruskal/step_deps.parquet
- config_name: coq-kruskal-proof_axioms
data_files:
- split: train
path: coq-kruskal/proof_axioms.parquet
- config_name: coq-kruskal-env_toc
data_files:
- split: train
path: coq-kruskal/env_toc.parquet
- config_name: coq-kruskal-env_metadata
data_files:
- split: train
path: coq-kruskal/env_metadata.parquet
- config_name: coq-library-fol-sources
data_files:
- split: train
path: coq-library-fol/sources.parquet
- config_name: coq-library-fol-toc_nodes
data_files:
- split: train
path: coq-library-fol/toc_nodes.parquet
- config_name: coq-library-fol-proofs
data_files:
- split: train
path: coq-library-fol/proofs.parquet
- config_name: coq-library-fol-proof_steps
data_files:
- split: train
path: coq-library-fol/proof_steps.parquet
- config_name: coq-library-fol-step_deps
data_files:
- split: train
path: coq-library-fol/step_deps.parquet
- config_name: coq-library-fol-proof_axioms
data_files:
- split: train
path: coq-library-fol/proof_axioms.parquet
- config_name: coq-library-fol-env_toc
data_files:
- split: train
path: coq-library-fol/env_toc.parquet
- config_name: coq-library-fol-env_metadata
data_files:
- split: train
path: coq-library-fol/env_metadata.parquet
- config_name: coq-libvalidsdp-sources
data_files:
- split: train
path: coq-libvalidsdp/sources.parquet
- config_name: coq-libvalidsdp-toc_nodes
data_files:
- split: train
path: coq-libvalidsdp/toc_nodes.parquet
- config_name: coq-libvalidsdp-proofs
data_files:
- split: train
path: coq-libvalidsdp/proofs.parquet
- config_name: coq-libvalidsdp-proof_steps
data_files:
- split: train
path: coq-libvalidsdp/proof_steps.parquet
- config_name: coq-libvalidsdp-step_deps
data_files:
- split: train
path: coq-libvalidsdp/step_deps.parquet
- config_name: coq-libvalidsdp-proof_axioms
data_files:
- split: train
path: coq-libvalidsdp/proof_axioms.parquet
- config_name: coq-libvalidsdp-env_toc
data_files:
- split: train
path: coq-libvalidsdp/env_toc.parquet
- config_name: coq-libvalidsdp-env_metadata
data_files:
- split: train
path: coq-libvalidsdp/env_metadata.parquet
- config_name: coq-math-classes-sources
data_files:
- split: train
path: coq-math-classes/sources.parquet
- config_name: coq-math-classes-toc_nodes
data_files:
- split: train
path: coq-math-classes/toc_nodes.parquet
- config_name: coq-math-classes-proofs
data_files:
- split: train
path: coq-math-classes/proofs.parquet
- config_name: coq-math-classes-proof_steps
data_files:
- split: train
path: coq-math-classes/proof_steps.parquet
- config_name: coq-math-classes-step_deps
data_files:
- split: train
path: coq-math-classes/step_deps.parquet
- config_name: coq-math-classes-proof_axioms
data_files:
- split: train
path: coq-math-classes/proof_axioms.parquet
- config_name: coq-math-classes-env_toc
data_files:
- split: train
path: coq-math-classes/env_toc.parquet
- config_name: coq-math-classes-env_metadata
data_files:
- split: train
path: coq-math-classes/env_metadata.parquet
- config_name: coq-mathcomp-sources
data_files:
- split: train
path: coq-mathcomp/sources.parquet
- config_name: coq-mathcomp-toc_nodes
data_files:
- split: train
path: coq-mathcomp/toc_nodes.parquet
- config_name: coq-mathcomp-proofs
data_files:
- split: train
path: coq-mathcomp/proofs.parquet
- config_name: coq-mathcomp-proof_steps
data_files:
- split: train
path: coq-mathcomp/proof_steps.parquet
- config_name: coq-mathcomp-step_deps
data_files:
- split: train
path: coq-mathcomp/step_deps.parquet
- config_name: coq-mathcomp-proof_axioms
data_files:
- split: train
path: coq-mathcomp/proof_axioms.parquet
- config_name: coq-mathcomp-env_toc
data_files:
- split: train
path: coq-mathcomp/env_toc.parquet
- config_name: coq-mathcomp-env_metadata
data_files:
- split: train
path: coq-mathcomp/env_metadata.parquet
- config_name: coq-mk-sources
data_files:
- split: train
path: coq-mk/sources.parquet
- config_name: coq-mk-toc_nodes
data_files:
- split: train
path: coq-mk/toc_nodes.parquet
- config_name: coq-mk-proofs
data_files:
- split: train
path: coq-mk/proofs.parquet
- config_name: coq-mk-proof_steps
data_files:
- split: train
path: coq-mk/proof_steps.parquet
- config_name: coq-mk-step_deps
data_files:
- split: train
path: coq-mk/step_deps.parquet
- config_name: coq-mk-proof_axioms
data_files:
- split: train
path: coq-mk/proof_axioms.parquet
- config_name: coq-mk-env_toc
data_files:
- split: train
path: coq-mk/env_toc.parquet
- config_name: coq-mk-env_metadata
data_files:
- split: train
path: coq-mk/env_metadata.parquet
- config_name: coq-mmaps-sources
data_files:
- split: train
path: coq-mmaps/sources.parquet
- config_name: coq-mmaps-toc_nodes
data_files:
- split: train
path: coq-mmaps/toc_nodes.parquet
- config_name: coq-mmaps-proofs
data_files:
- split: train
path: coq-mmaps/proofs.parquet
- config_name: coq-mmaps-proof_steps
data_files:
- split: train
path: coq-mmaps/proof_steps.parquet
- config_name: coq-mmaps-step_deps
data_files:
- split: train
path: coq-mmaps/step_deps.parquet
- config_name: coq-mmaps-proof_axioms
data_files:
- split: train
path: coq-mmaps/proof_axioms.parquet
- config_name: coq-mmaps-env_toc
data_files:
- split: train
path: coq-mmaps/env_toc.parquet
- config_name: coq-mmaps-env_metadata
data_files:
- split: train
path: coq-mmaps/env_metadata.parquet
- config_name: coq-ordinal-sources
data_files:
- split: train
path: coq-ordinal/sources.parquet
- config_name: coq-ordinal-toc_nodes
data_files:
- split: train
path: coq-ordinal/toc_nodes.parquet
- config_name: coq-ordinal-proofs
data_files:
- split: train
path: coq-ordinal/proofs.parquet
- config_name: coq-ordinal-proof_steps
data_files:
- split: train
path: coq-ordinal/proof_steps.parquet
- config_name: coq-ordinal-step_deps
data_files:
- split: train
path: coq-ordinal/step_deps.parquet
- config_name: coq-ordinal-proof_axioms
data_files:
- split: train
path: coq-ordinal/proof_axioms.parquet
- config_name: coq-ordinal-env_toc
data_files:
- split: train
path: coq-ordinal/env_toc.parquet
- config_name: coq-ordinal-env_metadata
data_files:
- split: train
path: coq-ordinal/env_metadata.parquet
- config_name: coq-pil-sources
data_files:
- split: train
path: coq-pil/sources.parquet
- config_name: coq-pil-toc_nodes
data_files:
- split: train
path: coq-pil/toc_nodes.parquet
- config_name: coq-pil-proofs
data_files:
- split: train
path: coq-pil/proofs.parquet
- config_name: coq-pil-proof_steps
data_files:
- split: train
path: coq-pil/proof_steps.parquet
- config_name: coq-pil-step_deps
data_files:
- split: train
path: coq-pil/step_deps.parquet
- config_name: coq-pil-proof_axioms
data_files:
- split: train
path: coq-pil/proof_axioms.parquet
- config_name: coq-pil-env_toc
data_files:
- split: train
path: coq-pil/env_toc.parquet
- config_name: coq-pil-env_metadata
data_files:
- split: train
path: coq-pil/env_metadata.parquet
- config_name: coq-plouffe-sources
data_files:
- split: train
path: coq-plouffe/sources.parquet
- config_name: coq-plouffe-toc_nodes
data_files:
- split: train
path: coq-plouffe/toc_nodes.parquet
- config_name: coq-plouffe-proofs
data_files:
- split: train
path: coq-plouffe/proofs.parquet
- config_name: coq-plouffe-proof_steps
data_files:
- split: train
path: coq-plouffe/proof_steps.parquet
- config_name: coq-plouffe-step_deps
data_files:
- split: train
path: coq-plouffe/step_deps.parquet
- config_name: coq-plouffe-proof_axioms
data_files:
- split: train
path: coq-plouffe/proof_axioms.parquet
- config_name: coq-plouffe-env_toc
data_files:
- split: train
path: coq-plouffe/env_toc.parquet
- config_name: coq-plouffe-env_metadata
data_files:
- split: train
path: coq-plouffe/env_metadata.parquet
- config_name: coq-quantumlib-sources
data_files:
- split: train
path: coq-quantumlib/sources.parquet
- config_name: coq-quantumlib-toc_nodes
data_files:
- split: train
path: coq-quantumlib/toc_nodes.parquet
- config_name: coq-quantumlib-proofs
data_files:
- split: train
path: coq-quantumlib/proofs.parquet
- config_name: coq-quantumlib-proof_steps
data_files:
- split: train
path: coq-quantumlib/proof_steps.parquet
- config_name: coq-quantumlib-step_deps
data_files:
- split: train
path: coq-quantumlib/step_deps.parquet
- config_name: coq-quantumlib-proof_axioms
data_files:
- split: train
path: coq-quantumlib/proof_axioms.parquet
- config_name: coq-quantumlib-env_toc
data_files:
- split: train
path: coq-quantumlib/env_toc.parquet
- config_name: coq-quantumlib-env_metadata
data_files:
- split: train
path: coq-quantumlib/env_metadata.parquet
- config_name: coq-quickchick-sources
data_files:
- split: train
path: coq-quickchick/sources.parquet
- config_name: coq-quickchick-toc_nodes
data_files:
- split: train
path: coq-quickchick/toc_nodes.parquet
- config_name: coq-quickchick-proofs
data_files:
- split: train
path: coq-quickchick/proofs.parquet
- config_name: coq-quickchick-proof_steps
data_files:
- split: train
path: coq-quickchick/proof_steps.parquet
- config_name: coq-quickchick-step_deps
data_files:
- split: train
path: coq-quickchick/step_deps.parquet
- config_name: coq-quickchick-proof_axioms
data_files:
- split: train
path: coq-quickchick/proof_axioms.parquet
- config_name: coq-quickchick-env_toc
data_files:
- split: train
path: coq-quickchick/env_toc.parquet
- config_name: coq-quickchick-env_metadata
data_files:
- split: train
path: coq-quickchick/env_metadata.parquet
- config_name: coq-reglang-sources
data_files:
- split: train
path: coq-reglang/sources.parquet
- config_name: coq-reglang-toc_nodes
data_files:
- split: train
path: coq-reglang/toc_nodes.parquet
- config_name: coq-reglang-proofs
data_files:
- split: train
path: coq-reglang/proofs.parquet
- config_name: coq-reglang-proof_steps
data_files:
- split: train
path: coq-reglang/proof_steps.parquet
- config_name: coq-reglang-step_deps
data_files:
- split: train
path: coq-reglang/step_deps.parquet
- config_name: coq-reglang-proof_axioms
data_files:
- split: train
path: coq-reglang/proof_axioms.parquet
- config_name: coq-reglang-env_toc
data_files:
- split: train
path: coq-reglang/env_toc.parquet
- config_name: coq-reglang-env_metadata
data_files:
- split: train
path: coq-reglang/env_metadata.parquet
- config_name: coq-relation-sources
data_files:
- split: train
path: coq-relation/sources.parquet
- config_name: coq-relation-toc_nodes
data_files:
- split: train
path: coq-relation/toc_nodes.parquet
- config_name: coq-relation-proofs
data_files:
- split: train
path: coq-relation/proofs.parquet
- config_name: coq-relation-proof_steps
data_files:
- split: train
path: coq-relation/proof_steps.parquet
- config_name: coq-relation-step_deps
data_files:
- split: train
path: coq-relation/step_deps.parquet
- config_name: coq-relation-proof_axioms
data_files:
- split: train
path: coq-relation/proof_axioms.parquet
- config_name: coq-relation-env_toc
data_files:
- split: train
path: coq-relation/env_toc.parquet
- config_name: coq-relation-env_metadata
data_files:
- split: train
path: coq-relation/env_metadata.parquet
- config_name: coq-sail-sources
data_files:
- split: train
path: coq-sail/sources.parquet
- config_name: coq-sail-toc_nodes
data_files:
- split: train
path: coq-sail/toc_nodes.parquet
- config_name: coq-sail-proofs
data_files:
- split: train
path: coq-sail/proofs.parquet
- config_name: coq-sail-proof_steps
data_files:
- split: train
path: coq-sail/proof_steps.parquet
- config_name: coq-sail-step_deps
data_files:
- split: train
path: coq-sail/step_deps.parquet
- config_name: coq-sail-proof_axioms
data_files:
- split: train
path: coq-sail/proof_axioms.parquet
- config_name: coq-sail-env_toc
data_files:
- split: train
path: coq-sail/env_toc.parquet
- config_name: coq-sail-env_metadata
data_files:
- split: train
path: coq-sail/env_metadata.parquet
- config_name: coq-ssprove-sources
data_files:
- split: train
path: coq-ssprove/sources.parquet
- config_name: coq-ssprove-toc_nodes
data_files:
- split: train
path: coq-ssprove/toc_nodes.parquet
- config_name: coq-ssprove-proofs
data_files:
- split: train
path: coq-ssprove/proofs.parquet
- config_name: coq-ssprove-proof_steps
data_files:
- split: train
path: coq-ssprove/proof_steps.parquet
- config_name: coq-ssprove-step_deps
data_files:
- split: train
path: coq-ssprove/step_deps.parquet
- config_name: coq-ssprove-proof_axioms
data_files:
- split: train
path: coq-ssprove/proof_axioms.parquet
- config_name: coq-ssprove-env_toc
data_files:
- split: train
path: coq-ssprove/env_toc.parquet
- config_name: coq-ssprove-env_metadata
data_files:
- split: train
path: coq-ssprove/env_metadata.parquet
- config_name: coq-stdpp-sources
data_files:
- split: train
path: coq-stdpp/sources.parquet
- config_name: coq-stdpp-toc_nodes
data_files:
- split: train
path: coq-stdpp/toc_nodes.parquet
- config_name: coq-stdpp-proofs
data_files:
- split: train
path: coq-stdpp/proofs.parquet
- config_name: coq-stdpp-proof_steps
data_files:
- split: train
path: coq-stdpp/proof_steps.parquet
- config_name: coq-stdpp-step_deps
data_files:
- split: train
path: coq-stdpp/step_deps.parquet
- config_name: coq-stdpp-proof_axioms
data_files:
- split: train
path: coq-stdpp/proof_axioms.parquet
- config_name: coq-stdpp-env_toc
data_files:
- split: train
path: coq-stdpp/env_toc.parquet
- config_name: coq-stdpp-env_metadata
data_files:
- split: train
path: coq-stdpp/env_metadata.parquet
- config_name: coq-trocq-sources
data_files:
- split: train
path: coq-trocq/sources.parquet
- config_name: coq-trocq-toc_nodes
data_files:
- split: train
path: coq-trocq/toc_nodes.parquet
- config_name: coq-trocq-proofs
data_files:
- split: train
path: coq-trocq/proofs.parquet
- config_name: coq-trocq-proof_steps
data_files:
- split: train
path: coq-trocq/proof_steps.parquet
- config_name: coq-trocq-step_deps
data_files:
- split: train
path: coq-trocq/step_deps.parquet
- config_name: coq-trocq-proof_axioms
data_files:
- split: train
path: coq-trocq/proof_axioms.parquet
- config_name: coq-trocq-env_toc
data_files:
- split: train
path: coq-trocq/env_toc.parquet
- config_name: coq-trocq-env_metadata
data_files:
- split: train
path: coq-trocq/env_metadata.parquet
- config_name: coq-unimath-sources
data_files:
- split: train
path: coq-unimath/sources.parquet
- config_name: coq-unimath-toc_nodes
data_files:
- split: train
path: coq-unimath/toc_nodes.parquet
- config_name: coq-unimath-proofs
data_files:
- split: train
path: coq-unimath/proofs.parquet
- config_name: coq-unimath-proof_steps
data_files:
- split: train
path: coq-unimath/proof_steps.parquet
- config_name: coq-unimath-step_deps
data_files:
- split: train
path: coq-unimath/step_deps.parquet
- config_name: coq-unimath-proof_axioms
data_files:
- split: train
path: coq-unimath/proof_axioms.parquet
- config_name: coq-unimath-env_toc
data_files:
- split: train
path: coq-unimath/env_toc.parquet
- config_name: coq-unimath-env_metadata
data_files:
- split: train
path: coq-unimath/env_metadata.parquet
- config_name: coq-zorns-lemma-sources
data_files:
- split: train
path: coq-zorns-lemma/sources.parquet
- config_name: coq-zorns-lemma-toc_nodes
data_files:
- split: train
path: coq-zorns-lemma/toc_nodes.parquet
- config_name: coq-zorns-lemma-proofs
data_files:
- split: train
path: coq-zorns-lemma/proofs.parquet
- config_name: coq-zorns-lemma-proof_steps
data_files:
- split: train
path: coq-zorns-lemma/proof_steps.parquet
- config_name: coq-zorns-lemma-step_deps
data_files:
- split: train
path: coq-zorns-lemma/step_deps.parquet
- config_name: coq-zorns-lemma-proof_axioms
data_files:
- split: train
path: coq-zorns-lemma/proof_axioms.parquet
- config_name: coq-zorns-lemma-env_toc
data_files:
- split: train
path: coq-zorns-lemma/env_toc.parquet
- config_name: coq-zorns-lemma-env_metadata
data_files:
- split: train
path: coq-zorns-lemma/env_metadata.parquet
- config_name: rocq-metarocq-sources
data_files:
- split: train
path: rocq-metarocq/sources.parquet
- config_name: rocq-metarocq-toc_nodes
data_files:
- split: train
path: rocq-metarocq/toc_nodes.parquet
- config_name: rocq-metarocq-proofs
data_files:
- split: train
path: rocq-metarocq/proofs.parquet
- config_name: rocq-metarocq-proof_steps
data_files:
- split: train
path: rocq-metarocq/proof_steps.parquet
- config_name: rocq-metarocq-step_deps
data_files:
- split: train
path: rocq-metarocq/step_deps.parquet
- config_name: rocq-metarocq-proof_axioms
data_files:
- split: train
path: rocq-metarocq/proof_axioms.parquet
- config_name: rocq-metarocq-env_toc
data_files:
- split: train
path: rocq-metarocq/env_toc.parquet
- config_name: rocq-metarocq-env_metadata
data_files:
- split: train
path: rocq-metarocq/env_metadata.parquet
- config_name: rocq-num-analysis-sources
data_files:
- split: train
path: rocq-num-analysis/sources.parquet
- config_name: rocq-num-analysis-toc_nodes
data_files:
- split: train
path: rocq-num-analysis/toc_nodes.parquet
- config_name: rocq-num-analysis-proofs
data_files:
- split: train
path: rocq-num-analysis/proofs.parquet
- config_name: rocq-num-analysis-proof_steps
data_files:
- split: train
path: rocq-num-analysis/proof_steps.parquet
- config_name: rocq-num-analysis-step_deps
data_files:
- split: train
path: rocq-num-analysis/step_deps.parquet
- config_name: rocq-num-analysis-proof_axioms
data_files:
- split: train
path: rocq-num-analysis/proof_axioms.parquet
- config_name: rocq-num-analysis-env_toc
data_files:
- split: train
path: rocq-num-analysis/env_toc.parquet
- config_name: rocq-num-analysis-env_metadata
data_files:
- split: train
path: rocq-num-analysis/env_metadata.parquet
- config_name: rocq-ollibs-sources
data_files:
- split: train
path: rocq-ollibs/sources.parquet
- config_name: rocq-ollibs-toc_nodes
data_files:
- split: train
path: rocq-ollibs/toc_nodes.parquet
- config_name: rocq-ollibs-proofs
data_files:
- split: train
path: rocq-ollibs/proofs.parquet
- config_name: rocq-ollibs-proof_steps
data_files:
- split: train
path: rocq-ollibs/proof_steps.parquet
- config_name: rocq-ollibs-step_deps
data_files:
- split: train
path: rocq-ollibs/step_deps.parquet
- config_name: rocq-ollibs-proof_axioms
data_files:
- split: train
path: rocq-ollibs/proof_axioms.parquet
- config_name: rocq-ollibs-env_toc
data_files:
- split: train
path: rocq-ollibs/env_toc.parquet
- config_name: rocq-ollibs-env_metadata
data_files:
- split: train
path: rocq-ollibs/env_metadata.parquet
- config_name: rocq-pi-agm-sources
data_files:
- split: train
path: rocq-pi-agm/sources.parquet
- config_name: rocq-pi-agm-toc_nodes
data_files:
- split: train
path: rocq-pi-agm/toc_nodes.parquet
- config_name: rocq-pi-agm-proofs
data_files:
- split: train
path: rocq-pi-agm/proofs.parquet
- config_name: rocq-pi-agm-proof_steps
data_files:
- split: train
path: rocq-pi-agm/proof_steps.parquet
- config_name: rocq-pi-agm-step_deps
data_files:
- split: train
path: rocq-pi-agm/step_deps.parquet
- config_name: rocq-pi-agm-proof_axioms
data_files:
- split: train
path: rocq-pi-agm/proof_axioms.parquet
- config_name: rocq-pi-agm-env_toc
data_files:
- split: train
path: rocq-pi-agm/env_toc.parquet
- config_name: rocq-pi-agm-env_metadata
data_files:
- split: train
path: rocq-pi-agm/env_metadata.parquet
- config_name: rocq-relation-algebra-sources
data_files:
- split: train
path: rocq-relation-algebra/sources.parquet
- config_name: rocq-relation-algebra-toc_nodes
data_files:
- split: train
path: rocq-relation-algebra/toc_nodes.parquet
- config_name: rocq-relation-algebra-proofs
data_files:
- split: train
path: rocq-relation-algebra/proofs.parquet
- config_name: rocq-relation-algebra-proof_steps
data_files:
- split: train
path: rocq-relation-algebra/proof_steps.parquet
- config_name: rocq-relation-algebra-step_deps
data_files:
- split: train
path: rocq-relation-algebra/step_deps.parquet
- config_name: rocq-relation-algebra-proof_axioms
data_files:
- split: train
path: rocq-relation-algebra/proof_axioms.parquet
- config_name: rocq-relation-algebra-env_toc
data_files:
- split: train
path: rocq-relation-algebra/env_toc.parquet
- config_name: rocq-relation-algebra-env_metadata
data_files:
- split: train
path: rocq-relation-algebra/env_metadata.parquet
- config_name: rocq-rouche-capelli-sources
data_files:
- split: train
path: rocq-rouche-capelli/sources.parquet
- config_name: rocq-rouche-capelli-toc_nodes
data_files:
- split: train
path: rocq-rouche-capelli/toc_nodes.parquet
- config_name: rocq-rouche-capelli-proofs
data_files:
- split: train
path: rocq-rouche-capelli/proofs.parquet
- config_name: rocq-rouche-capelli-proof_steps
data_files:
- split: train
path: rocq-rouche-capelli/proof_steps.parquet
- config_name: rocq-rouche-capelli-step_deps
data_files:
- split: train
path: rocq-rouche-capelli/step_deps.parquet
- config_name: rocq-rouche-capelli-proof_axioms
data_files:
- split: train
path: rocq-rouche-capelli/proof_axioms.parquet
- config_name: rocq-rouche-capelli-env_toc
data_files:
- split: train
path: rocq-rouche-capelli/env_toc.parquet
- config_name: rocq-rouche-capelli-env_metadata
data_files:
- split: train
path: rocq-rouche-capelli/env_metadata.parquet
---

# theostos/pile-of-rocq

Pile-of-Rocq exported as normalized parquet tables with `docstring` + `env_toc`.

Each config is `<env>-<table>` and loads one parquet table for one env.

## Load examples
```python
from datasets import load_dataset

toc = load_dataset('theostos/pile-of-rocq', 'coq-actuary-toc_nodes', split='train')
steps = load_dataset('theostos/pile-of-rocq', 'coq-actuary-proof_steps', split='train')
print(len(toc), len(steps))
```

## Environments in this export
- count: 48
- `coq-actuary`
- `coq-atbr`
- `coq-color`
- `coq-compcert`
- `coq-coqeal`
- `coq-coqprime`
- `coq-coqtail`
- `coq-coquelicot`
- `coq-corn`
- `coq-ext-lib`
- `coq-extructures`
- `coq-fcsl-pcm`
- `coq-flocq`
- `coq-fourcolor`
- `coq-geocoq`
- `coq-graph-theory`
- `coq-high-school-geometry`
- `coq-hott`
- `coq-infotheo`
- `coq-iris`
- `coq-itree`
- `coq-karp-miller`
- `coq-kruskal`
- `coq-library-fol`
- `coq-libvalidsdp`
- `coq-math-classes`
- `coq-mathcomp`
- `coq-mk`
- `coq-mmaps`
- `coq-ordinal`
- `coq-pil`
- `coq-plouffe`
- `coq-quantumlib`
- `coq-quickchick`
- `coq-reglang`
- `coq-relation`
- `coq-sail`
- `coq-ssprove`
- `coq-stdpp`
- `coq-trocq`
- `coq-unimath`
- `coq-zorns-lemma`
- `rocq-metarocq`
- `rocq-num-analysis`
- `rocq-ollibs`
- `rocq-pi-agm`
- `rocq-relation-algebra`
- `rocq-rouche-capelli`