Hugging Face
Models
Datasets
Spaces
Buckets
new
Docs
Enterprise
Pricing
Log In
Sign Up
Spaces:
xcz0
/
lean4-eval-pipeline
like
0
Sleeping
App
Files
Files
Community
Fetching metadata from the HF Docker repository...
main
lean4-eval-pipeline
Commit History
增强 LLM 客户端功能,支持多种推理提供方和错误处理,优化生成 Lean 代码的调用逻辑
965cabb
xcz0
commited on
Dec 22, 2025
重构生成 Lean 代码的逻辑,增加提取计划和代码块的功能,并优化错误处理
c82ffa7
xcz0
commited on
Dec 20, 2025
优化 LLM 客户端配置,修正生成 Lean 代码的调用方式
ba8d406
xcz0
commited on
Dec 20, 2025
调整 mathlib 预编译缓存下载和构建顺序
83272ff
xcz0
commited on
Dec 20, 2025
修正 Lean 项目初始化及 REPL 路径
cef2210
xcz0
commited on
Dec 20, 2025
优化 Dockerfile 和 app.py,修正 Lean 依赖构建命令及 REPL 执行路径
3807c9d
xcz0
commited on
Dec 20, 2025
更新 Dockerfile,移除 lakefile.lean 并统一使用 TOML 配置依赖
2342b0d
xcz0
commited on
Dec 20, 2025
优化 Dockerfile,修复 Python 依赖安装方式并调整系统依赖
0ac0929
xcz0
commited on
Dec 20, 2025
优化 Dockerfile,调整 lean4-repl 工具的构建方式并添加 .dockerignore 文件
98593a4
xcz0
commited on
Dec 20, 2025
修复 Dockerfile 中的 COPY 命令格式错误
d00a1db
xcz0
commited on
Dec 20, 2025
Initial deployment of Lean4 evaluation pipeline
1b458f7
xcz0
commited on
Dec 20, 2025
initial commit
dcbd781
verified
xcz0
commited on
Dec 20, 2025