forked from bai/curriculum-project-hub
61 lines
1.9 KiB
Lean4
61 lines
1.9 KiB
Lean4
import Spec.Prelude
|
|
|
|
/-!
|
|
# AgentRole —— Agent 角色与技能配置 (ADR-0017, ADR-0018)
|
|
|
|
AgentRole 是 org-scoped 运行时配置:system prompt、tool allowlist、default model
|
|
和 skill 绑定。通过 CLI 管理,不需重启进程生效。
|
|
|
|
Role 的执行面(model/prompt/tools/skill 内容)变更时,该 role 的 active sessions
|
|
归档——下次 run 不能在旧指令下创建的 provider context 上恢复。
|
|
仅 label/排序变更不影响会话连续性(ADR-0017)。
|
|
|
|
Run 时只读加载 role 选中的 skill 不可变版本到 run-scoped 目录,
|
|
run 结束后删除(ADR-0018)。Skill 管理是 org-scoped;存储机制 `OPEN`。
|
|
-/
|
|
|
|
namespace Spec.System
|
|
|
|
variable (I : Identifiers)
|
|
|
|
/-- Agent 角色(`PINNED`, org-scoped, ADR-0017)。 -/
|
|
structure AgentRole where
|
|
/-- 所属组织(`PINNED`)。 -/
|
|
organization : I.OrganizationId
|
|
/-- 斜杠命令名(`OPEN` 表示;如 /draft)。 -/
|
|
roleId : String
|
|
/-- system prompt(`PINNED`)。 -/
|
|
systemPrompt : String
|
|
/-- tool allowlist(`PINNED`;tool 标识集合 `OPEN`)。 -/
|
|
tools : List String
|
|
/-- 默认 model(`PINNED`;model ID 表示 `OPEN`)。 -/
|
|
defaultModel : String
|
|
|
|
/-- Agent 技能(`PINNED`, org-scoped, ADR-0017/0018)。 -/
|
|
structure AgentSkill where
|
|
/-- 所属组织(`PINNED`)。 -/
|
|
organization : I.OrganizationId
|
|
/-- 名称(`PINNED`)。 -/
|
|
name : String
|
|
/-- 版本(`PINNED`)。 -/
|
|
version : String
|
|
/-- 内容摘要(`PINNED`;SHA-256 content-addressed)。 -/
|
|
contentDigest : String
|
|
/-- 描述(`OPEN`)。 -/
|
|
description : String
|
|
|
|
/-- Role-Skill 绑定(`PINNED`, ADR-0017)。一个 role 可绑定零或多个 skill。 -/
|
|
structure AgentRoleSkillBinding where
|
|
/-- 所属组织(`PINNED`)。 -/
|
|
organization : I.OrganizationId
|
|
/-- 绑定的 role(`PINNED`)。 -/
|
|
roleId : String
|
|
/-- skill 名称(`PINNED`)。 -/
|
|
skillName : String
|
|
/-- skill 版本(`PINNED`)。 -/
|
|
skillVersion : String
|
|
/-- 排序(`PINNED`)。 -/
|
|
sortOrder : Nat
|
|
|
|
end Spec.System
|