返回首页
最新
我希望在使用 Copilot 时，无论是 Copilot CLI、Copilot App 还是 IDE 中的 Copilot，都能有一致的体验，但目前这并不可能。例如，CLI 中方便的 `/review` 命令在 App 中并不可用。虽然 App 友好且对话性强，但无法像 IDE 中的 Copilot 那样进行代码导航。IDE 中的 Copilot 效果很好，但缺少其他两个版本的一些功能。
你是如何使用 Copilot 的？你使用哪些产品？尤其是那些声称几个月没有写代码的人。
几十年来，我一直担心互联网的构建主要围绕非虚构作品，因此我创建了一些东西，以展示我们如何在网络上庆祝优秀的虚构作品。<p>我从一个精彩的公共领域图书馆开始，并添加了工具，让大家可以分享自己的故事。<p>非常期待听到任何反馈，也希望你能分享一些好书！
据我所知，这是首个经过正式验证的三维构造实体几何（CSG）操作实现：网格交集，使用Lean 4实现，并根据简明的规范进行了验证，该规范准确地确定了生成网格的表面，并保证了三角剖分的实际良构性条件。
该项目也是一个避免依赖AI生成代码的实验。人类审阅者只需阅读93行正式规范，并运行Lean检查器来认证内核的正确性，从而跳过复杂的1000多行AI编写的实现代码。为了证明正确性，AI自主编写了超过60,000行的Lean证明，这些证明也无需人类检查。Lean检查器在编译时保证符合规范，对任何大型语言模型（LLM）没有任何信任。这使我们能够将实现和证明视为一个黑箱。我引导代理通过readme中描述的里程碑，达成了这里展示的结果。
同时，请查看网页演示 <a href="https://schildep.github.io/verified-3d-mesh-intersection/" rel="nofollow">https://schildep.github.io/verified-3d-mesh-intersection/</a>，该演示在您的浏览器中运行经过验证的网格交集内核，已编译为WebAssembly。
嗨，HN——我们创建了 `dn`，因为编码的速度加快了，但软件构建的速度却没有。使用命令行界面（CLI）通过可重用的代理工作流和其他支持命令更快地清理你的待办事项。你或你的代理可以使用 kickstart、meld、loop、land、fixup 等命令将 Markdown 规范转化为实现。在 GitHub Actions 中使用 CLI，可以在夜间持久地交接团队在早上处理的拉取请求和 GitHub 问题。
例如：
```sh
dn --agent codex kickstart --awp \
<a href="https://github.com/owner/repo/issues/123" rel="nofollow">https://github.com/owner/repo/issues/123</a>
```
`dn` 会读取问题和仓库说明，在 `plans/` 下写入一个命名的 Markdown 计划，要求选定的编码代理进行实现，并跟踪验收标准。在 AWP 模式下，它会创建一个分支，提交，推送，并打开拉取请求。
你可以为你的代理安装 `dn` 技能。我们目前支持 OpenCode、Claude Code、Cursor、Copilot 和 Codex。你与代理的对话仅限于你的机器。`dn` 技能帮助将这些上下文记录在 GitHub 问题和你的 git 仓库中，作为文件系统上下文。当你的团队和他们使用的代理共享上下文时，生产力会成倍增加。
最新版本增加了 Docker 和 exe.dev 沙箱以供代理运行、远程进度报告，以及更清晰的 `meld` → `loop` → `land` 工作流，以便在多个会话和开发者之间拆分工作。我们非常希望收到你的反馈，以使 `dn` 成为更好的产品，现在还处于早期阶段！
我们还创建了 <a href="https://denoise.cloud" rel="nofollow">https://denoise.cloud</a>，以便产品经理可以与 `dn` 用户并肩工作。使用 denoise 可以简化软件开发生命周期，为你的团队解锁巨大的生产力提升！我们的赌注是，小团队不需要更多的仪表板或另一个专有代理。他们需要人类判断与机器执行之间更清晰的界限。
在这里查看 denoise 的实际应用：<a href="https://x.com/DenoiseCloud/status/2078607769259721016" rel="nofollow">https://x.com/DenoiseCloud/status/2078607769259721016</a>