# Claude Code 启动提示词

历史文件：用户已撤回Claude Code交接，明确改为Codex自主实现、发布与验收。下面仅保存当时模板与提示词来源，当前执行请读PROJECT.md/PROGRESS.md/CLAUDE.md；不可用旧模板覆盖已实现源码或撤销最新授权。

**历史权限说明：** 下方是原文档阶段模板，未启动Claude。最新用户已明确授权本项目本地实现及公开GitHub、CI、Mooncakes和网站交付，无需重复确认。

```text
你将接手一个新的MoonBit项目：MoonBit原生Metamath证明验证与逐步执行库，附CLI和网页证明实验器。请先读下面的本地资料，不要要求我重新解释聊天历史，也不要重新发散选题。

当前日期请按实际Asia/Shanghai读取；资料包日期2026-10-23。官网目前写十月31日截止，但官网链接的飞书章程有24日和九月旧日期；保留冲突，依据我提供的官方通知更新，不擅自声称资格已确认。

资料目录：
D:\Study_Works\MoonBit\moonmetamath

按顺序读取：
1. CLAUDE.md、PROJECT.md、PROGRESS.md
2. README.md、DESIGN_AND_SCOPE.md
3. REFERENCES.md
4. IMPLEMENTATION_PLAN.md
5. ACCEPTANCE.md

实施目录：D:\Study_Works\MoonBit\moonmetamath；当前已准备规划与交接文档，尚无实现代码或独立Git。
父目录是已有MoonFlowGraph仓库；moonportcheck、moontrack、moonsplit是已有项目。先确认目标目录状态，不覆盖已有内容，不修改这些旧项目的业务、分支、配置或未跟踪文件。

当我亲自发送本启动提示时，本次授权你在已准备的实施目录内创建必要源码/文档/测试/脚本，增量维护已有PROJECT.md、CLAUDE.md和PROGRESS.md，不覆盖规划资料；运行本地构建和测试，取得计划列明的公开参考资料及固定工具链到项目独立缓存。允许在该目录初始化独立Git仓库，并在真实任务完成后作有意义的本地阶段提交；默认分支codex/metamath-v0.1。禁止在父仓库批量git add，禁止补造/空拆提交。参考材料只读、许可清楚。

不授权：创建远程仓库、push、PR/合并、Mooncakes正式发布、部署、报名、对外发消息或邀请试用者、修改全局工具链/模型provider、启动后台循环/定时任务、批量删除。先把上述事项必要的本地准备做成可审查成果，再一次性列清需要我批准的具体操作。没有外部授权不能因此停止本地核心、测试和文档的已授权工作。

目标不是完整Lean，也不是训练自动证明模型。核心必须由MoonBit执行，Python的mmverify.py、C/Rust检查器只作测试参考。主要移植来源是MIT的mmverify.py，版本与许可在REFERENCES固定。Metamath规范高于参考实现；尤其不能直接照搬其$f/$e顺序限制。

工具链注意：本机全局moonc仍是v0.10.3。已核实的隔离v0.10.14工具在
D:\Study_Works\MoonBit\moonportcheck\.toolchains\windows-x86_64
可以只读检查和使用，不能改动旧项目；新项目建立自己的工具链入口。固定版本、官方归档及哈希见REFERENCES。不能悄悄升级全局或回退latest。Node要求24。Python仅测试使用，先检查实际可用版本，不安装无关环境。

请从T0按任务依赖持续执行到本地可交付版本，不把搭好目录、发出subagent、完成一个回合或写好计划当作完成。每个必要任务通过后主动推进下一项；遇到失败先核实固定版本源码和最小反例，在授权内修复。独立工作可以并行，核心接口/同一源码文件只有一个写者；T5、T7、最终交付安排独立review，处理有依据的问题，不无限复审。

核心范围：
- .mm标准ASCII输入、声明、作用域、文件包含、普通和压缩证明；
- 同时代换、类型码、mandatory hypotheses声明顺序、合法空代换、$d条件；
- parse/verify/可应用定理三个层次分开；不能使用未验证$p、目标自身、未来定理或非活动假设；活动$f/$e和显式$a按规范合法使用；
- 同一执行器服务普通/压缩/交互；错误单步原子失败；
- start/apply/inspect/rewind/finish，只有单项且等于目标才完成；
- 仅从ApplyLabel构造的完成会话导出普通.mm，使用目标前缀和原上下文；压缩replay首版不直接导出，不伪造缺失的推导；
- Node CLI和实际可操作网页；网页长同步调用放Worker，取消使用terminate并标未完成，重新开始重建上下文；
- schema1、退出码和资源限额按规格实现，不把未完成/取消/超限当成功。

参考材料：固定demo0.mm、miu.mm、peano.mm、hol.mm为十月目标，完整set.mm约52MB是增强项。使用外部正反例和独立checker；对照必须真正在验证证明，不能只看文件读入或日志里一句verified。导出的候选必须由C/Rust至少一个独立checker接受。缺工具先记录并继续独立可做项，不得假称通过。

开始后48小时执行G0：普通/压缩共用语义、真实小库、关键反例、JS运行和独立差异均可解释。若仍接受错误证明或只能依赖Python运行，优先修复，明确撤回无法兑现的十月承诺；不放宽$d、scope或最终目标条件。可选AI、视觉细节、大库性能可以延后，must不能无声降级。

复现入口须实现为run_check.ps1/.sh、run_demo.ps1/.sh、run_acceptance.ps1/.sh以及文档约定的Node脚本。执行并保存实际日志、输入版本、检查范围和未完成项，不把计划命令写成已运行。local验收通过不等于远端CI、registry发布或赛事审核通过。

进度只维护新项目PROGRESS.md作为权威入口，PROJECT.md保存长期背景和复现入口。每单元写完成内容、依据、命令/输出、限制、下一单元与责任者；临时失败不覆盖原记录。会话需要交接时，写清当前未完成目标、恢复命令和下一项，不让我反复催“继续”。当前不授权后台调度；使用你已有的前台原生执行方式即可。

十月初审材料要尽早准备，不等到29日。至少三场景和十个有效提交来自真实工程。官方要求人工撰写的一页申报正文由我亲自定稿，你负责提供事实、来源、可运行证据和结构。没有真实试用不能写已有用户，没有实际模型调用不能把预置回放称为AI自主证明。

完成时交付：
1. 新项目可运行源码、MIT/参考许可、固定版本和真实兼容范围；
2. 核心/CLI/网页/导出/独立消费者实际验收结果，PASS/FAIL/PENDING分开；
3. G0-G4本地候选包与实际日志、未完成项和风险；
4. 待授权的公开仓库、push/CI、Mooncakes发布、部署及报名操作清单；
5. 长期下一阶段建议，以真实接入和兼容证据为依据，不擅自扩展成通用Agent平台。

先简短报告你读到的当前目录/工具链状态和将执行的第一单元，然后直接在上述授权内推进，无需再次询问是否开始本地实施。
```

## 用户只想先做G0时的替换句

将“持续执行到本地可交付版本”替换为：“本次只授权执行T0–T5并完成G0，交付真实结果后停止；其余任务保留规划，不擅自继续。”其余权限与真实性约束保持。

## 跨会话恢复用一句话

```text
继续D:\Study_Works\MoonBit\moonmetamath：先读PROJECT.md和唯一PROGRESS.md，再定位本交接包的对应任务。核实未完成目标、上次命令/产物、实际失败与授权边界，从下一项必要工作继续；不重开实验、不重写已通过模块，不将部分门槛当整项目完成。
```