Upload 3 files

app.py

@@ -0,0 +1,202 @@
+import gradio as gr
+import requests
+import json
+import time
+import os
+
+# 配置
+KIMINA_SERVER_URL = "http://localhost:8000"
+HEALTH_CHECK_INTERVAL = 2  # 秒
+MAX_WAIT_TIME = 30  # 秒
+
+
+def check_server_health():
+    """检查 Kimina 服务器是否就绪"""
+    try:
+        response = requests.get(f"{KIMINA_SERVER_URL}/health", timeout=5)
+        return response.status_code == 200
+    except:
+        return False
+
+
+def wait_for_server():
+    """等待服务器启动"""
+    print("等待 Kimina 服务器启动...")
+    start_time = time.time()
+
+    while time.time() - start_time < MAX_WAIT_TIME:
+        if check_server_health():
+            print("Kimina 服务器已就绪！")
+            return True
+        print(f"服务器尚未就绪，等待 {HEALTH_CHECK_INTERVAL} 秒...")
+        time.sleep(HEALTH_CHECK_INTERVAL)
+
+    print(f"等待超时 ({MAX_WAIT_TIME} 秒)")
+    return False
+
+
+def verify_lean_code(code, infotree_type="original"):
+    """验证 Lean 代码"""
+    if not wait_for_server():
+        return "❌ 错误：Kimina 服务器未启动"
+
+    try:
+        payload = {
+            "codes": [{
+                "custom_id": "user_input",
+                "proof": code
+            }],
+            "infotree_type": infotree_type
+        }
+
+        response = requests.post(
+            f"{KIMINA_SERVER_URL}/verify",
+            json=payload,
+            timeout=30
+        )
+
+        if response.status_code == 200:
+            result = response.json()
+            if "results" in result and result["results"]:
+                item = result["results"][0]
+
+                if item["type"] == "success":
+                    return f"✅ 验证成功！\n\n输出：{item.get('message', '无输出')}"
+                elif item["type"] == "error":
+                    return f"❌ 验证失败：\n\n错误信息：{item.get('message', '未知错误')}"
+                else:
+                    return f"⚠️ 未知结果类型：{item}"
+            else:
+                return "❌ 错误：服务器返回无效响应"
+        else:
+            return f"❌ 服务器错误 (状态码：{response.status_code}): {response.text}"
+
+    except requests.exceptions.Timeout:
+        return "❌ 错误：请求超时，代码可能太复杂或服务器繁忙"
+    except requests.exceptions.ConnectionError:
+        return "❌ 错误：无法连接到 Kimina 服务器"
+    except Exception as e:
+        return f"❌ 错误：{str(e)}"
+
+
+def create_demo():
+    """创建 Gradio 界面"""
+
+    # 等待服务器启动（在后台进行）
+    import threading
+    def wait_in_background():
+        wait_for_server()
+
+    thread = threading.Thread(target=wait_in_background, daemon=True)
+    thread.start()
+
+    with gr.Blocks(title="Kimina Lean Server", theme=gr.themes.Soft()) as demo:
+        gr.Markdown("""
+        # ⚡ Kimina Lean Server
+        在线验证 Lean 4 代码
+
+        ## 使用示例
+        ```lean
+        #check Nat
+        theorem test : 1 + 1 = 2 := by native_decide
+        example : 2 + 2 = 4 := by native_decide
+        ```
+        """)
+
+        with gr.Row():
+            with gr.Column(scale=3):
+                code_input = gr.Code(
+                    label="Lean 4 代码",
+                    value="#check Nat\ntheorem test : 1 + 1 = 2 := by native_decide",
+                    language="python",
+                    lines=10,
+                    interactive=True
+                )
+
+                infotree_type = gr.Radio(
+                    choices=["original", "compressed"],
+                    value="original",
+                    label="信息树类型",
+                    info="选择返回的信息树格式"
+                )
+
+                submit_btn = gr.Button("验证代码", variant="primary", size="lg")
+
+            with gr.Column(scale=2):
+                output = gr.Textbox(
+                    label="验证结果",
+                    lines=15,
+                    interactive=False
+                )
+
+                examples = gr.Examples(
+                    examples=[
+                        ["#check Nat", "original"],
+                        ["theorem test : 1 + 1 = 2 := by native_decide", "original"],
+                        ["example : True := by trivial", "original"],
+                        ["#eval List.range 5", "original"],
+                        ["""theorem add_comm (a b : Nat) : a + b = b + a := by
+  induction a with
+  | zero => simp
+  | succ a ih => simp [Nat.succ_add, ih]""", "compressed"]
+                    ],
+                    inputs=[code_input, infotree_type],
+                    label="示例代码"
+                )
+
+        # 状态指示器
+        status = gr.Textbox(
+            value="🟡 正在启动 Kimina 服务器...",
+            label="服务器状态",
+            interactive=False
+        )
+
+        # 绑定事件
+        submit_btn.click(
+            fn=verify_lean_code,
+            inputs=[code_input, infotree_type],
+            outputs=output
+        )
+
+        # 自动更新状态
+        def update_status():
+            if check_server_health():
+                return "🟢 Kimina 服务器已就绪"
+            else:
+                return "🔴 Kimina 服务器未就绪"
+
+        demo.load(
+            fn=update_status,
+            outputs=status,
+            every=5  # 每5秒更新一次
+        )
+
+        gr.Markdown("""
+        ## 特性说明
+
+        1. **并行验证**：支持同时验证多个代码片段
+        2. **错误报告**：详细的错误信息和位置
+        3. **mathlib4 支持**：内置完整的 mathlib4 库
+        4. **高性能**：优化的 REPL 管理和内存控制
+
+        ## 支持的 Lean 功能
+
+        - 定理证明
+        - 定义检查
+        - 类型检查
+        - 求值 (#eval)
+        - 元编程
+        """)
+
+    return demo
+
+
+if __name__ == "__main__":
+    # 在 Gradio 中启动应用
+    demo = create_demo()
+    demo.launch(
+        server_name="0.0.0.0",
+        server_port=7860,
+        share=False,
+        debug=True
+    )

requirements.txt

@@ -0,0 +1,15 @@
+# Kimina 客户端
+kimina-client>=0.2.0
+
+# Gradio 前端
+gradio>=4.0.0
+
+# FastAPI 和依赖
+fastapi>=0.104.0
+uvicorn[standard]>=0.24.0
+httpx>=0.25.0
+
+# 其他工具
+structlog>=23.0.0
+pydantic>=2.0.0
+websockets>=12.0

start.sh

@@ -0,0 +1,34 @@
+#!/bin/bash
+set -e
+
+echo "🚀 启动 Kimina Lean Server 空间..."
+
+# 设置环境变量
+export LEAN_SERVER_REPL_PATH="/home/user/repl/.lake/build/bin/repl"
+export LEAN_SERVER_PROJECT_DIR="/home/user/mathlib4"
+
+# 启动 Kimina 服务器（后台运行）
+echo "启动 Kimina Lean Server..."
+python -m server &
+KIMINA_PID=$!
+
+# 等待服务器启动
+echo "等待 Kimina 服务器启动..."
+sleep 10
+
+# 检查服务器是否运行
+if ps -p $KIMINA_PID > /dev/null; then
+    echo "✅ Kimina 服务器已启动 (PID: $KIMINA_PID)"
+else
+    echo "❌ Kimina 服务器启动失败"
+    exit 1
+fi
+
+# 启动 Gradio 前端
+echo "启动 Gradio 前端界面..."
+python app.py
+
+# 清理（如果前端退出）
+echo "正在关闭 Kimina 服务器..."
+kill $KIMINA_PID
+wait $KIMINA_PID