From 3fa6a5a5a5adab4322792c9ad1bf3bea20365d71 Mon Sep 17 00:00:00 2001 From: sjfhsjfh Date: Sun, 12 Jul 2026 18:55:52 +0800 Subject: [PATCH] fix(spec): replace @Claude with @bot in Prelude and Run --- spec/Spec/Prelude.lean | 2 +- spec/Spec/System/Agent/Run.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/Spec/Prelude.lean b/spec/Spec/Prelude.lean index 85342b3..4439d4d 100644 --- a/spec/Spec/Prelude.lean +++ b/spec/Spec/Prelude.lean @@ -30,7 +30,7 @@ structure Identifiers where /-- Project explorer folder 标识(`OPEN` 表示;ADR-0021 透明组织节点,非权限资源)。 -/ FolderId : Type /-- 一次 agent 任务的标识(`OPEN` 表示;锁的 owner、审计主体,`AgentRun`。provider 无关, - ADR-0017;`@Claude` 仅为触发品牌,不承诺 provider)。 -/ + ADR-0017;`@bot` 仅为触发品牌,不承诺 provider)。 -/ RunId : Type /-- 长生命周期 agent 会话标识(`OPEN` 表示;**provider/model 绑定, ADR-0017**——一次 session 不跨 provider/model;切 model 即新 session,跨 session 连续性由 ADR-0003 项目 diff --git a/spec/Spec/System/Agent/Run.lean b/spec/Spec/System/Agent/Run.lean index 4ecbd7d..5bcb865 100644 --- a/spec/Spec/System/Agent/Run.lean +++ b/spec/Spec/System/Agent/Run.lean @@ -1,7 +1,7 @@ /-! # Run —— AgentRun 状态机 -一次 `@Claude` 创建一个 `AgentRun`(ADR-0001),它在终止时释放项目锁(ADR-0002)。 +一次 `@bot` 创建一个 `AgentRun`(ADR-0001),它在终止时释放项目锁(ADR-0002)。 合法转移关系在任何 ADR / likec4 散文里都未定下,故本模块只刻画**状态**与**终止 判定**(后者是 Lock 排他不变式的依赖),不臆造转移边。 -/