Spaces:
Runtime error
Runtime error
File size: 1,780 Bytes
f9f24ec 50b49a8 f9f24ec 94d1d62 2319432 e406738 f9f24ec f698f3c 94d1d62 f698f3c 4f34678 e04d7d7 2db7e37 f9f24ec e04d7d7 f9b254f e04d7d7 f698f3c 488a55a 0974549 94d1d62 07da79f 94d1d62 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 |
import streamlit as st
import json
from datasets import load_dataset
import sqlparse
st.set_page_config(page_title="Proofsteps from Proof-Pile-V2", layout="wide")
st.markdown("<h1 style='text-align: center; color: #00BFFF;'>Proofsteps Insepction 🔍</h1>", unsafe_allow_html=True)
st.markdown("""
Here you can inspect proofsteps from [Proof-Pile-V2](https://huggingface.co/datasets/EleutherAI/proof-pile-2).
""")
@st.cache(max_entries=100)
def load_data(lang):
if lang == "Lean Proofsteps":
split = "lean_proofsteps"
elif lang == "Isabelle Proofsteps":
split = "isa_proofsteps"
ds = load_dataset("xu3kev/proof-pile-2-proofsteps", split=f"{split}[:5%]")
return ds
list_languages = ['Lean Proofsteps', 'Isabelle Proofsteps']
chosen_language = st.sidebar.selectbox(
label="Select a Proof Language", options=list_languages, index=0
)
print(chosen_language)
samples = load_data(chosen_language)
st.sidebar.header('Sample Selection')
index_example = st.sidebar.number_input(f"Choose a sample from the existing {len(samples)} samples:", min_value=0, max_value=max(0, len(samples)-1), value=0, step=1)
#db_id = samples[index_example]["db_id"]
#st.markdown(f'<h2 style="color:blue;">{index_example} Question:</h2>', unsafe_allow_html=True)
#st.code(samples[index_example]["question"])
#sql_str = samples[index_example]["SQL"]
#sql_str_pretty = sqlparse.format(sql_str, reindent=True, keyword_case='upper')
#st.markdown(f'<h2 style="color:blue;">SQL:</h2>', unsafe_allow_html=True)
#st.code(sql_str_pretty)
st.markdown(f'<h2 style="color:blue;">Content:</h2>', unsafe_allow_html=True)
st.code(samples[index_example]["text"])
#st.markdown(f'<h2 style="color:blue;">Metadata:</h2>', unsafe_allow_html=True)
#st.code(samples[index_example]["meta"])
|