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.