Spaces:
Runtime error
Runtime error
Update app.py
Browse files
app.py
CHANGED
|
@@ -12,12 +12,20 @@ Here you can inspect proofsteps from [Proof-Pile-V2](https://huggingface.co/data
|
|
| 12 |
""")
|
| 13 |
|
| 14 |
@st.cache()
|
| 15 |
-
def load_data():
|
| 16 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
| 17 |
return ds
|
| 18 |
|
|
|
|
|
|
|
|
|
|
|
|
|
| 19 |
|
| 20 |
-
samples = load_data()
|
| 21 |
st.sidebar.header('Sample Selection')
|
| 22 |
index_example = st.sidebar.number_input(f"Choose a sample from the existing {len(samples)} notebooks:", min_value=0, max_value=max(0, len(samples)-1), value=0, step=1)
|
| 23 |
|
|
|
|
| 12 |
""")
|
| 13 |
|
| 14 |
@st.cache()
|
| 15 |
+
def load_data(lang):
|
| 16 |
+
if lang == "Lean Proofsteps":
|
| 17 |
+
split = "lean_proofsteps"
|
| 18 |
+
elif lang == "Isabelle Proofsteps":
|
| 19 |
+
split = "isa_proofsteps"
|
| 20 |
+
ds = load_dataset("xu3kev/proof-pile-2-proofsteps", split="lean_proofsteps[:2%]")
|
| 21 |
return ds
|
| 22 |
|
| 23 |
+
list_languages = ['Lean Proofsteps', 'Isabelle Proofsteps']
|
| 24 |
+
chosen_language = st.sidebar.selectbox(
|
| 25 |
+
label="Select a Proof Language", options=list_languages, index=0
|
| 26 |
+
)
|
| 27 |
|
| 28 |
+
samples = load_data(chosen_language)
|
| 29 |
st.sidebar.header('Sample Selection')
|
| 30 |
index_example = st.sidebar.number_input(f"Choose a sample from the existing {len(samples)} notebooks:", min_value=0, max_value=max(0, len(samples)-1), value=0, step=1)
|
| 31 |
|