Spaces:
Runtime error
Runtime error
Update app.py
Browse files
app.py
CHANGED
|
@@ -17,7 +17,7 @@ def load_data(lang):
|
|
| 17 |
split = "lean_proofsteps"
|
| 18 |
elif lang == "Isabelle Proofsteps":
|
| 19 |
split = "isa_proofsteps"
|
| 20 |
-
ds = load_dataset("xu3kev/proof-pile-2-proofsteps", split="
|
| 21 |
return ds
|
| 22 |
|
| 23 |
list_languages = ['Lean Proofsteps', 'Isabelle Proofsteps']
|
|
|
|
| 17 |
split = "lean_proofsteps"
|
| 18 |
elif lang == "Isabelle Proofsteps":
|
| 19 |
split = "isa_proofsteps"
|
| 20 |
+
ds = load_dataset("xu3kev/proof-pile-2-proofsteps", split=f"{split}[:2%]")
|
| 21 |
return ds
|
| 22 |
|
| 23 |
list_languages = ['Lean Proofsteps', 'Isabelle Proofsteps']
|