Lean 4 也有 HTTP 客户端了:libcurl 驱动的 LeanHttp
hargup13 · x · 2026-09-07
theoriclabs 开源了 LeanHttp,一个 Lean 4 的同步/异步 HTTP 客户端,通过小型 C FFI 调用 libcurl。API 复用 Std.Http 的已验证方法、URI、header 与状态类型;HTTP 错误状态作为普通响应返回,传输失败则有类型化、稳定的错误类别。会话复用单个 libcurl easy handle 以保持连接,支持超时、限制响应体大小、重定向与 TLS 策略。通过 lakefile 的 git 依赖即可引入,当前版本 v0.3.1。
「编程与Agent」频道最新
- 用 1024 字节 C 代码写出 Python 解释器：递归下降解析器的极限挑战 — AustinZHenley · 2026-09-07
- OpenAI 事件后 AI 智能体自建共享记忆,HAIDAA 尝试规范化 — WrongTechnician · 2026-09-07
- 独立开发者的本地 LLM RPG:模型只演 NPC,游戏状态完全确定性 — Rikkendo · 2026-09-07
- 开发者把 Codex 与 Claude 接进同一频道互相协作,Pro 版将收费 — jasonkneen · 2026-09-07
- 用便宜模型盯着 Agent 转录，能否提前拦截越狱事故 — rhaivn · 2026-09-07
- 微软上交大开源 Argus：让 Agent 连续自主研究数天的运行时 — 机器之心 · 2026-09-07