Spaces:
Runtime error
Runtime error
| 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). | |
| """) | |
| 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"]) | |