Create gui.py

gui.py

@@ -0,0 +1,194 @@
+import chromadb
+import gradio as gr
+import matplotlib.pyplot as plt
+import io
+from PIL import Image
+import re
+
+# 初始化集合
+client = chromadb.PersistentClient(path="chroma_db2")
+output_collection = client.get_collection("data_collection")
+
+def remove1(latex_str):
+    # 定义需要移除的命令的正则表达式
+    unsupported_commands = [
+        r'\\ref\{([^}]+)\}',  # 匹配 \ref{...}，保留括号内容
+        r'\\label\{([^}]+)\}',  # 匹配 \label{...}，保留括号内容
+        r'\\Ob\(([^)]+)\)',
+    ]
+    latex_str=latex_str.replace("\\\\","\\")
+    # 逐个移除不支持的命令
+    for pattern in unsupported_commands:
+        latex_str = re.sub(pattern, r'\1', latex_str)
+
+    return latex_str
+
+plt.rcParams.update({
+    "text.usetex": True,
+    "font.family": "serif",
+    "axes.spines.right": False,
+    "axes.spines.top": False,
+    "text.latex.preamble": r"\usepackage{amsmath,amssymb}"
+})
+
+def show_latex(formula):
+    try:
+        # 创建图像
+        fig = plt.figure()
+        plt.axis("off")
+        plt.text(0.5, 0.5, "\n \n"+f"{remove1(formula)}", 
+                 ha="center", va="center", 
+                 fontsize=24)
+
+        # 保存到内存缓冲区
+        buf = io.BytesIO()
+        plt.savefig(buf, format="png", bbox_inches="tight", dpi=150)
+        plt.close(fig)
+        buf.seek(0)
+        return Image.open(buf)
+    except Exception as e:
+        return show_latex("Sorry, due to the incompatibility of some LaTeX expressions, rendering errors occurred.")
+
+def search(query,enable_latex):
+    output_results = output_collection.get(
+        where={"$or": [{"tag": query}, {"label": query}]},
+        limit=1
+    )
+    
+    if not output_results["ids"]:
+        return ["No matching results found",None,'']
+    
+    # 获取匹配的output信息
+    tag= output_results["metadatas"][0]["tag"]
+    label= output_results["metadatas"][0]["label"]
+    latex= output_results["documents"][0]
+    latex_output = f"""
+    <div style="margin-bottom: 25px; padding: 15px; border: 1px solid #e0e0e0; border-radius: 8px;">
+        <div style="margin: 15px 0;">
+                <p style="font-size: 1.1em; margin: 8px 0;">
+                    <strong>✍ Tag:</strong> {tag}
+                </p>
+                <p style="font-size: 1.1em; margin: 8px 0;">
+                    <strong>💬 Label:</strong> {label}
+                </p>
+                <p style="font-size: 1.1em; margin: 8px 0; color: #e67e22;">
+                    <strong>⭐ LaTeX:</strong> {latex}
+                </p>
+        </div>
+        <div style="text-align: center; margin-top: 20px;">
+            <a href="https://stacks.math.columbia.edu/tag/{tag}" 
+                target="_blank" 
+                style="display: inline-block;
+                    background: #3498db;
+                    color: white !important;
+                    padding: 12px 25px;
+                    border-radius: 5px;
+                    text-decoration: none;
+                    font-size: 1.1em;
+                    transition: all 0.3s ease;
+                    box-shadow: 0 2px 5px rgba(0,0,0,0.1);">
+                📖 Proceed To The Docs Link
+            </a>
+        </div>
+    </div>
+    """
+    latex_image = show_latex("\n \n"+remove1(latex)) if enable_latex else None
+    answer = '<div style="padding: 10px;">'
+    for l in range(10):
+        kind = output_results["metadatas"][0][str(l)+'kind'].strip()
+        fn = output_results["metadatas"][0][str(l)+'formal name'].strip("'")
+        fs = output_results["metadatas"][0][str(l)+'formal statement']
+        inn = output_results["metadatas"][0][str(l)+'informal name'].strip("'")
+        ins = output_results["metadatas"][0][str(l)+'informal statement']
+    
+        answer += f"""
+        <div style="margin-bottom: 25px; padding: 15px; border: 1px solid #e0e0e0; border-radius: 8px;">
+            <!-- 放大并居中的formal name -->
+            <div style="text-align: center; margin: 15px 0;">
+                <h2 style="font-size: 1.8em; color: #2c3e50; 
+                         margin: 0;
+                          padding-bottom: 10px;
+                          border-bottom: 3px solid #3498db;
+                          display: inline-block;">
+                    {fn}
+                </h2>
+            </div>
+
+            <!-- 强调的formal statement -->
+            <div style="background: #f8f9fa;
+                       padding: 15px;
+                       border-radius: 6px;
+                       margin: 15px 0;
+                       border-left: 4px solid #3498db;">
+                <p style="font-size: 1.2em; line-height: 1.6; color: #2c3e50; margin: 0;font-family: 'Courier New', Consolas, Monaco, monospace;">
+                    <strong style="font-size: 1.1em; color: #3498db;">📜 Formal Statement:</strong><br>
+                    {fs}
+                </p>
+            </div>
+
+            <!-- 其他信息 -->
+            <div style="margin: 15px 0;">
+                <p style="font-size: 1.1em; margin: 8px 0;">
+                    <strong>⭐ Kind:</strong> {kind}
+                </p>
+                <p style="font-size: 1.1em; margin: 8px 0;">
+                    <strong>✍ Informal Name:</strong> {inn}
+                </p>
+                <p style="font-size: 1.1em; margin: 8px 0;">
+                    <strong>💬 Informal Statement:</strong> {ins}
+                </p>
+                <p style="font-size: 1.1em; margin: 8px 0; color: #e67e22;">
+                    <strong>✌ Similarity Ranking:</strong> {l+1}
+                </p>
+            </div>
+
+            <!-- 文档链接 -->
+            <div style="text-align: center; margin-top: 20px;">
+                <a href="https://leanprover-community.github.io/mathlib4_docs/find/?pattern={fn}#doc" 
+                   target="_blank" 
+                   style="display: inline-block;
+                         background: #3498db;
+                          color: white !important;
+                          padding: 12px 25px;
+                          border-radius: 5px;
+                          text-decoration: none;
+                          font-size: 1.1em;
+                          transition: all 0.3s ease;
+                          box-shadow: 0 2px 5px rgba(0,0,0,0.1);">
+                    📖 View Full Documentation
+                </a>
+            </div>
+        </div>
+        """
+    answer += '</div>'
+    
+    return [latex_output,latex_image,answer]
+
+with gr.Blocks(theme=gr.themes.Soft(), title="Stack-Mathlib4 Search") as demo:
+    gr.Markdown("""<center><font size=8> Stack-Mathlib4 Search</font></center>""")
+        
+    with gr.Tab("Theorem Search"):
+        with gr.Row():
+            label_input = gr.Textbox(
+                placeholder="", 
+                label="Please enter a label or a tag"
+            )
+            search_button = gr.Button("Search", variant="primary")
+        
+        enable_switch = gr.Checkbox(
+            label="LaTeX Rendering", 
+            value=True,
+            info="Toggle LaTeX formula display"
+        )
+        
+        information = gr.HTML(label="Information of the Theorem", elem_classes="result-box")
+        latex_2 = gr.Image(label="LaTeX Rendering", interactive=False)
+        answer = gr.HTML(label="Top Matching Theorems", elem_classes="result-box")
+
+        search_button.click(
+            fn=search,
+            inputs=[label_input, enable_switch],
+            outputs=[information, latex_2, answer]
+        )
+
+demo.launch(share=True)