forked from bai/curriculum-project-hub
ChickenPige0n
854c6189bb
Add a shared transparent OrganizationAgentConfigFolder tree for grouping agent roles and skills in the admin UI without affecting identity, bindings, run loading, or slash commands.
95 lines
4.1 KiB
Lean4
95 lines
4.1 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`。
|
|
|
|
管理面分组:skill 与 role 共用一棵 org 内可嵌套 folder 树(ADR-0028)。folder 是透明
|
|
组织节点——只做后台导航/分组,不进入身份、解析与授权;name/roleId 唯一性、role→skill
|
|
绑定、run 加载与 slash 命令均与 folder 无关。
|
|
-/
|
|
|
|
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
|
|
/-- 管理面分组 folder(`PINNED`, ADR-0028;`none` 表示未分类)。透明节点,见
|
|
`AgentConfigFolder`——不进入 role 的身份与解析,roleId 仍 org 内唯一。 -/
|
|
folder : Option I.AgentConfigFolderId
|
|
|
|
/-- 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
|
|
/-- 管理面分组 folder(`PINNED`, ADR-0028;`none` 表示未分类)。透明节点,见
|
|
`AgentConfigFolder`——不进入 skill 的身份与解析,name 仍 org 内唯一。 -/
|
|
folder : Option I.AgentConfigFolderId
|
|
|
|
/-- 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
|
|
|
|
/-- Agent 配置 folder(`PINNED`, org-scoped, ADR-0028):skill 与 role **共用**的一棵
|
|
可嵌套 folder 树的节点,仅承担管理面的导航与分组。它是透明组织节点(与 ADR-0021
|
|
project Folder 同例):不是权限资源、不持有 grants;不进入 skill name / roleId 的身份
|
|
与解析——name/roleId 仍在 org 内唯一、与 folder 无关;role→skill 绑定、run 的 skill
|
|
快照加载与飞书 slash 命令均不引用 folder。folder 归属变更是 label 类变更
|
|
(ADR-0017),不归档会话。folder 仅在为空(无子 folder、无挂载的 skill/role)时可删
|
|
(`PINNED`)——挂载物的级动归置规则未定,故先禁止。 -/
|
|
structure AgentConfigFolder where
|
|
/-- 所属组织(`PINNED`)。 -/
|
|
organization : I.OrganizationId
|
|
/-- folder 标识(`OPEN` 表示)。 -/
|
|
id : I.AgentConfigFolderId
|
|
/-- 父 folder;`none` 为根层(`PINNED`,可嵌套)。 -/
|
|
parent : Option I.AgentConfigFolderId
|
|
|
|
/-- Skill/role 的 folder 归属良构性(`PINNED`, ADR-0028):每个 skill/role 至多归属于
|
|
一个 folder,且只能归属于与其**同 org** 的 folder;`none`(未分类)总是良构。
|
|
移动 skill/role 进出 folder 不改变其自身授权与解析。 -/
|
|
def AgentConfigFolderPlacement.WellScoped
|
|
(organization : I.OrganizationId)
|
|
(placement : Option I.AgentConfigFolderId)
|
|
(folderOrg : I.AgentConfigFolderId → Option I.OrganizationId) : Prop :=
|
|
∀ folderId, placement = some folderId → folderOrg folderId = some organization
|
|
|
|
end Spec.System
|