Spaces:
Build error
Build error
Update app.py
Browse files
app.py
CHANGED
|
@@ -31,37 +31,6 @@ plt.rcParams.update({
|
|
| 31 |
"text.latex.preamble": r"\usepackage{amsmath,amssymb}"
|
| 32 |
})
|
| 33 |
|
| 34 |
-
def show_latex(formula):
|
| 35 |
-
try:
|
| 36 |
-
# 配置LaTeX渲染参数
|
| 37 |
-
plt.rcParams.update({
|
| 38 |
-
"text.usetex": True, # 启用LaTeX渲染
|
| 39 |
-
"font.family": "serif", # 使用衬线字体
|
| 40 |
-
"font.serif": ["Computer Modern"], # LaTeX默认字体
|
| 41 |
-
"axes.labelsize": 24, # 保持字体大小一致
|
| 42 |
-
})
|
| 43 |
-
|
| 44 |
-
# 创建图像
|
| 45 |
-
fig = plt.figure()
|
| 46 |
-
plt.axis("off")
|
| 47 |
-
|
| 48 |
-
# 使用LaTeX渲染公式(添加$符号包裹公式)
|
| 49 |
-
plt.text(0.5, 0.5, f"${remove1(formula)}$",
|
| 50 |
-
ha="center",
|
| 51 |
-
va="center",
|
| 52 |
-
fontsize=24,
|
| 53 |
-
math_fontfamily='cm') # 明确指定数学字体
|
| 54 |
-
|
| 55 |
-
# 保存到内存缓冲区
|
| 56 |
-
buf = io.BytesIO()
|
| 57 |
-
plt.savefig(buf, format="png", bbox_inches="tight", pad_inches=0.1, dpi=300)
|
| 58 |
-
plt.close(fig)
|
| 59 |
-
buf.seek(0)
|
| 60 |
-
return Image.open(buf)
|
| 61 |
-
except Exception as e:
|
| 62 |
-
# 出错时使用简单文本提示
|
| 63 |
-
return show_latex(r"\text{Sorry, LaTeX rendering failed. Please check your formula syntax.}")
|
| 64 |
-
|
| 65 |
def search(query,enable_latex):
|
| 66 |
output_results = output_collection.get(
|
| 67 |
where={"$or": [{"tag": query}, {"label": query}]},
|
|
@@ -105,7 +74,6 @@ def search(query,enable_latex):
|
|
| 105 |
</div>
|
| 106 |
</div>
|
| 107 |
"""
|
| 108 |
-
latex_image = show_latex("\n \n"+remove1(latex)) if enable_latex else None
|
| 109 |
answer = '<div style="padding: 10px;">'
|
| 110 |
for l in range(10):
|
| 111 |
kind = output_results["metadatas"][0][str(l)+'kind'].strip()
|
|
@@ -175,33 +143,25 @@ def search(query,enable_latex):
|
|
| 175 |
"""
|
| 176 |
answer += '</div>'
|
| 177 |
|
| 178 |
-
return [latex_output,
|
| 179 |
|
| 180 |
with gr.Blocks(theme=gr.themes.Soft(), title="Stack-Mathlib4 Search") as demo:
|
| 181 |
gr.Markdown("""<center><font size=8> Stack-Mathlib4 Search</font></center>""")
|
| 182 |
|
| 183 |
with gr.Tab("Theorem Search"):
|
| 184 |
-
|
| 185 |
-
|
| 186 |
-
|
| 187 |
-
label="Please enter a label or a tag"
|
| 188 |
-
)
|
| 189 |
-
search_button = gr.Button("Search", variant="primary")
|
| 190 |
-
|
| 191 |
-
enable_switch = gr.Checkbox(
|
| 192 |
-
label="LaTeX Rendering",
|
| 193 |
-
value=True,
|
| 194 |
-
info="Toggle LaTeX formula display"
|
| 195 |
)
|
|
|
|
| 196 |
|
| 197 |
information = gr.HTML(label="Information of the Theorem", elem_classes="result-box")
|
| 198 |
-
latex_2 = gr.Image(label="LaTeX Rendering", interactive=False)
|
| 199 |
answer = gr.HTML(label="Top Matching Theorems", elem_classes="result-box")
|
| 200 |
|
| 201 |
search_button.click(
|
| 202 |
fn=search,
|
| 203 |
-
inputs=[label_input
|
| 204 |
-
outputs=[information,
|
| 205 |
)
|
| 206 |
|
| 207 |
demo.launch(share=True)
|
|
|
|
| 31 |
"text.latex.preamble": r"\usepackage{amsmath,amssymb}"
|
| 32 |
})
|
| 33 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 34 |
def search(query,enable_latex):
|
| 35 |
output_results = output_collection.get(
|
| 36 |
where={"$or": [{"tag": query}, {"label": query}]},
|
|
|
|
| 74 |
</div>
|
| 75 |
</div>
|
| 76 |
"""
|
|
|
|
| 77 |
answer = '<div style="padding: 10px;">'
|
| 78 |
for l in range(10):
|
| 79 |
kind = output_results["metadatas"][0][str(l)+'kind'].strip()
|
|
|
|
| 143 |
"""
|
| 144 |
answer += '</div>'
|
| 145 |
|
| 146 |
+
return [latex_output,answer]
|
| 147 |
|
| 148 |
with gr.Blocks(theme=gr.themes.Soft(), title="Stack-Mathlib4 Search") as demo:
|
| 149 |
gr.Markdown("""<center><font size=8> Stack-Mathlib4 Search</font></center>""")
|
| 150 |
|
| 151 |
with gr.Tab("Theorem Search"):
|
| 152 |
+
label_input = gr.Textbox(
|
| 153 |
+
placeholder="",
|
| 154 |
+
label="Please enter a label or a tag"
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 155 |
)
|
| 156 |
+
search_button = gr.Button("Search", variant="primary")
|
| 157 |
|
| 158 |
information = gr.HTML(label="Information of the Theorem", elem_classes="result-box")
|
|
|
|
| 159 |
answer = gr.HTML(label="Top Matching Theorems", elem_classes="result-box")
|
| 160 |
|
| 161 |
search_button.click(
|
| 162 |
fn=search,
|
| 163 |
+
inputs=[label_input],
|
| 164 |
+
outputs=[information, answer]
|
| 165 |
)
|
| 166 |
|
| 167 |
demo.launch(share=True)
|