Datasetpublic

theostos/pile-of-rocq

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 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… See the full description on the dataset page: https://huggingface.co/datasets/theostos/pile-of-rocq.

sourceHugging Faceupdated 5mo agoView on Hugging Face

0likes2.6kdownloads

Dataset Card

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