Dataset Preview
The full dataset viewer is not available (click to read why). Only showing a preview of the rows.
The dataset generation failed
Error code: DatasetGenerationError
Exception: TypeError
Message: int() argument must be a string, a bytes-like object or a real number, not 'NoneType'
Traceback: Traceback (most recent call last):
File "/usr/local/lib/python3.14/site-packages/datasets/builder.py", line 1531, in _prepare_split_single
for key, record in generator:
^^^^^^^^^
File "/src/services/worker/src/worker/job_runners/config/parquet_and_info.py", line 613, in wrapped
for item in generator(*args, **kwargs):
~~~~~~~~~^^^^^^^^^^^^^^^^^
File "/usr/local/lib/python3.14/site-packages/datasets/packaged_modules/webdataset/webdataset.py", line 127, in _generate_examples
for example_idx, example in enumerate(self._get_pipeline_from_tar(tar_path, tar_iterator)):
~~~~~~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/usr/local/lib/python3.14/site-packages/datasets/packaged_modules/webdataset/webdataset.py", line 32, in _get_pipeline_from_tar
for filename, f in tar_iterator:
^^^^^^^^^^^^
File "/usr/local/lib/python3.14/site-packages/datasets/utils/track.py", line 49, in __iter__
for x in self.generator(*self.args):
~~~~~~~~~~~~~~^^^^^^^^^^^^
File "/usr/local/lib/python3.14/site-packages/datasets/utils/file_utils.py", line 1400, in _iter_from_urlpath
with xopen(urlpath, "rb", download_config=download_config, block_size=0) as f:
~~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/usr/local/lib/python3.14/site-packages/datasets/utils/file_utils.py", line 977, in xopen
file_obj = fs.open(paths[0], mode)
File "<string>", line 3, in open
File "/usr/local/lib/python3.14/unittest/mock.py", line 1176, in __call__
return self._mock_call(*args, **kwargs)
~~~~~~~~~~~~~~~^^^^^^^^^^^^^^^^^
File "/usr/local/lib/python3.14/unittest/mock.py", line 1180, in _mock_call
return self._execute_mock_call(*args, **kwargs)
~~~~~~~~~~~~~~~~~~~~~~~^^^^^^^^^^^^^^^^^
File "/usr/local/lib/python3.14/unittest/mock.py", line 1247, in _execute_mock_call
result = effect(*args, **kwargs)
File "/src/services/worker/src/worker/job_runners/config/parquet_and_info.py", line 786, in wrapped
tracker.files[urlpath] = {"read": 0, "size": int(f.size)}
~~~^^^^^^^^
TypeError: int() argument must be a string, a bytes-like object or a real number, not 'NoneType'
The above exception was the direct cause of the following exception:
Traceback (most recent call last):
File "/src/services/worker/src/worker/job_runners/config/parquet_and_info.py", line 1369, in compute_config_parquet_and_info_response
parquet_operations, partial, estimated_dataset_info = stream_convert_to_parquet(
~~~~~~~~~~~~~~~~~~~~~~~~~^
builder, max_dataset_size_bytes=max_dataset_size_bytes
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
)
^
File "/src/services/worker/src/worker/job_runners/config/parquet_and_info.py", line 948, in stream_convert_to_parquet
builder._prepare_split(split_generator=splits_generators[split], file_format="parquet")
~~~~~~~~~~~~~~~~~~~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/usr/local/lib/python3.14/site-packages/datasets/builder.py", line 1393, in _prepare_split
for job_id, done, content in self._prepare_split_single(
~~~~~~~~~~~~~~~~~~~~~~~~~~^
gen_kwargs=gen_kwargs, job_id=job_id, **_prepare_split_args
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
):
^
File "/usr/local/lib/python3.14/site-packages/datasets/builder.py", line 1571, in _prepare_split_single
raise DatasetGenerationError("An error occurred while generating the dataset") from e
datasets.exceptions.DatasetGenerationError: An error occurred while generating the datasetNeed help to make the dataset viewer work? Make sure to review how to configure the dataset viewer, and open a discussion for direct support.
sample unknown | __key__ string | __url__ string |
|---|---|---|
[
35,
33,
47,
98,
105,
110,
47,
115,
104,
10,
35,
10,
35,
32,
65,
110,
32,
101,
120,
97,
109,
112,
108,
101,
32,
104,
111,
111,
107,
32,
115,
99,
114,
105,
112,
116,
32,
116,
111,
32,
99,
104,
101,
99,
107,
32,
116,
104,
1... | v4.28.0/.git/hooks/applypatch-msg | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
[
35,
33,
47,
98,
105,
110,
47,
115,
104,
10,
35,
10,
35,
32,
65,
110,
32,
101,
120,
97,
109,
112,
108,
101,
32,
104,
111,
111,
107,
32,
115,
99,
114,
105,
112,
116,
32,
116,
111,
32,
99,
104,
101,
99,
107,
32,
116,
104,
1... | v4.28.0/.git/hooks/commit-msg | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
[
35,
33,
47,
117,
115,
114,
47,
98,
105,
110,
47,
112,
101,
114,
108,
10,
10,
117,
115,
101,
32,
115,
116,
114,
105,
99,
116,
59,
10,
117,
115,
101,
32,
119,
97,
114,
110,
105,
110,
103,
115,
59,
10,
117,
115,
101,
32,
73,
... | v4.28.0/.git/hooks/fsmonitor-watchman | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
[
35,
33,
47,
98,
105,
110,
47,
115,
104,
10,
35,
10,
35,
32,
65,
110,
32,
101,
120,
97,
109,
112,
108,
101,
32,
104,
111,
111,
107,
32,
115,
99,
114,
105,
112,
116,
32,
116,
111,
32,
112,
114,
101,
112,
97,
114,
101,
32,
... | v4.28.0/.git/hooks/post-update | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
[
35,
33,
47,
98,
105,
110,
47,
115,
104,
10,
35,
10,
35,
32,
65,
110,
32,
101,
120,
97,
109,
112,
108,
101,
32,
104,
111,
111,
107,
32,
115,
99,
114,
105,
112,
116,
32,
116,
111,
32,
118,
101,
114,
105,
102,
121,
32,
119,
... | v4.28.0/.git/hooks/pre-applypatch | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
[
35,
33,
47,
98,
105,
110,
47,
115,
104,
10,
35,
10,
35,
32,
65,
110,
32,
101,
120,
97,
109,
112,
108,
101,
32,
104,
111,
111,
107,
32,
115,
99,
114,
105,
112,
116,
32,
116,
111,
32,
118,
101,
114,
105,
102,
121,
32,
119,
... | v4.28.0/.git/hooks/pre-commit | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
[
35,
33,
47,
98,
105,
110,
47,
115,
104,
10,
35,
10,
35,
32,
65,
110,
32,
101,
120,
97,
109,
112,
108,
101,
32,
104,
111,
111,
107,
32,
115,
99,
114,
105,
112,
116,
32,
116,
111,
32,
118,
101,
114,
105,
102,
121,
32,
119,
... | v4.28.0/.git/hooks/pre-merge-commit | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
[
35,
33,
47,
98,
105,
110,
47,
115,
104,
10,
10,
35,
32,
65,
110,
32,
101,
120,
97,
109,
112,
108,
101,
32,
104,
111,
111,
107,
32,
115,
99,
114,
105,
112,
116,
32,
116,
111,
32,
118,
101,
114,
105,
102,
121,
32,
119,
104,
... | v4.28.0/.git/hooks/pre-push | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
[
35,
33,
47,
98,
105,
110,
47,
115,
104,
10,
35,
10,
35,
32,
67,
111,
112,
121,
114,
105,
103,
104,
116,
32,
40,
99,
41,
32,
50,
48,
48,
54,
44,
32,
50,
48,
48,
56,
32,
74,
117,
110,
105,
111,
32,
67,
32,
72,
97,
109,
... | v4.28.0/.git/hooks/pre-rebase | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
[
35,
33,
47,
98,
105,
110,
47,
115,
104,
10,
35,
10,
35,
32,
65,
110,
32,
101,
120,
97,
109,
112,
108,
101,
32,
104,
111,
111,
107,
32,
115,
99,
114,
105,
112,
116,
32,
116,
111,
32,
109,
97,
107,
101,
32,
117,
115,
101,
... | v4.28.0/.git/hooks/pre-receive | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
[
35,
33,
47,
98,
105,
110,
47,
115,
104,
10,
35,
10,
35,
32,
65,
110,
32,
101,
120,
97,
109,
112,
108,
101,
32,
104,
111,
111,
107,
32,
115,
99,
114,
105,
112,
116,
32,
116,
111,
32,
112,
114,
101,
112,
97,
114,
101,
32,
... | v4.28.0/.git/hooks/prepare-commit-msg | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
[
35,
33,
47,
98,
105,
110,
47,
115,
104,
10,
10,
35,
32,
65,
110,
32,
101,
120,
97,
109,
112,
108,
101,
32,
104,
111,
111,
107,
32,
115,
99,
114,
105,
112,
116,
32,
116,
111,
32,
117,
112,
100,
97,
116,
101,
32,
97,
32,
9... | v4.28.0/.git/hooks/push-to-checkout | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
[
35,
33,
47,
98,
105,
110,
47,
115,
104,
10,
10,
35,
32,
65,
110,
32,
101,
120,
97,
109,
112,
108,
101,
32,
104,
111,
111,
107,
32,
115,
99,
114,
105,
112,
116,
32,
116,
111,
32,
118,
97,
108,
105,
100,
97,
116,
101,
32,
... | v4.28.0/.git/hooks/sendemail-validate | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
[
35,
33,
47,
98,
105,
110,
47,
115,
104,
10,
35,
10,
35,
32,
65,
110,
32,
101,
120,
97,
109,
112,
108,
101,
32,
104,
111,
111,
107,
32,
115,
99,
114,
105,
112,
116,
32,
116,
111,
32,
98,
108,
111,
99,
107,
32,
117,
110,
9... | v4.28.0/.git/hooks/update | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.git/objects/pack/pack-74ecd7f034501279e47278042591d14454503002 | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.github/workflows-archive/README | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.github/workflows-archive/blueprint-old | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.github/workflows/check-imports | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.github/workflows/ci | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.github/workflows/docs | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.github/workflows/pr-summary | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.github/workflows/release-tag | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.github/workflows/review | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.github/workflows/update | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.github/dependabot | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/Data/Classes/Slice | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/Data/CodingTheory/BerlekampWelch/BerlekampWelch | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/Data/CodingTheory/BerlekampWelch/Condition | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/Data/CodingTheory/BerlekampWelch/ElocPoly | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/Data/CodingTheory/BerlekampWelch/Existence | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/Data/CodingTheory/BerlekampWelch/Sorries | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/Data/CodingTheory/Basic | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/Data/CodingTheory/Prelims | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/Data/CodingTheory/ReedSolomon | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/Data/Fin/Tuple/Defs | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/Data/Fin/Tuple/Lemmas | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/Data/Fin/Tuple/Notation | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/Data/Fin/Basic | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/Data/Fin/Fold | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/Data/Fin/Lift | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/Data/Fin/Sigma | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/Data/MvPolynomial/Degrees | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/Data/MvPolynomial/Interpolation | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/Data/MvPolynomial/LinearMvExtension | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/Data/MvPolynomial/Multilinear | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/Data/Polynomial/Interface | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/OracleReduction/Composition/Sequential/Append | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/OracleReduction/Composition/Sequential/General | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/OracleReduction/LiftContext/Lens | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/OracleReduction/LiftContext/OracleReduction | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/OracleReduction/LiftContext/Reduction | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/OracleReduction/ProtocolSpec/Basic | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/OracleReduction/ProtocolSpec/Cast | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/OracleReduction/ProtocolSpec/SeqCompose | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/OracleReduction/Security/Basic | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/OracleReduction/Security/RoundByRound | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/OracleReduction/Basic | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/OracleReduction/Execution | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/OracleReduction/OracleInterface | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/OracleReduction/Prelude | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/ProofSystem/Component/CheckClaim | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/ProofSystem/Component/RandomQuery | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/ProofSystem/Component/ReduceClaim | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/ProofSystem/Component/SendClaim | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/ProofSystem/Sumcheck/Spec/SingleRound | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/ToVCVio/Lemmas | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/ToVCVio/Oracle | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/ir/ArkLib/ToVCVio/SimOracle | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/Data/Classes/Slice | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/Data/CodingTheory/BerlekampWelch/BerlekampWelch | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/Data/CodingTheory/BerlekampWelch/Condition | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/Data/CodingTheory/BerlekampWelch/ElocPoly | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/Data/CodingTheory/BerlekampWelch/Existence | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/Data/CodingTheory/BerlekampWelch/Sorries | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/Data/CodingTheory/Basic | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/Data/CodingTheory/Prelims | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/Data/CodingTheory/ReedSolomon | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/Data/Fin/Tuple/Defs | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/Data/Fin/Tuple/Lemmas | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/Data/Fin/Tuple/Notation | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/Data/Fin/Basic | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/Data/Fin/Fold | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/Data/Fin/Lift | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/Data/Fin/Sigma | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/Data/MvPolynomial/Degrees | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/Data/MvPolynomial/Interpolation | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/Data/MvPolynomial/LinearMvExtension | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/Data/MvPolynomial/Multilinear | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/Data/Polynomial/Interface | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/OracleReduction/Composition/Sequential/Append | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/OracleReduction/Composition/Sequential/General | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/OracleReduction/LiftContext/Lens | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/OracleReduction/LiftContext/OracleReduction | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/OracleReduction/LiftContext/Reduction | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/OracleReduction/ProtocolSpec/Basic | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/OracleReduction/ProtocolSpec/Cast | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/OracleReduction/ProtocolSpec/SeqCompose | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/OracleReduction/Security/Basic | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
null | v4.28.0/.lake/build/lib/lean/ArkLib/OracleReduction/Security/RoundByRound | hf://datasets/grenadeComing/lean-refactor-envs@13980598ab58a0a43a7038d195a507f05c0d4d6e/projects/arklib/v4.28.0.tar.gz |
End of preview.
Lean environments for the Lean Refactor Arena
This repo contains the prebuilt Lean environments (dependencies such as Mathlib already compiled) of Strata, PhysLib, CSLib, ArkLib and PutnamBench, for every Lean version the warm-up problems list. LeanPool will be added for the final benchmark. Linux x86_64.
| Project | Folder | Lean versions |
|---|---|---|
| Strata | projects/strata |
v4.26.0, v4.27.0, v4.29.1 |
| PhysLib | projects/physlib |
v4.32.0 |
| CSLib | projects/cslib |
v4.30.0, v4.31.0, v4.32.0, v4.33.0-rc2 |
| ArkLib | projects/arklib |
v4.28.0, v4.29.0, v4.30.0, v4.31.0 |
| PutnamBench | projects/putnambench |
v4.25.0, v4.26.0, v4.27.0 |
| LeanPool | to be added |
Also included: Lean REPL builds (repl/: v4.26.0, v4.31.0, v4.32.0) and Lean toolchains (toolchains/: v4.25.0 to
v4.33.0-rc2). Each archive is <version>.tar.gz; manifest.json lists git revisions and checksums.
Restore: python environments/restore.py --repo grenadeComing/lean-refactor-envs --root <dir> --check
- Downloads last month
- 47