forked from EduCraft/curriculum-project-hub
Compare commits
28 Commits
| Author | SHA1 | Date | |
|---|---|---|---|
 sjfhsjfh
|
3ebe4b754d
|
||
|
sjfhsjfh
|
3fa6a5a5a5
|
||
|
sjfhsjfh
|
be4260bcd0
|
||
|
sjfhsjfh
|
a4449f03c4
|
||
|
sjfhsjfh
|
01bc20d25f
|
||
|
sjfhsjfh
|
38c3231190
|
||
|
sjfhsjfh
|
63416e06ea
|
||
|
sjfhsjfh
|
39bd2c9ff7
|
||
|
sjfhsjfh
|
e17e038232
|
||
|
sjfhsjfh
|
678bc9f56c
|
||
|
sjfhsjfh
|
3a50ed0ce2
|
||
 hongjr03
|
53998d2651 | ||
|
hongjr03
|
5b55cf18a8 | ||
|
hongjr03
|
b0d691d53f | ||
|
hongjr03
|
1f48c5b707 | ||
|
hongjr03
|
12a2f3117f | ||
|
hongjr03
|
2ee84d9543 | ||
|
hongjr03
|
3087132083 | ||
|
hongjr03
|
63c86322de | ||
|
hongjr03
|
ebf870249f | ||
|
hongjr03
|
f065f9f978 | ||
|
hongjr03
|
e7ad5580ec | ||
|
hongjr03
|
19d942e812 | ||
|
hongjr03
|
e5e923dd34 | ||
|
hongjr03
|
df0b12e38b | ||
|
hongjr03
|
83ec835d4c | ||
|
hongjr03
|
6ed56ddfc8 | ||
|
hongjr03
|
3bf643ff4d |
@@ -11,6 +11,9 @@
|
||||
# regenerable, not for VCS. The embedded engine mounts cph-render directly.
|
||||
render/vendor/local-packages/
|
||||
|
||||
# Environment
|
||||
.env
|
||||
|
||||
# Node (hub/ TS workspace and any future JS package)
|
||||
node_modules/
|
||||
|
||||
|
||||
Binary file not shown.
|
After Width: | Height: | Size: 106 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 159 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 140 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 135 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 128 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 101 KiB |
@@ -1,81 +1,219 @@
|
||||
# para-26071100 飞书应用配置清单
|
||||
# Educraft 组织接入与飞书应用配置指南
|
||||
|
||||
本文供 `para-26071100` 的飞书企业管理员操作。不要把 App Secret 粘贴到群聊、工单或本文档中；请通过约定的安全渠道交给平台部署人员。
|
||||
本文供准备接入 Educraft Alpha Silo 的学校、教培机构和组织管理员使用。完成本文后，请把末尾的“部署信息交付单”交给 Educraft 部署人员；我们会为组织创建独立的服务账号、数据库、运行目录和域名入口。
|
||||
|
||||
## 1. 创建企业自建应用
|
||||
> **安全提醒：** App Secret、模型 Provider Token 属于密钥，禁止粘贴到飞书群、普通云文档、工单正文或截图中。请只通过双方约定的安全渠道传递。
|
||||
|
||||
1. 打开飞书开放平台开发者后台。
|
||||
2. 在目标企业下创建“企业自建应用”。
|
||||
3. 应用名称可填写 `Educraft para-26071100`。
|
||||
4. 在“凭证与基础信息”记录：
|
||||
- App ID（通常以 `cli_` 开头）
|
||||
- App Secret
|
||||
5. 添加并启用“机器人”能力。
|
||||
## 1. 双方分别负责什么
|
||||
|
||||
Bot Open ID 不需要管理员手工寻找。平台部署人员会使用 App ID/App Secret 调用飞书 Bot Info API 获取，并在 bootstrap 时校验它确实属于这一个应用。
|
||||
| 角色 | 负责事项 |
|
||||
| --- | --- |
|
||||
| 组织管理员 | 创建企业自建应用、启用机器人、开通最小权限、配置事件、回调和 OAuth 重定向 URL、发布应用、提供 OWNER 身份 |
|
||||
| Educraft 部署人员 | 分配组织 slug 和域名、部署独立 Silo、加密保存应用及模型密钥、初始化 OWNER、联调和验收 |
|
||||
| 试点 OWNER | 把机器人加入试点群、创建或绑定项目、组织首轮验收 |
|
||||
|
||||
## 2. 开通权限
|
||||
## 2. 创建企业自建应用
|
||||
|
||||
在“权限管理”中搜索并申请下列能力。飞书控制台的中文名称可能随版本调整；如控制台同时显示 scope，可优先核对括号中的 scope。
|
||||
1. 打开[飞书开放平台开发者后台](https://open.feishu.cn/app)。
|
||||
2. 在目标企业下点击“创建企业自建应用”。应用名称建议填写“Educraft + 组织简称”。
|
||||
3. 进入“凭证与基础信息”，记录 App ID 和 App Secret。
|
||||
4. 进入“添加应用能力”，添加并启用“机器人”。
|
||||
|
||||
- 接收群聊中 @ 机器人的消息（`im:message.group_at_msg:readonly`）
|
||||
- 以应用身份发送消息（`im:message:send_as_bot`）
|
||||
- 获取消息内容，用于读取触发消息和线程上下文（`im:message:readonly`）
|
||||
- 获取与上传图片或文件资源（`im:resource`）
|
||||
- 添加、删除消息表情回复（`im:message.reactions:write_only`）
|
||||
- 获取用户基本信息（`contact:user.base:readonly`、`contact:user.basic_profile:readonly`）
|
||||
|
||||
|
||||
如果飞书 API 调试台提示某个上述操作缺少更细粒度权限，请把提示截图交给平台部署人员，不要直接勾选通讯录全量读取或其他超出清单的权限。
|
||||
App ID 通常以 `cli_` 开头，可以写入交付单。App Secret 必须通过安全渠道单独发送。Bot Open ID 不需要管理员手工查找；部署程序会用 App ID/App Secret 调用 Bot Info API 获取并校验归属。
|
||||
|
||||
## 3. 配置事件与卡片回调
|
||||
## 3. 开通最小权限
|
||||
|
||||
1. 进入“事件与回调”。
|
||||
2. 订阅方式选择“使用长连接接收事件”。
|
||||
3. 添加事件 `im.message.receive_v1`（接收消息）。
|
||||
4. 启用卡片交互回调 `card.action.trigger`，用于审批、中断运行和群聊建项目按钮。
|
||||
5. 不需要填写公网 Event Callback URL；Hub 使用飞书长连接。
|
||||
进入“权限管理”，点击“开通权限”，搜索并申请以下应用身份权限。控制台中文名称可能调整，请优先核对 scope。
|
||||
|
||||
## 4. 配置 OAuth 回调
|
||||
| 用途 | Scope |
|
||||
| --- | --- |
|
||||
| 接收群聊中 @ 机器人的消息 | `im:message.group_at_msg:readonly` |
|
||||
| 以应用身份发送消息 | `im:message:send_as_bot` |
|
||||
| 读取触发消息和线程上下文 | `im:message:readonly` |
|
||||
| 获取与上传图片或文件 | `im:resource` |
|
||||
| 添加、删除消息表情回复 | `im:message.reactions:write_only` |
|
||||
| 获取用户基本信息 | `contact:user.base:readonly` |
|
||||
| 获取用户基本资料 | `contact:user.basic_profile:readonly` |
|
||||
| 通过手机号或邮箱查询 OWNER Open ID | `contact:user.id:readonly` |
|
||||
|
||||
域名 DNS 和 TLS 生效后，在安全设置/重定向 URL 中添加：
|
||||
### 批量导入权限（推荐）
|
||||
|
||||
```text
|
||||
https://para-26071100.educraft.paradigm-edu.net/auth/feishu/callback
|
||||
在“权限管理”页面点击“批量处理 → 导入”，粘贴以下 JSON 后确认。导入只会新增本次列出的权限，不会删除或影响应用已经申请、开通的其他权限。
|
||||
|
||||
```json
|
||||
{
|
||||
"scopes": {
|
||||
"tenant": [
|
||||
"im:message.group_at_msg:readonly",
|
||||
"im:message:send_as_bot",
|
||||
"im:message:readonly",
|
||||
"im:resource",
|
||||
"im:message.reactions:write_only",
|
||||
"contact:user.base:readonly",
|
||||
"contact:user.basic_profile:readonly",
|
||||
"contact:user.id:readonly"
|
||||
],
|
||||
"user": []
|
||||
}
|
||||
}
|
||||
```
|
||||
|
||||
该回调用于 OWNER 登录受控的 Host Console。飞书群机器人长连接本身不依赖这个 URL。
|
||||
Educraft 机器人以应用身份调用上述 API，因此这些 scope 全部放在 `tenant`，不要为了省事把相同权限重复放进 `user`。
|
||||
|
||||
## 5. 发布并安装应用
|
||||
|
||||
|
||||
1. 创建应用版本并提交企业管理员审核。
|
||||
2. 将应用可用范围至少包含试点 OWNER 和试点群成员。
|
||||
3. 发布版本。
|
||||
4. 将机器人加入准备试用的飞书群。
|
||||
如果 API 调试台提示缺少更细粒度权限，请把错误提示和发生时间截图给部署人员。不要自行开通通讯录全量读取等超出本表的权限。
|
||||
|
||||
## 6. 获取首位 OWNER 身份
|
||||
## 4. 配置事件与卡片回调
|
||||
|
||||
平台 bootstrap 需要 OWNER 的飞书 Open ID 和显示名称。可通过飞书 API 调试台的用户信息接口查询；Open ID 通常以 `ou_` 开头。Union ID 可选，不影响首次部署。
|
||||
进入“事件与回调”。
|
||||
|
||||
请把以下结果通过安全渠道交给平台部署人员：
|
||||
1. 在“事件配置”中将订阅方式设为“使用长连接接收事件”。
|
||||
2. 添加事件“接收消息” `im.message.receive_v1`。
|
||||
3. 在“回调配置”中同样选择长连接。
|
||||
4. 添加回调“卡片回传交互” `card.action.trigger`，用于审批、运行中断和项目创建/绑定按钮。
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
这里不需要填写公网 Event Callback URL。Educraft Hub 使用飞书官方 SDK 的长连接模式。
|
||||
|
||||
## 5. 配置用户 OAuth 重定向 URL（必需）
|
||||
|
||||
普通群成员首次使用前，需要通过飞书 OAuth 建立其在本应用下的用户身份。进入“安全设置 → 重定向 URL”，添加组织专属 callback：
|
||||
|
||||
```text
|
||||
Organization: para-26071100
|
||||
App ID: cli_...
|
||||
App Secret: （安全渠道发送）
|
||||
OWNER Open ID: ou_...
|
||||
OWNER 显示名称:
|
||||
OWNER Union ID: （可选）
|
||||
试点群名称: （可选，便于验收）
|
||||
https://<organization-slug>.educraft.paradigm-edu.net/auth/feishu/callback
|
||||
```
|
||||
|
||||
## 7. 验收动作
|
||||
例如组织 slug 为 `example-school`：
|
||||
|
||||
平台通知部署完成后：
|
||||
```text
|
||||
https://example-school.educraft.paradigm-edu.net/auth/feishu/callback
|
||||
```
|
||||
|
||||
1. OWNER 打开 Host Console，完成飞书 OAuth 登录。
|
||||
2. 在试点群中 @机器人发送一条纯文本消息。
|
||||
3. 如果群尚未绑定项目，机器人应返回项目创建/绑定卡片。
|
||||
4. 创建项目后再次 @机器人，确认出现处理状态、流式卡片和最终回答。
|
||||
5. 再测试一个小文件附件，以及运行中断按钮。
|
||||
|
||||
|
||||
任何一步失败时，请保留发生时间、群名、消息截图和飞书 request/log ID；不要在截图中包含 App Secret 或 Provider token。
|
||||
必须使用 Educraft 部署人员最终确认的 slug；不要直接照抄示例。该 URL 用于 OAuth 返回并创建应用作用域下的飞书用户身份，不代表当前已经开放组织管理台。
|
||||
|
||||
组织专属 OAuth 同时完成身份建立和入组：首次成功登录的用户会自动成为当前 Organization 的 `MEMBER`，回到群聊即可使用。`OWNER` 和 `ADMIN` 仍只能由部署人员或管理员显式授予；曾被移除的成员重新登录不会自动恢复资格。
|
||||
|
||||
## 6. 发布并安装应用
|
||||
|
||||
1. 进入“版本管理与发布”，点击“创建版本”。
|
||||
2. 将应用可用范围至少覆盖试点 OWNER 和试点群成员。
|
||||
3. 提交企业管理员审核并发布。
|
||||
4. 发布成功后，将机器人加入准备试用的群。
|
||||
|
||||
|
||||
|
||||
仅保存开发配置但未发布时，新增权限、事件和可用范围通常不会对试点用户生效。
|
||||
|
||||
## 7. 获取首位 OWNER 身份
|
||||
|
||||
首次部署必须指定一位组织 OWNER。OWNER 是 Educraft 组织内的初始管理员，不等同于飞书应用所有者；两者可以是同一个人，也可以不同。部署所需的 Open ID 必须由本次创建的企业自建应用查询，因为同一用户在不同应用下的 Open ID 不同，不能复用其他应用查到的值。
|
||||
|
||||
### 7.1 确认 OWNER
|
||||
|
||||
先确认哪一位企业成员将担任 OWNER。记录其飞书显示名称，并准备在飞书的成员选择器中按姓名找到本人。若企业内有同名成员，选择前须通过部门等信息核对身份。
|
||||
|
||||
### 7.2 开通查询权限和数据范围
|
||||
|
||||
确认应用已开通上文列出的用户基本信息和用户 ID 权限。如果使用上文的批量导入 JSON，这些权限已包含在内。
|
||||
|
||||
应用的通讯录数据范围还必须覆盖这位 OWNER。最小做法是把 OWNER 加入应用可用范围；不需要为此开放全企业通讯录。
|
||||
|
||||
### 7.3 在官方接口页面获取 Open ID
|
||||
|
||||
1. 打开飞书开放平台的[“获取单个用户信息”接口页面](https://open.feishu.cn/document/server-docs/contact-v3/user/get)。如果使用带 `appId` 参数的页面链接，可以直接进入对应应用；本文不提供固定 App ID，请在页面顶部选择本组织刚创建的企业自建应用，并核对 App ID 与交付单一致。
|
||||
2. 找到路径参数 `user_id`，点击参数输入框旁的“获取”。
|
||||
3. 在成员选择器中找到并选择 OWNER；如有同名成员，依据部门等信息确认本人。
|
||||
4. ID 类型选择 `open_id`。将选择器返回的值填入 `user_id`，并保持查询参数 `user_id_type=open_id`。
|
||||
5. 以应用身份（`tenant_access_token`）调用接口，核对成功响应中 `data.user.name` 与 OWNER 本人一致。
|
||||
6. 复制完整的 `data.user.open_id` 交给 Educraft 部署人员。Open ID 通常以 `ou_` 开头。
|
||||
|
||||
参数旁的“获取”是飞书文档调试台提供的成员选择功能，不是要求管理员预先知道 Open ID。不要复用其他应用查到的 Open ID；同一用户在不同应用下的 Open ID 不同。若无法选择成员或接口调用失败，依次检查：页面当前选择的 App ID、应用可用范围和通讯录数据范围是否覆盖 OWNER、用户基本信息与用户 ID 权限是否已开通并随应用版本发布。
|
||||
|
||||
### 7.4 核对并交付
|
||||
|
||||
交付前完成以下检查：
|
||||
|
||||
- 返回用户的姓名与 OWNER 本人一致；
|
||||
- Open ID 来自本次组织的这一个 App ID；
|
||||
- Open ID 完整复制，没有空格或省略号；
|
||||
- 显示名称使用组织希望在 Educraft 中展示的姓名；
|
||||
- Union ID 不是必填项，查不到可以留空。
|
||||
|
||||
最终向部署人员提供：
|
||||
|
||||
```text
|
||||
OWNER Open ID：ou_...
|
||||
OWNER 显示名称：
|
||||
OWNER Union ID：（可选）
|
||||
用于查询的 App ID：cli_...
|
||||
```
|
||||
|
||||
Open ID 和显示名称可以放在普通交付单中；不要把 App Secret 一起粘贴进去。
|
||||
|
||||
## 8. 部署信息交付单
|
||||
|
||||
请复制下面的模板填写。标注“安全渠道”的字段不要与普通字段放在同一条群消息或云文档中。
|
||||
|
||||
```text
|
||||
【组织信息】
|
||||
组织正式名称：
|
||||
组织简称：
|
||||
期望 organization slug：（小写字母、数字和连字符，例如 example-school）
|
||||
期望机器人显示名称：
|
||||
|
||||
【飞书应用】
|
||||
App ID：cli_...
|
||||
App Secret：（通过安全渠道单独发送）
|
||||
应用已发布：是 / 否
|
||||
机器人能力已启用：是 / 否
|
||||
消息事件和卡片回调已配置：是 / 否
|
||||
OAuth 重定向 URL 已配置：是 / 否
|
||||
|
||||
【首位 OWNER】
|
||||
OWNER Open ID：ou_...
|
||||
OWNER 显示名称：
|
||||
OWNER Union ID：（可选）
|
||||
|
||||
【试点范围】
|
||||
试点群名称：（可选，用于验收定位）
|
||||
初始 Team 名称：（可选；没有 Team 不影响首次部署）
|
||||
预计试用人数：
|
||||
|
||||
【模型配置】
|
||||
Provider 名称：（例如 OpenRouter）
|
||||
Provider Base URL：
|
||||
Provider Token：（通过安全渠道单独发送）
|
||||
启用的模型 ID：
|
||||
```
|
||||
|
||||
Educraft 部署人员收到信息后，会回传最终 organization slug、访问域名、部署窗口和验收时间。若期望 slug 已被占用或不符合命名规则，会在部署前协调调整。
|
||||
|
||||
## 9. 上线验收
|
||||
|
||||
部署人员通知服务就绪后，由 OWNER 完成：
|
||||
|
||||
1. OWNER 在试点群中 @机器人发送一条纯文本消息。
|
||||
2. 如果群尚未绑定项目，确认机器人返回项目创建/绑定卡片。
|
||||
3. 创建项目后再次 @机器人，确认出现处理状态、流式卡片和最终回答。
|
||||
4. 选择一位非 OWNER 试点成员完成 OAuth 登录，确认其自动以 MEMBER 身份加入组织。
|
||||
5. 该成员在同一群中 @机器人，确认能够进入已绑定项目。
|
||||
6. 测试一个小文件附件、一次运行中断，以及一个需要生成文档的任务。
|
||||
|
||||
出现问题时，请保留发生时间、群名、消息截图和飞书 request/log ID。截图前确认其中不包含 App Secret、Provider Token 或其他密钥。
|
||||
|
||||
## 10. Alpha 阶段边界
|
||||
|
||||
- 每个组织运行在独立的系统用户、服务实例、数据库和持久化目录中。
|
||||
- 组织的 role、system prompt、tools 和 skills 是运行时配置，不需要跟随版本发布。
|
||||
- 同一项目同一时间只执行一个任务，避免并发修改同一个 workspace；组织级并发上限由部署配置决定。
|
||||
- 当前由 Educraft 人工创建组织、OWNER、Provider Connection 和初始 Team，并通过服务器上的受控管理命令运维；组织管理台尚未开放。
|
||||
- 非 OWNER 试点成员通过组织专属 OAuth 首次登录后自动成为 MEMBER；OWNER/ADMIN 提权和被移除成员的恢复仍需人工操作。
|
||||
- Alpha 不提供开放注册、自助密钥管理或跨组织资源共享。
|
||||
|
||||
@@ -0,0 +1,133 @@
|
||||
# New Alpha Silo runbook
|
||||
|
||||
Use this runbook for a new Organization. A Silo is not merely another row in
|
||||
the existing database: it has an independent PostgreSQL role/database, Linux
|
||||
service identity, systemd unit, secret directory/keyring, workspace, skill
|
||||
store, loopback port, domain, Feishu app and provider credential.
|
||||
|
||||
The repeatable entry point is:
|
||||
|
||||
```sh
|
||||
bash hub/deploy/new_silo.sh
|
||||
```
|
||||
|
||||
After collecting the Organization inputs, the wizard shows the assigned
|
||||
resources and asks once before applying them directly over SSH. The generated
|
||||
bundle is only a root-secret-safe retry and audit checkpoint; the operator does
|
||||
not execute it manually during the normal path.
|
||||
|
||||
It gathers values and writes a private deployment bundle below
|
||||
`~/.cph-silo-plans/<instance-id>/`. The directory and all generated files are
|
||||
mode `0700`/`0600`. Never commit, paste into chat, or copy that directory into
|
||||
an immutable release. Run the wizard once per Organization; do not edit a copy
|
||||
from another Organization.
|
||||
|
||||
## Inputs to collect
|
||||
|
||||
The wizard derives the instance/Organization id from the slug, uses the current
|
||||
release and managed Alpha defaults, connects to the managed host (currently
|
||||
`39.107.254.4`), derives
|
||||
`https://<organization-slug>.educraft.paradigm-edu.net` from the wildcard DNS,
|
||||
and allocates an unused loopback port plus short workspace path by inspecting
|
||||
existing Silo environments, listening sockets and workspace paths over
|
||||
read-only SSH. The Organization administrator supplies:
|
||||
|
||||
- Organization display name and slug;
|
||||
- Feishu App ID and App Secret (the wizard resolves the bot Open ID);
|
||||
- the first OWNER's Open ID and display name;
|
||||
- an Organization-exclusive OpenRouter token.
|
||||
|
||||
Everything else is platform-managed or derived: instance/Organization id,
|
||||
server, SSH settings, release, resource ceilings, database coordinates and
|
||||
generated password, domain, port, workspace, provider/base URL, model/role,
|
||||
curated skills, concurrency, request/file limits and the managed Mihomo proxy
|
||||
environment. `NODE_USE_ENV_PROXY=1` is required on Node.js 24 so Hub's built-in
|
||||
`fetch` actually uses that proxy; merely setting `HTTP_PROXY`/`HTTPS_PROXY` is
|
||||
not sufficient.
|
||||
|
||||
The Feishu app is scoped to this Silo. OAuth users authenticated by that app are
|
||||
automatically admitted to this Organization; OWNER remains the initial
|
||||
privileged membership used for controlled administration and bootstrap. An
|
||||
empty initial team list does not block the Alpha.
|
||||
|
||||
To target a replacement platform-managed host, the platform operator may set
|
||||
`CPH_ALPHA_HOST`, `CPH_ALPHA_DEPLOY_USER`, `CPH_ALPHA_SSH_PORT` and
|
||||
`CPH_ALPHA_BASE_DOMAIN` before running the wizard. These are fleet controls,
|
||||
not Organization setup questions.
|
||||
|
||||
Obtain a person's Open ID from the Feishu user-get documentation page by
|
||||
clicking the `user_id` value picker and selecting the person. Configure the
|
||||
redirect URL shown by the generated `OPERATE.md`; it is required for first-time
|
||||
OAuth admission.
|
||||
|
||||
## Host prerequisites
|
||||
|
||||
Before the first Silo on a host, install Node.js 24+, npm, rsync, PostgreSQL
|
||||
server/client, `pg_isready`, systemd, bubblewrap, socat, `runuser`, `setpriv`,
|
||||
`pg_dump`, tar, sha256sum, Nginx, Certbot, Typst and a compatible `cph` binary.
|
||||
Configure outbound proxying independently at host/service level and verify both
|
||||
GitHub and the selected model provider through it. The wizard does not install
|
||||
or select proxy nodes.
|
||||
|
||||
Use a deployment account with only the required passwordless sudo operations.
|
||||
The application itself always runs as the installer-created non-root
|
||||
`cph-<instance-id>` user. PostgreSQL must have a separate login role and logical
|
||||
database per Silo even when all Silo databases share one PostgreSQL server.
|
||||
|
||||
## Execute a generated bundle
|
||||
|
||||
Open the bundle's `OPERATE.md` and perform its numbered gates in order:
|
||||
|
||||
1. DNS, Feishu redirect URL, permissions and event subscription.
|
||||
2. Dedicated PostgreSQL role and database.
|
||||
3. Immutable release publication. Exit 78 is expected only when the first
|
||||
installer call seeds this instance's keyring and environment template.
|
||||
4. Root-owned secret installation and off-host keyring recovery copy.
|
||||
5. Prisma migration, stopped service installation and idempotent bootstrap.
|
||||
6. Explicit runtime role/skill installation.
|
||||
7. Nginx/TLS, service start, internal/external health and Feishu acceptance.
|
||||
8. First off-host backup.
|
||||
|
||||
Every command must fail fast. Do not add `|| true` around install, migration,
|
||||
bootstrap, Nginx validation, health, or backup checks. If a check fails, retain
|
||||
the unit logs and the exact failed stage before changing configuration.
|
||||
|
||||
## Default runtime role and skills
|
||||
|
||||
Roles and skills are dynamic Silo state, not release contents. The release
|
||||
contains only the management CLI. Stage approved skill directories on the host
|
||||
and install them with `agent_config.sh`; PostgreSQL records role definitions and
|
||||
skill selections while the versioned skill content lives in the Silo state
|
||||
directory and is included in backups.
|
||||
|
||||
For the current Alpha, upsert the default role with the agreed education
|
||||
assistant system prompt, model selection, tools policy and approved skill list.
|
||||
Keep the prompt in a root-controlled staging file, pass it via
|
||||
`--system-prompt-file`, then verify with `agent_config.sh list`. Do not sync an
|
||||
operator's entire personal skill directory: each enabled skill must be reviewed
|
||||
and named explicitly. Typst being installed on the host and the Typst skill
|
||||
being enabled are separate gates.
|
||||
|
||||
## Acceptance gate
|
||||
|
||||
A Silo is ready only when all of the following pass:
|
||||
|
||||
- its systemd service is active and both loopback and TLS health endpoints pass;
|
||||
- startup preflight sees exactly the configured Organization plus active Feishu
|
||||
and provider connections;
|
||||
- OWNER completes OAuth and can interact with the bot;
|
||||
- a non-OWNER completes OAuth and can interact with the same app/Organization;
|
||||
- two Feishu groups bind distinct projects/sessions;
|
||||
- a restart preserves persisted session cursor behavior;
|
||||
- the configured provider/model succeeds through the host proxy;
|
||||
- every enabled skill is listed, and a Typst task succeeds if Typst is enabled;
|
||||
- the first business backup and separate recovery backup are stored off-host.
|
||||
|
||||
## Rollback boundary
|
||||
|
||||
For a failed code release, point only this instance back to the previous
|
||||
immutable release and rerun its installer with the same instance parameters.
|
||||
Do not roll back a database after migrations unless that release's documented
|
||||
database compatibility permits it. Preserve the environment, keyring, database,
|
||||
workspace and skill store. For destructive recovery, stop traffic and use the
|
||||
separate restore procedure; never substitute another Silo's state.
|
||||
@@ -1,5 +1,16 @@
|
||||
# Alpha Silo service installation
|
||||
|
||||
For a brand-new Organization, start with the repeatable wizard and end-to-end
|
||||
operator runbook:
|
||||
|
||||
```sh
|
||||
bash hub/deploy/new_silo.sh
|
||||
```
|
||||
|
||||
See [NEW_SILO_RUNBOOK.md](NEW_SILO_RUNBOOK.md). The remainder of this document
|
||||
describes the individual installer and maintenance primitives used by the
|
||||
generated bundle.
|
||||
|
||||
The supervised alpha runs one Organization per named Silo. The supported host
|
||||
has systemd, PostgreSQL, Node.js 24+, `pg_isready`, `runuser`, `setpriv`,
|
||||
bubblewrap, `socat`, `pg_dump`, `tar`, `sha256sum`, and a compatible `cph`.
|
||||
|
||||
Executable
+73
@@ -0,0 +1,73 @@
|
||||
#!/usr/bin/env bash
|
||||
# Apply a bundle produced by new_silo.sh to the managed Alpha host.
|
||||
set -euo pipefail
|
||||
|
||||
BUNDLE="${1:?usage: apply_new_silo.sh BUNDLE_DIR}"
|
||||
ANSWERS="$BUNDLE/answers.env"
|
||||
[ -f "$ANSWERS" ] || { echo "missing $ANSWERS" >&2; exit 1; }
|
||||
|
||||
value() { sed -n "s/^$1=//p" "$ANSWERS" | tail -n1; }
|
||||
INSTANCE_ID="$(value INSTANCE_ID)"
|
||||
ORG_ID="$(value ORGANIZATION_ID)"
|
||||
HOST="$(value DEPLOY_HOST)"
|
||||
SSH_USER="$(value DEPLOY_USER)"
|
||||
SSH_PORT="$(value DEPLOY_SSH_PORT)"
|
||||
SSH_KEY="$(value DEPLOY_SSH_KEY)"
|
||||
BASE="$(value DEPLOY_BASE)"
|
||||
RELEASE="$(value RELEASE_ID)"
|
||||
HUB_PORT="$(value HUB_PORT)"
|
||||
WORKSPACE="$(value WORKSPACE_ROOT)"
|
||||
MEMORY="$(value MEMORY_MAX)"
|
||||
CPU="$(value CPU_QUOTA)"
|
||||
TASKS="$(value TASKS_MAX)"
|
||||
DB_NAME="$(value DATABASE_NAME)"
|
||||
DB_USER="$(value DATABASE_USER)"
|
||||
DB_PASSWORD="$(value DATABASE_PASSWORD)"
|
||||
PUBLIC_URL="$(value PUBLIC_BASE_URL)"
|
||||
DOMAIN="${PUBLIC_URL#https://}"
|
||||
HUB_DIR="$BASE/releases/$RELEASE/hub"
|
||||
ENV_PATH="$BASE/.secrets/$INSTANCE_ID/platform.env"
|
||||
KEYRING_PATH="$BASE/.secrets/$INSTANCE_ID/secret-keyring.json"
|
||||
UNIT="cph-hub-$INSTANCE_ID.service"
|
||||
SSH=(ssh -i "$SSH_KEY" -p "$SSH_PORT" -o BatchMode=yes "$SSH_USER@$HOST")
|
||||
SCP=(scp -i "$SSH_KEY" -P "$SSH_PORT")
|
||||
|
||||
for file in platform.env bootstrap.json default-role-prompt.md; do
|
||||
[ -f "$BUNDLE/$file" ] || { echo "missing bundle file: $file" >&2; exit 1; }
|
||||
done
|
||||
|
||||
echo "[1/8] Verify immutable release"
|
||||
"${SSH[@]}" "test -f '$BASE/releases/$RELEASE/.complete'"
|
||||
|
||||
echo "[2/8] Create dedicated database"
|
||||
if ! "${SSH[@]}" "sudo -u postgres psql -Atqc \"select 1 from pg_database where datname='$DB_NAME'\"" | grep -qx 1; then
|
||||
printf "CREATE ROLE %s LOGIN PASSWORD '%s';\nCREATE DATABASE %s OWNER %s;\n" \
|
||||
"$DB_USER" "$DB_PASSWORD" "$DB_NAME" "$DB_USER" | "${SSH[@]}" sudo -u postgres psql -v ON_ERROR_STOP=1
|
||||
fi
|
||||
|
||||
echo "[3/8] Seed instance keyring and service template"
|
||||
set +e
|
||||
"${SSH[@]}" "BASE='$BASE' HUB_DIR='$HUB_DIR' INSTANCE_ID='$INSTANCE_ID' WORKSPACE_ROOT='$WORKSPACE' PORT='$HUB_PORT' MEMORY_MAX='$MEMORY' CPU_QUOTA='$CPU' TASKS_MAX='$TASKS' bash '$HUB_DIR/deploy/install_service.sh'"
|
||||
status=$?
|
||||
set -e
|
||||
[ "$status" -eq 0 ] || [ "$status" -eq 78 ] || exit "$status"
|
||||
|
||||
echo "[4/8] Upload root-only configuration"
|
||||
remote_stage="/root/.cph-bootstrap-$INSTANCE_ID"
|
||||
"${SSH[@]}" "install -d -o root -g root -m 0700 '$remote_stage'"
|
||||
"${SCP[@]}" "$BUNDLE/platform.env" "$BUNDLE/bootstrap.json" "$BUNDLE/default-role-prompt.md" "$SSH_USER@$HOST:$remote_stage/"
|
||||
"${SSH[@]}" "install -o root -g root -m 0600 '$remote_stage/platform.env' '$ENV_PATH'; chmod 0600 '$remote_stage/bootstrap.json' '$remote_stage/default-role-prompt.md'"
|
||||
|
||||
echo "[5/8] Migrate, install, and bootstrap"
|
||||
"${SSH[@]}" "set -euo pipefail; set -a; . '$ENV_PATH'; set +a; node '$HUB_DIR/node_modules/prisma/build/index.js' migrate deploy --schema '$HUB_DIR/prisma/schema.prisma'; BASE='$BASE' HUB_DIR='$HUB_DIR' INSTANCE_ID='$INSTANCE_ID' WORKSPACE_ROOT='$WORKSPACE' PORT='$HUB_PORT' MEMORY_MAX='$MEMORY' CPU_QUOTA='$CPU' TASKS_MAX='$TASKS' bash '$HUB_DIR/deploy/install_service.sh'; node '$HUB_DIR/dist/deployment/bootstrap-silo-cli.js' --config-file '$remote_stage/bootstrap.json' --keyring-file '$KEYRING_PATH'"
|
||||
|
||||
echo "[6/8] Copy curated skills and configure default role"
|
||||
"${SSH[@]}" "set -euo pipefail; stage='/var/lib/cph-hub/$INSTANCE_ID/state/operator-staging'; install -d -o cph-$INSTANCE_ID -g cph-$INSTANCE_ID -m 0700 \"\$stage/skills\"; install -o cph-$INSTANCE_ID -g cph-$INSTANCE_ID -m 0600 '$remote_stage/default-role-prompt.md' \"\$stage/default-role-prompt.md\"; for source in /var/lib/cph-hub/para-26071100/state/skills/versions/*; do name=\$(sed -n 's/^name: *//p' \"\$source/SKILL.md\" | head -n1); case \"\$name\" in outline|lesson-project|data-processing-spec|typst) cp -a \"\$source\" \"\$stage/skills/\$name\"; chown -R cph-$INSTANCE_ID:cph-$INSTANCE_ID \"\$stage/skills/\$name\";; esac; done; for name in outline lesson-project data-processing-spec typst; do INSTANCE_ID='$INSTANCE_ID' ENV_FILE='$ENV_PATH' HUB_DIR='$HUB_DIR' bash '$HUB_DIR/deploy/agent_config.sh' install-skill --organization '$ORG_ID' --source \"\$stage/skills/\$name\" --version 1; done; INSTANCE_ID='$INSTANCE_ID' ENV_FILE='$ENV_PATH' HUB_DIR='$HUB_DIR' bash '$HUB_DIR/deploy/agent_config.sh' upsert-role --organization '$ORG_ID' --role draft --label '智能助手' --system-prompt-file \"\$stage/default-role-prompt.md\" --tools-json null; INSTANCE_ID='$INSTANCE_ID' ENV_FILE='$ENV_PATH' HUB_DIR='$HUB_DIR' bash '$HUB_DIR/deploy/agent_config.sh' set-role-skills --organization '$ORG_ID' --role draft --skills outline,lesson-project,data-processing-spec,typst; rm -rf \"\$stage\""
|
||||
|
||||
echo "[7/8] Configure Nginx and TLS"
|
||||
printf 'server { listen 80; listen [::]:80; server_name %s; client_max_body_size 2m; location / { proxy_pass http://127.0.0.1:%s; proxy_http_version 1.1; proxy_set_header Host $host; proxy_set_header X-Real-IP $remote_addr; proxy_set_header X-Forwarded-For $proxy_add_x_forwarded_for; proxy_set_header X-Forwarded-Proto $scheme; proxy_set_header Upgrade $http_upgrade; proxy_set_header Connection $connection_upgrade; proxy_read_timeout 3600s; proxy_send_timeout 3600s; proxy_buffering off; } }\n' "$DOMAIN" "$HUB_PORT" | "${SSH[@]}" "install -o root -g root -m 0644 /dev/stdin '/etc/nginx/sites-available/$INSTANCE_ID'; ln -sfn '/etc/nginx/sites-available/$INSTANCE_ID' '/etc/nginx/sites-enabled/$INSTANCE_ID'; nginx -t; systemctl reload nginx; certbot --nginx --non-interactive --agree-tos --redirect --register-unsafely-without-email -d '$DOMAIN'"
|
||||
|
||||
echo "[8/8] Start and verify"
|
||||
"${SSH[@]}" "systemctl enable --now '$UNIT'; systemctl is-active --quiet '$UNIT'; curl --fail --silent 'http://127.0.0.1:$HUB_PORT/api/healthz' >/dev/null; rm -f '$remote_stage/bootstrap.json'"
|
||||
curl --fail --silent --show-error "$PUBLIC_URL/api/healthz" >/dev/null
|
||||
echo "Deployed $INSTANCE_ID at $PUBLIC_URL"
|
||||
Executable
+412
@@ -0,0 +1,412 @@
|
||||
#!/usr/bin/env bash
|
||||
#
|
||||
# A wizard — walks a human through a manual procedure step by step.
|
||||
# Generated by the /wizard skill.
|
||||
#
|
||||
# Everything above the "STAGES" marker is the wizard library: do not hand-edit
|
||||
# it. Author the per-step stages below the marker.
|
||||
|
||||
set -euo pipefail
|
||||
|
||||
# ──────────────────────────────────────────────────────────────────────────
|
||||
# Wizard library — delightful, consistent UX. Identical across every wizard.
|
||||
# ──────────────────────────────────────────────────────────────────────────
|
||||
|
||||
if [[ -t 1 ]] && command -v tput >/dev/null 2>&1 && [[ "$(tput colors 2>/dev/null || echo 0)" -ge 8 ]]; then
|
||||
BOLD=$(tput bold); DIM=$(tput dim); RESET=$(tput sgr0)
|
||||
BLUE=$(tput setaf 4); GREEN=$(tput setaf 2); YELLOW=$(tput setaf 3); RED=$(tput setaf 1)
|
||||
else
|
||||
BOLD=""; DIM=""; RESET=""; BLUE=""; GREEN=""; YELLOW=""; RED=""
|
||||
fi
|
||||
|
||||
# Author sets these two at the top of the stages section.
|
||||
TOTAL_STAGES=0
|
||||
TOTAL_MINUTES=0
|
||||
|
||||
_STAGE_INDEX=0
|
||||
_MINUTES_ELAPSED=0
|
||||
ENV_FILE="${ENV_FILE:-.env}"
|
||||
WRITTEN_ENV=() # KEYs written to ENV_FILE this run
|
||||
WRITTEN_SECRET=() # secret NAMEs set this run
|
||||
SKIPPED=() # things we couldn't do (e.g. gh missing)
|
||||
|
||||
# _clear — wipe the terminal so only the current step is on screen. No-op when
|
||||
# output isn't a terminal, so piped logs stay readable.
|
||||
_clear() {
|
||||
[[ -t 1 ]] || return 0
|
||||
if command -v tput >/dev/null 2>&1; then tput clear; else printf '\033[2J\033[3J\033[H'; fi
|
||||
}
|
||||
|
||||
# banner "Title" — opening frame: what this wizard does and how long it takes.
|
||||
banner() {
|
||||
_clear
|
||||
printf '\n%s%s %s%s\n' "$BOLD" "$BLUE" "$1" "$RESET"
|
||||
printf '%s %s stages · about %s minutes%s\n\n' \
|
||||
"$DIM" "$TOTAL_STAGES" "$TOTAL_MINUTES" "$RESET"
|
||||
printf '%s You drive the browser; this wizard tells you exactly what to do and\n' "$DIM"
|
||||
printf ' captures the values you copy back. Stop any time with Ctrl-C and re-run\n'
|
||||
printf ' later — it remembers values already saved.%s\n' "$RESET"
|
||||
pause "Ready to start?"
|
||||
}
|
||||
|
||||
# stage "Name" <minutes> — clear the screen, then announce a stage and show
|
||||
# progress + time remaining. Clearing keeps only the current step on screen.
|
||||
stage() {
|
||||
_clear
|
||||
_STAGE_INDEX=$((_STAGE_INDEX + 1))
|
||||
local remaining=$((TOTAL_MINUTES - _MINUTES_ELAPSED))
|
||||
(( remaining < 0 )) && remaining=0
|
||||
_MINUTES_ELAPSED=$((_MINUTES_ELAPSED + ${2:-0}))
|
||||
printf '\n%s%s▸ Stage %s/%s · %s%s %s(~%s min left)%s\n' \
|
||||
"$BOLD" "$BLUE" "$_STAGE_INDEX" "$TOTAL_STAGES" "$1" "$RESET" "$DIM" "$remaining" "$RESET"
|
||||
}
|
||||
|
||||
# say "..." — a plain instruction line.
|
||||
say() { printf ' %s\n' "$1"; }
|
||||
# step "..." — a numbered-feeling action the human takes in the browser.
|
||||
step() { printf ' %s•%s %s\n' "$BLUE" "$RESET" "$1"; }
|
||||
note() { printf ' %s%s%s\n' "$DIM" "$1" "$RESET"; }
|
||||
warn() { printf ' %s⚠ %s%s\n' "$YELLOW" "$1" "$RESET"; }
|
||||
|
||||
# open_url URL — open in the human's browser, cross-platform incl. WSL.
|
||||
open_url() {
|
||||
local url="$1"
|
||||
printf ' %s↗ opening%s %s\n' "$GREEN" "$RESET" "$url"
|
||||
{ if command -v wslview >/dev/null 2>&1; then wslview "$url"
|
||||
elif command -v explorer.exe >/dev/null 2>&1; then explorer.exe "$url"
|
||||
elif command -v xdg-open >/dev/null 2>&1; then xdg-open "$url"
|
||||
elif command -v open >/dev/null 2>&1; then open "$url"
|
||||
else warn "couldn't open a browser — visit it manually: $url"; fi
|
||||
} >/dev/null 2>&1 || warn "couldn't open a browser — visit it manually: $url"
|
||||
}
|
||||
|
||||
# pause "msg" — wait for the human to confirm they've done the manual part.
|
||||
pause() {
|
||||
printf ' %s%s%s ' "$DIM" "${1:-Press Enter to continue}" "$RESET"
|
||||
read -r _ || true
|
||||
}
|
||||
|
||||
# confirm "question" — y/N gate; returns success on yes.
|
||||
confirm() {
|
||||
local reply=""
|
||||
printf ' %s? %s [y/N] ' "$YELLOW" "$1"
|
||||
read -r reply || true
|
||||
[[ "$reply" =~ ^[Yy] ]]
|
||||
}
|
||||
|
||||
# _existing KEY — current value of KEY in ENV_FILE, if any.
|
||||
_existing() {
|
||||
[[ -f "$ENV_FILE" ]] || return 1
|
||||
local line; line=$(grep -E "^${1}=" "$ENV_FILE" | tail -n1) || return 1
|
||||
printf '%s' "${line#*=}"
|
||||
}
|
||||
|
||||
# ask KEY "Prompt" — read a value into $KEY. Offers the existing .env value as
|
||||
# a default on re-runs (Enter keeps it). Visible input (non-secret).
|
||||
ask() {
|
||||
local key="$1" prompt="$2" current input
|
||||
current=$(_existing "$key" || true)
|
||||
if [[ -n "$current" ]]; then
|
||||
printf ' %s%s%s %s[Enter keeps current]%s ' "$BOLD" "$prompt" "$RESET" "$DIM" "$RESET"
|
||||
else
|
||||
printf ' %s%s%s ' "$BOLD" "$prompt" "$RESET"
|
||||
fi
|
||||
read -r input || true
|
||||
[[ -z "$input" && -n "$current" ]] && input="$current"
|
||||
printf -v "$key" '%s' "$input"
|
||||
}
|
||||
|
||||
# ask_secret KEY "Prompt" — like ask, but input is hidden.
|
||||
ask_secret() {
|
||||
local key="$1" prompt="$2" current input
|
||||
current=$(_existing "$key" || true)
|
||||
if [[ -n "$current" ]]; then
|
||||
printf ' %s%s%s %s[Enter keeps current]%s ' "$BOLD" "$prompt" "$RESET" "$DIM" "$RESET"
|
||||
else
|
||||
printf ' %s%s%s ' "$BOLD" "$prompt" "$RESET"
|
||||
fi
|
||||
read -rs input || true
|
||||
printf '\n'
|
||||
[[ -z "$input" && -n "$current" ]] && input="$current"
|
||||
printf -v "$key" '%s' "$input"
|
||||
}
|
||||
|
||||
# write_env KEY VALUE — upsert KEY=VALUE into ENV_FILE (creates it; replaces
|
||||
# any existing line). Idempotent.
|
||||
write_env() {
|
||||
local key="$1" value="$2" tmp
|
||||
touch "$ENV_FILE"
|
||||
tmp=$(mktemp)
|
||||
grep -vE "^${key}=" "$ENV_FILE" > "$tmp" || true
|
||||
printf '%s=%s\n' "$key" "$value" >> "$tmp"
|
||||
mv "$tmp" "$ENV_FILE"
|
||||
WRITTEN_ENV+=("$key")
|
||||
printf ' %s✓ wrote%s %s → %s\n' "$GREEN" "$RESET" "$key" "$ENV_FILE"
|
||||
}
|
||||
|
||||
# set_secret NAME VALUE — set a GitHub Actions repo secret via gh. Falls back
|
||||
# to a warning (and records it) if gh is unavailable or unauthenticated.
|
||||
set_secret() {
|
||||
local name="$1" value="$2"
|
||||
if command -v gh >/dev/null 2>&1 && gh auth status >/dev/null 2>&1; then
|
||||
if printf '%s' "$value" | gh secret set "$name" >/dev/null 2>&1; then
|
||||
WRITTEN_SECRET+=("$name")
|
||||
printf ' %s✓ set%s GitHub secret %s\n' "$GREEN" "$RESET" "$name"
|
||||
return
|
||||
fi
|
||||
fi
|
||||
SKIPPED+=("GitHub secret $name (set it manually: gh secret set $name)")
|
||||
warn "skipped GitHub secret $name — gh not ready; set it later"
|
||||
}
|
||||
|
||||
# set_var NAME VALUE — set a GitHub Actions repo variable (non-secret).
|
||||
set_var() {
|
||||
local name="$1" value="$2"
|
||||
if command -v gh >/dev/null 2>&1 && gh auth status >/dev/null 2>&1; then
|
||||
if gh variable set "$name" --body "$value" >/dev/null 2>&1; then
|
||||
printf ' %s✓ set%s GitHub variable %s\n' "$GREEN" "$RESET" "$name"
|
||||
return
|
||||
fi
|
||||
fi
|
||||
SKIPPED+=("GitHub variable $name")
|
||||
warn "skipped GitHub variable $name — gh not ready; set it later"
|
||||
}
|
||||
|
||||
# finish — clear, then a closing summary of everything configured.
|
||||
finish() {
|
||||
_clear
|
||||
printf '\n%s%s ✓ Setup complete%s\n' "$BOLD" "$GREEN" "$RESET"
|
||||
(( ${#WRITTEN_ENV[@]} )) && note "wrote ${#WRITTEN_ENV[@]} value(s) to $ENV_FILE: ${WRITTEN_ENV[*]}"
|
||||
(( ${#WRITTEN_SECRET[@]} )) && note "set ${#WRITTEN_SECRET[@]} GitHub secret(s): ${WRITTEN_SECRET[*]}"
|
||||
if (( ${#SKIPPED[@]} )); then
|
||||
printf '\n'; warn "still to do by hand:"
|
||||
for s in "${SKIPPED[@]}"; do note " - $s"; done
|
||||
fi
|
||||
printf '\n'
|
||||
}
|
||||
|
||||
# ──────────────────────────────────────────────────────────────────────────
|
||||
# STAGES — author this section. One stage() per step the human takes.
|
||||
# Replace the example below. Set the two totals to match the stages you write.
|
||||
# ──────────────────────────────────────────────────────────────────────────
|
||||
|
||||
TOTAL_STAGES=7
|
||||
TOTAL_MINUTES=35
|
||||
|
||||
SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
|
||||
REPO_ROOT="$(cd "$SCRIPT_DIR/../.." && pwd)"
|
||||
PLAN_ROOT="${CPH_SILO_PLAN_ROOT:-$HOME/.cph-silo-plans}"
|
||||
umask 077
|
||||
|
||||
require_value() {
|
||||
local key="$1" value="$2"
|
||||
[[ -n "$value" ]] || { warn "$key is required"; exit 1; }
|
||||
[[ "$value" != *$'\n'* && "$value" != *$'\r'* ]] || {
|
||||
warn "$key must be a single line"
|
||||
exit 1
|
||||
}
|
||||
}
|
||||
|
||||
seed_default() {
|
||||
local key="$1" value="$2"
|
||||
_existing "$key" >/dev/null 2>&1 || write_env "$key" "$value"
|
||||
}
|
||||
|
||||
capture() {
|
||||
local key="$1" prompt="$2"
|
||||
ask "$key" "$prompt"
|
||||
require_value "$key" "${!key}"
|
||||
write_env "$key" "${!key}"
|
||||
}
|
||||
|
||||
capture_secret() {
|
||||
local key="$1" prompt="$2"
|
||||
ask_secret "$key" "$prompt"
|
||||
require_value "$key" "${!key}"
|
||||
write_env "$key" "${!key}"
|
||||
}
|
||||
|
||||
allocate_host_slot() {
|
||||
local allocation local_reserved="" answers_file reserved_port
|
||||
for answers_file in "$PLAN_ROOT"/*/answers.env; do
|
||||
[ -f "$answers_file" ] || continue
|
||||
reserved_port="$(sed -n 's/^HUB_PORT=//p' "$answers_file" | tail -n1)"
|
||||
[[ "$reserved_port" =~ ^[0-9]+$ ]] || continue
|
||||
local_reserved="${local_reserved:+$local_reserved,}$reserved_port"
|
||||
done
|
||||
allocation="$(ssh \
|
||||
-i "$DEPLOY_SSH_KEY" \
|
||||
-p "$DEPLOY_SSH_PORT" \
|
||||
-o BatchMode=yes \
|
||||
-o StrictHostKeyChecking=accept-new \
|
||||
"$DEPLOY_USER@$DEPLOY_HOST" \
|
||||
bash -s -- "$local_reserved" <<'REMOTE'
|
||||
set -euo pipefail
|
||||
local_reserved=",${1:-},"
|
||||
for candidate in $(seq 8788 8999); do
|
||||
reserved=false
|
||||
if [[ "$local_reserved" == *",$candidate,"* ]]; then
|
||||
continue
|
||||
fi
|
||||
for env_file in /srv/curriculum-project-hub/.secrets/*/platform.env; do
|
||||
[ -f "$env_file" ] || continue
|
||||
if [ "$(sed -n "s/^PORT=//p" "$env_file")" = "$candidate" ]; then
|
||||
reserved=true
|
||||
break
|
||||
fi
|
||||
done
|
||||
workspace="/w/$candidate"
|
||||
if [ "$reserved" = false ] && ! ss -H -ltn "sport = :$candidate" | grep -q . && [ ! -e "$workspace" ]; then
|
||||
printf "%s %s\n" "$candidate" "$workspace"
|
||||
exit 0
|
||||
fi
|
||||
done
|
||||
echo "no free Alpha Silo slot in 8788..8999" >&2
|
||||
exit 1
|
||||
REMOTE
|
||||
)"
|
||||
read -r HUB_PORT WORKSPACE_ROOT <<<"$allocation"
|
||||
require_value HUB_PORT "$HUB_PORT"
|
||||
require_value WORKSPACE_ROOT "$WORKSPACE_ROOT"
|
||||
write_env HUB_PORT "$HUB_PORT"
|
||||
write_env WORKSPACE_ROOT "$WORKSPACE_ROOT"
|
||||
}
|
||||
|
||||
banner "New Alpha Silo"
|
||||
|
||||
stage "Organization identity and private plan" 3
|
||||
say "One run creates one Organization's private deployment bundle."
|
||||
ask ORGANIZATION_SLUG "Organization slug (lowercase, max 24 chars; e.g. school-a):"
|
||||
require_value ORGANIZATION_SLUG "$ORGANIZATION_SLUG"
|
||||
[[ "$ORGANIZATION_SLUG" =~ ^[a-z0-9]([a-z0-9-]{0,22}[a-z0-9])?$ ]] || {
|
||||
warn "invalid Organization slug"
|
||||
exit 1
|
||||
}
|
||||
INSTANCE_ID="$ORGANIZATION_SLUG"
|
||||
ORGANIZATION_ID="$ORGANIZATION_SLUG"
|
||||
OUTPUT_DIR="$PLAN_ROOT/$INSTANCE_ID"
|
||||
mkdir -p "$OUTPUT_DIR"
|
||||
chmod 0700 "$OUTPUT_DIR"
|
||||
ENV_FILE="$OUTPUT_DIR/answers.env"
|
||||
touch "$ENV_FILE"
|
||||
chmod 0600 "$ENV_FILE"
|
||||
write_env INSTANCE_ID "$INSTANCE_ID"
|
||||
write_env ORGANIZATION_ID "$ORGANIZATION_ID"
|
||||
write_env ORGANIZATION_SLUG "$ORGANIZATION_SLUG"
|
||||
capture ORGANIZATION_NAME "Organization display name:"
|
||||
|
||||
stage "Host, release, and isolation" 5
|
||||
say "The Alpha host is platform-managed. Port and short workspace path are allocated from live host state."
|
||||
DEPLOY_HOST="${CPH_ALPHA_HOST:-39.107.254.4}"
|
||||
DEPLOY_USER="${CPH_ALPHA_DEPLOY_USER:-root}"
|
||||
DEPLOY_SSH_PORT="${CPH_ALPHA_SSH_PORT:-22}"
|
||||
write_env DEPLOY_HOST "$DEPLOY_HOST"
|
||||
write_env DEPLOY_USER "$DEPLOY_USER"
|
||||
write_env DEPLOY_SSH_PORT "$DEPLOY_SSH_PORT"
|
||||
seed_default DEPLOY_BASE "/srv/curriculum-project-hub"
|
||||
seed_default DEPLOY_SSH_KEY "$HOME/.ssh/id_ed25519"
|
||||
write_env RELEASE_ID "v$(node -p 'require(process.argv[1]).version' "$REPO_ROOT/hub/package.json")"
|
||||
seed_default MEMORY_MAX "16G"
|
||||
seed_default CPU_QUOTA "400%"
|
||||
seed_default TASKS_MAX "512"
|
||||
seed_default CPH_BIN "/usr/local/bin/cph"
|
||||
note "Managed Alpha host: $DEPLOY_USER@$DEPLOY_HOST:$DEPLOY_SSH_PORT"
|
||||
DEPLOY_SSH_KEY="$(_existing DEPLOY_SSH_KEY)"
|
||||
MEMORY_MAX="$(_existing MEMORY_MAX)"
|
||||
CPU_QUOTA="$(_existing CPU_QUOTA)"
|
||||
TASKS_MAX="$(_existing TASKS_MAX)"
|
||||
[ -f "$DEPLOY_SSH_KEY" ] || { warn "managed SSH key is missing: $DEPLOY_SSH_KEY"; exit 1; }
|
||||
if [[ "$(_existing HUB_PORT || true)" =~ ^(878[8-9]|87[9][0-9]|8[89][0-9]{2})$ ]] && \
|
||||
[ "$(_existing WORKSPACE_ROOT || true)" = "/w/$(_existing HUB_PORT)" ]; then
|
||||
HUB_PORT="$(_existing HUB_PORT)"
|
||||
WORKSPACE_ROOT="$(_existing WORKSPACE_ROOT)"
|
||||
note "Keeping allocated host slot: port $HUB_PORT, workspace $WORKSPACE_ROOT"
|
||||
else
|
||||
say "Checking existing Silo environments, listening sockets, and workspace paths..."
|
||||
allocate_host_slot
|
||||
note "Allocated host slot: port $HUB_PORT, workspace $WORKSPACE_ROOT"
|
||||
fi
|
||||
note "Platform ceilings: MemoryMax=$MEMORY_MAX, CPUQuota=$CPU_QUOTA, TasksMax=$TASKS_MAX"
|
||||
|
||||
stage "Dedicated PostgreSQL database" 4
|
||||
say "A PostgreSQL server may be shared, but this Silo gets a distinct login role and database."
|
||||
seed_default DATABASE_HOST "127.0.0.1"
|
||||
seed_default DATABASE_PORT "5432"
|
||||
seed_default DATABASE_NAME "cph_${INSTANCE_ID//-/_}"
|
||||
seed_default DATABASE_USER "cph_${INSTANCE_ID//-/_}"
|
||||
DATABASE_NAME="$(_existing DATABASE_NAME)"
|
||||
if ! _existing DATABASE_PASSWORD >/dev/null 2>&1; then
|
||||
DATABASE_PASSWORD="$(openssl rand -base64 36 | tr -d '\n')"
|
||||
write_env DATABASE_PASSWORD "$DATABASE_PASSWORD"
|
||||
fi
|
||||
note "The generated OPERATE.md uses an interactive/protected SQL path; the password is never put in a command argument."
|
||||
|
||||
stage "Public URL and Feishu app" 9
|
||||
open_url "https://open.feishu.cn/app"
|
||||
say "Create or open the Organization's own app. Copy credentials from Credentials & Basic Info."
|
||||
PUBLIC_BASE_URL="https://${ORGANIZATION_SLUG}.${CPH_ALPHA_BASE_DOMAIN:-educraft.paradigm-edu.net}"
|
||||
write_env PUBLIC_BASE_URL "$PUBLIC_BASE_URL"
|
||||
note "Platform-assigned public URL: $PUBLIC_BASE_URL"
|
||||
capture FEISHU_APP_ID "Feishu App ID:"
|
||||
capture_secret FEISHU_APP_SECRET "Feishu App Secret:"
|
||||
say "Resolving the bot Open ID from Feishu..."
|
||||
FEISHU_BOT_OPEN_ID="$(printf '%s\0%s\0' "$FEISHU_APP_ID" "$FEISHU_APP_SECRET" | node "$SCRIPT_DIR/resolve_feishu_bot.mjs")"
|
||||
write_env FEISHU_BOT_OPEN_ID "$FEISHU_BOT_OPEN_ID"
|
||||
note "Resolved bot identity: $FEISHU_BOT_OPEN_ID"
|
||||
open_url "https://open.feishu.cn/document/server-docs/contact-v3/user/get"
|
||||
step "In the user/get page, click the user_id value picker, select the first OWNER, and copy the returned open_id."
|
||||
capture OWNER_OPEN_ID "OWNER Open ID (ou_...):"
|
||||
capture OWNER_DISPLAY_NAME "OWNER display name:"
|
||||
write_env OWNER_UNION_ID ""
|
||||
say "The exact redirect URL and acceptance steps will be written to OPERATE.md."
|
||||
|
||||
stage "Provider and Alpha limits" 5
|
||||
say "Use a provider credential exclusive to this Organization. Host proxy setup is a separate prerequisite."
|
||||
seed_default PROVIDER_ID "openrouter"
|
||||
seed_default PROVIDER_BASE_URL "https://openrouter.ai/api"
|
||||
seed_default DEFAULT_MODEL "anthropic/claude-sonnet-5"
|
||||
seed_default DEFAULT_ROLE_ID "draft"
|
||||
seed_default DEFAULT_ROLE_LABEL "智能助手"
|
||||
seed_default MAX_TURNS "25"
|
||||
seed_default MAX_CONCURRENT_RUNS "4"
|
||||
seed_default MAX_RUN_SECONDS "900"
|
||||
seed_default HTTP_BODY_LIMIT_BYTES "1048576"
|
||||
seed_default MAX_FILES_PER_MESSAGE "8"
|
||||
seed_default MAX_FILE_BYTES "26214400"
|
||||
seed_default HTTP_REQUESTS_PER_MINUTE "120"
|
||||
seed_default FEISHU_EVENTS_PER_MINUTE "120"
|
||||
capture_secret PROVIDER_AUTH_TOKEN "Provider auth token:"
|
||||
for key in PROVIDER_ID PROVIDER_BASE_URL DEFAULT_MODEL DEFAULT_ROLE_ID DEFAULT_ROLE_LABEL \
|
||||
MAX_TURNS MAX_CONCURRENT_RUNS MAX_RUN_SECONDS HTTP_BODY_LIMIT_BYTES \
|
||||
MAX_FILES_PER_MESSAGE MAX_FILE_BYTES HTTP_REQUESTS_PER_MINUTE FEISHU_EVENTS_PER_MINUTE; do
|
||||
printf -v "$key" '%s' "$(_existing "$key")"
|
||||
done
|
||||
write_env APPROVED_SKILLS "outline,lesson-project,data-processing-spec,typst"
|
||||
note "Platform runtime: OpenRouter, concurrency 4, default education role, curated skills."
|
||||
if ! _existing HUB_SESSION_SECRET >/dev/null 2>&1; then
|
||||
command -v openssl >/dev/null 2>&1 || { warn "openssl is required"; exit 1; }
|
||||
HUB_SESSION_SECRET="$(openssl rand -hex 32)"
|
||||
write_env HUB_SESSION_SECRET "$HUB_SESSION_SECRET"
|
||||
fi
|
||||
|
||||
stage "Render the private deployment bundle" 2
|
||||
say "This renders platform.env, bootstrap.json, deploy.env, nginx.conf and OPERATE.md."
|
||||
command -v node >/dev/null 2>&1 || { warn "Node.js is required to render safely"; exit 1; }
|
||||
node "$SCRIPT_DIR/render_new_silo_bundle.mjs" "$ENV_FILE" "$OUTPUT_DIR"
|
||||
chmod 0700 "$OUTPUT_DIR"
|
||||
chmod 0600 "$OUTPUT_DIR"/*
|
||||
say "Bundle: $OUTPUT_DIR"
|
||||
warn "It contains database, Feishu, provider and session secrets. Never commit or paste it."
|
||||
|
||||
stage "Operator handoff and gates" 7
|
||||
say "The deployment package is an internal retry/audit checkpoint; you do not operate it manually."
|
||||
step "Target: $PUBLIC_BASE_URL → $DEPLOY_HOST:$HUB_PORT"
|
||||
step "Resources: database $DATABASE_NAME, workspace $WORKSPACE_ROOT, service cph-hub-$INSTANCE_ID"
|
||||
warn "Confirmation will create server, database, TLS, and runtime state."
|
||||
if confirm "Deploy this Organization now?"; then
|
||||
bash "$SCRIPT_DIR/apply_new_silo.sh" "$OUTPUT_DIR"
|
||||
else
|
||||
warn "deployment skipped; rerun the wizard later and keep existing answers"
|
||||
fi
|
||||
|
||||
finish
|
||||
Executable
+217
@@ -0,0 +1,217 @@
|
||||
#!/usr/bin/env node
|
||||
|
||||
import { chmod, mkdir, readFile, writeFile } from "node:fs/promises";
|
||||
import { resolve } from "node:path";
|
||||
|
||||
const [answersPath, outputPath] = process.argv.slice(2);
|
||||
if (!answersPath || !outputPath) {
|
||||
throw new Error("usage: render_new_silo_bundle.mjs ANSWERS_ENV OUTPUT_DIR");
|
||||
}
|
||||
|
||||
function parseAnswers(source) {
|
||||
const values = new Map();
|
||||
for (const [index, line] of source.split("\n").entries()) {
|
||||
if (!line || line.startsWith("#")) continue;
|
||||
const separator = line.indexOf("=");
|
||||
if (separator < 1) throw new Error(`invalid answers line ${index + 1}`);
|
||||
const key = line.slice(0, separator);
|
||||
const value = line.slice(separator + 1);
|
||||
if (!/^[A-Z][A-Z0-9_]*$/.test(key)) {
|
||||
throw new Error(`invalid answers key on line ${index + 1}: ${key}`);
|
||||
}
|
||||
if (value.includes("\r") || value.includes("\n")) {
|
||||
throw new Error(`multiline value is not supported: ${key}`);
|
||||
}
|
||||
values.set(key, value);
|
||||
}
|
||||
return values;
|
||||
}
|
||||
|
||||
function required(values, key) {
|
||||
const value = values.get(key);
|
||||
if (!value) throw new Error(`missing required answer: ${key}`);
|
||||
return value;
|
||||
}
|
||||
|
||||
function optional(values, key, fallback = "") {
|
||||
return values.get(key) || fallback;
|
||||
}
|
||||
|
||||
function assertMatch(label, value, pattern) {
|
||||
if (!pattern.test(value)) throw new Error(`invalid ${label}: ${value}`);
|
||||
}
|
||||
|
||||
function envLine(key, value) {
|
||||
if (/[\r\n]/.test(value)) throw new Error(`unsafe newline in ${key}`);
|
||||
return `${key}=${value}`;
|
||||
}
|
||||
|
||||
const answers = parseAnswers(await readFile(resolve(answersPath), "utf8"));
|
||||
const instanceId = required(answers, "INSTANCE_ID");
|
||||
const orgId = required(answers, "ORGANIZATION_ID");
|
||||
const orgSlug = required(answers, "ORGANIZATION_SLUG");
|
||||
const port = required(answers, "HUB_PORT");
|
||||
const workspaceRoot = required(answers, "WORKSPACE_ROOT");
|
||||
const publicBaseUrl = required(answers, "PUBLIC_BASE_URL").replace(/\/$/, "");
|
||||
const domain = new URL(publicBaseUrl).hostname;
|
||||
const databasePassword = required(answers, "DATABASE_PASSWORD");
|
||||
const databaseUrl = `postgresql://${encodeURIComponent(required(answers, "DATABASE_USER"))}:${encodeURIComponent(databasePassword)}@${required(answers, "DATABASE_HOST")}:${required(answers, "DATABASE_PORT")}/${encodeURIComponent(required(answers, "DATABASE_NAME"))}`;
|
||||
|
||||
assertMatch("INSTANCE_ID", instanceId, /^[a-z0-9](?:[a-z0-9-]{0,22}[a-z0-9])?$/);
|
||||
assertMatch("organization slug", orgSlug, /^[a-z0-9](?:[a-z0-9-]*[a-z0-9])?$/);
|
||||
assertMatch("port", port, /^[1-9][0-9]{1,4}$/);
|
||||
assertMatch("database name", required(answers, "DATABASE_NAME"), /^[a-z_][a-z0-9_]*$/);
|
||||
assertMatch("database user", required(answers, "DATABASE_USER"), /^[a-z_][a-z0-9_]*$/);
|
||||
assertMatch("default role id", required(answers, "DEFAULT_ROLE_ID"), /^[a-z][a-z0-9-]*$/);
|
||||
assertMatch("release id", required(answers, "RELEASE_ID"), /^[A-Za-z0-9._-]+$/);
|
||||
if (!publicBaseUrl.startsWith("https://")) throw new Error("PUBLIC_BASE_URL must use https");
|
||||
for (const [label, value] of [
|
||||
["WORKSPACE_ROOT", workspaceRoot],
|
||||
["DEPLOY_BASE", required(answers, "DEPLOY_BASE")],
|
||||
["DEPLOY_SSH_KEY", required(answers, "DEPLOY_SSH_KEY")],
|
||||
["CPH_BIN", required(answers, "CPH_BIN")],
|
||||
]) {
|
||||
if (!value.startsWith("/") || /\s/.test(value)) {
|
||||
throw new Error(`${label} must be an absolute path without whitespace: ${value}`);
|
||||
}
|
||||
}
|
||||
if (Number(port) > 65535) throw new Error(`invalid port: ${port}`);
|
||||
if (Buffer.byteLength(workspaceRoot) > 16) {
|
||||
throw new Error(`WORKSPACE_ROOT exceeds the 16-byte sandbox socket limit: ${workspaceRoot}`);
|
||||
}
|
||||
|
||||
const outputDir = resolve(outputPath);
|
||||
await mkdir(outputDir, { recursive: true, mode: 0o700 });
|
||||
await chmod(outputDir, 0o700);
|
||||
|
||||
const base = required(answers, "DEPLOY_BASE");
|
||||
const release = required(answers, "RELEASE_ID");
|
||||
const releaseHub = `${base}/releases/${release}/hub`;
|
||||
const secretDir = `${base}/.secrets/${instanceId}`;
|
||||
const envPath = `${secretDir}/platform.env`;
|
||||
const keyringPath = `${secretDir}/secret-keyring.json`;
|
||||
const unit = `cph-hub-${instanceId}.service`;
|
||||
|
||||
const platformEnv = [
|
||||
"# Generated by hub/deploy/new_silo.sh. Install root:root mode 0600.",
|
||||
envLine("NODE_ENV", "production"),
|
||||
envLine("DATABASE_URL", databaseUrl),
|
||||
envLine("HUB_SILO_ORGANIZATION_ID", orgId),
|
||||
envLine("HUB_SYSTEMD_UNIT", unit),
|
||||
envLine("CPH_BIN", required(answers, "CPH_BIN")),
|
||||
envLine("HOST", "127.0.0.1"),
|
||||
envLine("PORT", port),
|
||||
envLine("HUB_PROJECT_WORKSPACE_ROOT", workspaceRoot),
|
||||
envLine("HUB_PUBLIC_BASE_URL", publicBaseUrl),
|
||||
envLine("HUB_SESSION_SECRET", required(answers, "HUB_SESSION_SECRET")),
|
||||
envLine("HUB_AGENT_MAX_TURNS", required(answers, "MAX_TURNS")),
|
||||
envLine("HUB_AGENT_MAX_CONCURRENT_RUNS", required(answers, "MAX_CONCURRENT_RUNS")),
|
||||
envLine("HUB_AGENT_MAX_RUN_SECONDS", required(answers, "MAX_RUN_SECONDS")),
|
||||
envLine("HUB_HTTP_BODY_LIMIT_BYTES", required(answers, "HTTP_BODY_LIMIT_BYTES")),
|
||||
envLine("HUB_MAX_FILES_PER_MESSAGE", required(answers, "MAX_FILES_PER_MESSAGE")),
|
||||
envLine("HUB_MAX_FILE_BYTES", required(answers, "MAX_FILE_BYTES")),
|
||||
envLine("HUB_HTTP_REQUESTS_PER_MINUTE", required(answers, "HTTP_REQUESTS_PER_MINUTE")),
|
||||
envLine("HUB_FEISHU_EVENTS_PER_MINUTE", required(answers, "FEISHU_EVENTS_PER_MINUTE")),
|
||||
envLine("HUB_FEISHU_LISTENER_ENABLED", "true"),
|
||||
envLine("HTTP_PROXY", "http://127.0.0.1:7890"),
|
||||
envLine("HTTPS_PROXY", "http://127.0.0.1:7890"),
|
||||
envLine("ALL_PROXY", "socks5h://127.0.0.1:7890"),
|
||||
envLine("NO_PROXY", "127.0.0.1,localhost,::1"),
|
||||
envLine("NODE_USE_ENV_PROXY", "1"),
|
||||
envLine("ANTHROPIC_DEFAULT_SONNET_MODEL", "anthropic/claude-sonnet-5"),
|
||||
envLine("CPH_SANDBOX_EXTRA_DENY_READ", `${envPath}:${keyringPath}`),
|
||||
"",
|
||||
].join("\n");
|
||||
|
||||
const bootstrap = {
|
||||
organization: {
|
||||
id: orgId,
|
||||
slug: orgSlug,
|
||||
name: required(answers, "ORGANIZATION_NAME"),
|
||||
},
|
||||
owner: {
|
||||
openId: required(answers, "OWNER_OPEN_ID"),
|
||||
displayName: required(answers, "OWNER_DISPLAY_NAME"),
|
||||
},
|
||||
feishu: {
|
||||
appId: required(answers, "FEISHU_APP_ID"),
|
||||
appSecret: required(answers, "FEISHU_APP_SECRET"),
|
||||
botOpenId: required(answers, "FEISHU_BOT_OPEN_ID"),
|
||||
},
|
||||
provider: {
|
||||
providerId: required(answers, "PROVIDER_ID"),
|
||||
baseUrl: required(answers, "PROVIDER_BASE_URL"),
|
||||
authToken: required(answers, "PROVIDER_AUTH_TOKEN"),
|
||||
},
|
||||
teams: [],
|
||||
};
|
||||
const ownerUnionId = optional(answers, "OWNER_UNION_ID");
|
||||
if (ownerUnionId) bootstrap.owner.unionId = ownerUnionId;
|
||||
|
||||
const deployEnv = [
|
||||
"# Source this file locally before deploy_platform.sh (contains no app/provider secrets).",
|
||||
envLine("PLATFORM_DEPLOY_HOST", required(answers, "DEPLOY_HOST")),
|
||||
envLine("PLATFORM_DEPLOY_SSH_KEY", required(answers, "DEPLOY_SSH_KEY")),
|
||||
envLine("PLATFORM_DEPLOY_USER", required(answers, "DEPLOY_USER")),
|
||||
envLine("PLATFORM_DEPLOY_PORT", required(answers, "DEPLOY_SSH_PORT")),
|
||||
envLine("PLATFORM_DEPLOY_HUB_PORT", port),
|
||||
envLine("PLATFORM_DEPLOY_BASE", base),
|
||||
envLine("PLATFORM_DEPLOY_RELEASE", release),
|
||||
envLine("PLATFORM_DEPLOY_INSTANCE", instanceId),
|
||||
envLine("PLATFORM_DEPLOY_WORKSPACE_ROOT", workspaceRoot),
|
||||
envLine("PLATFORM_DEPLOY_MEMORY_MAX", required(answers, "MEMORY_MAX")),
|
||||
envLine("PLATFORM_DEPLOY_CPU_QUOTA", required(answers, "CPU_QUOTA")),
|
||||
envLine("PLATFORM_DEPLOY_TASKS_MAX", required(answers, "TASKS_MAX")),
|
||||
envLine("PLATFORM_DEPLOY_HEALTH_URL", `http://127.0.0.1:${port}/api/healthz`),
|
||||
"",
|
||||
].join("\n");
|
||||
|
||||
const nginx = `# Install as /etc/nginx/conf.d/${instanceId}.conf after obtaining TLS certificates.\nserver {\n listen 80;\n server_name ${domain};\n return 301 https://$host$request_uri;\n}\n\nserver {\n listen 443 ssl http2;\n server_name ${domain};\n\n ssl_certificate /etc/letsencrypt/live/${domain}/fullchain.pem;\n ssl_certificate_key /etc/letsencrypt/live/${domain}/privkey.pem;\n\n location / {\n proxy_pass http://127.0.0.1:${port};\n proxy_http_version 1.1;\n proxy_set_header Host $host;\n proxy_set_header X-Real-IP $remote_addr;\n proxy_set_header X-Forwarded-For $proxy_add_x_forwarded_for;\n proxy_set_header X-Forwarded-Proto https;\n }\n}\n`;
|
||||
|
||||
const defaultRolePrompt = `你是一位教育机构智能助手，服务于学校和教培机构的日常管理与协作。
|
||||
## 核心能力
|
||||
**教务管理**：熟悉排课调课、班级管理、课时统计、师资调度等常见管理流程。
|
||||
**教研支持**：理解课程设计、教案编写、例题/变式题、定理证明、随堂练习、阶段性测验、知识点拆解、大纲对标等教学业务概念。
|
||||
**数字化操作**：熟练使用shell命令行进行文件管理、批量处理、脚本编写、文本处理（grep/sed/awk等）、自动化任务；能协助处理Markdown、Typst等文档、表格数据、格式转换等。
|
||||
## 行为准则
|
||||
- **实事求是**：不确定时明确说明，能力边界外的任务如实告知，不为完成目标而编造信息或勉强输出
|
||||
- **简洁优先**：直接给出答案或方案，省略铺垫和客套
|
||||
- **按需展开**：仅在问题复杂或用户明确要求时提供详细说明
|
||||
- **结构清晰**：多步骤内容使用编号，便于飞书阅读
|
||||
- **可操作性**：涉及操作时给出具体命令或步骤
|
||||
保持专业、高效，像一位熟悉业务的同事。
|
||||
`;
|
||||
|
||||
const operate = `# ${instanceId} deployment commands\n\nThis file contains no application/provider secrets. Run commands deliberately; do not source answers.env.\n\n## 1. DNS and Feishu\n\n- Point \`${domain}\` to \`${required(answers, "DEPLOY_HOST")}\`.\n- In the Feishu app, configure redirect URL: \`${publicBaseUrl}/auth/feishu/callback\`.\n- Enable the required bot/message/contact permissions and event subscription described in the customer setup document.\n\n## 2. Database (run as the PostgreSQL administrator)\n\nCreate one role and one database for this Silo. The password is in \`answers.env\`; use an interactive client or a protected SQL file, never a command-line argument.\n\n\`\`\`sql\nCREATE ROLE ${required(answers, "DATABASE_USER")} LOGIN PASSWORD '<copy DATABASE_PASSWORD from answers.env>';\nCREATE DATABASE ${required(answers, "DATABASE_NAME")} OWNER ${required(answers, "DATABASE_USER")};\n\`\`\`\n\n## 3. Publish the immutable release\n\nThe normal deploy script seeds the first-instance secrets and exits 78. That exit is expected only on this first pass.\n\n\`\`\`sh\nset -a; . ./deploy.env; set +a\nbash hub/deploy/deploy_platform.sh\n\`\`\`\n\n## 4. Install the generated secrets\n\nCopy \`platform.env\` and \`bootstrap.json\` to the server through a protected channel. On the server:\n\n\`\`\`sh\ninstall -d -o root -g root -m 0700 '${secretDir}'\ninstall -o root -g root -m 0600 platform.env '${envPath}'\ninstall -o root -g root -m 0600 bootstrap.json '/root/${instanceId}-bootstrap.json'\n# Copy ${keyringPath} to separate off-host recovery storage before continuing.\n\`\`\`\n\n## 5. Migrate, install the stopped service, and bootstrap\n\n\`\`\`sh\nset -a; . '${envPath}'; set +a\nnode '${releaseHub}/node_modules/prisma/build/index.js' migrate deploy --schema '${releaseHub}/prisma/schema.prisma'\nBASE='${base}' HUB_DIR='${releaseHub}' INSTANCE_ID='${instanceId}' WORKSPACE_ROOT='${workspaceRoot}' PORT='${port}' MEMORY_MAX='${required(answers, "MEMORY_MAX")}' CPU_QUOTA='${required(answers, "CPU_QUOTA")}' TASKS_MAX='${required(answers, "TASKS_MAX")}' bash '${releaseHub}/deploy/install_service.sh'\nnode '${releaseHub}/dist/deployment/bootstrap-silo-cli.js' --config-file '/root/${instanceId}-bootstrap.json' --keyring-file '${keyringPath}'\nrm -f '/root/${instanceId}-bootstrap.json'\n\`\`\`\n\n## 6. Runtime role and skills\n\nRuntime role/skill configuration is intentionally separate from the release. Follow NEW_SILO_RUNBOOK.md, staging each approved skill directory outside the immutable release, then use \`agent_config.sh\`. Do not silently copy a local personal skill collection.\n\n## 7. Nginx, start, and acceptance\n\nInstall \`nginx.conf\`, run \`nginx -t\`, reload Nginx, then:\n\n\`\`\`sh\nsystemctl start '${unit}'\nsystemctl is-active '${unit}'\ncurl --fail --silent --show-error 'http://127.0.0.1:${port}/api/healthz'\ncurl --fail --silent --show-error '${publicBaseUrl}/api/healthz'\njournalctl -u '${unit}' --since '-10 min' --no-pager\n\`\`\`\n\nAcceptance requires: Feishu OAuth completes, OWNER and a non-OWNER can @bot, a second group creates a separate project/session, Typst works when that skill is enabled, and restart preserves session cursor. Then take the first off-host backup.\n\n## 8. Later releases\n\nAfter the instance exists, source \`deploy.env\` with the new release id and run \`deploy_platform.sh\`. Never reuse another org's database, secret directory, workspace root, port, service identity, domain, Feishu app, or provider credential.\n`;
|
||||
|
||||
const selectedSkills = optional(answers, "APPROVED_SKILLS");
|
||||
const roleInstructions = `
|
||||
## Appendix: default runtime role
|
||||
|
||||
Copy \`default-role-prompt.md\` to \`/root/${instanceId}-default-role-prompt.md\`.
|
||||
After installing each reviewed skill with \`agent_config.sh install-skill\`, run:
|
||||
|
||||
\`\`\`sh
|
||||
INSTANCE_ID=${JSON.stringify(instanceId)} ENV_FILE=${JSON.stringify(envPath)} HUB_DIR=${JSON.stringify(releaseHub)} bash ${JSON.stringify(`${releaseHub}/deploy/agent_config.sh`)} upsert-role --organization ${JSON.stringify(orgId)} --role ${JSON.stringify(required(answers, "DEFAULT_ROLE_ID"))} --label ${JSON.stringify(required(answers, "DEFAULT_ROLE_LABEL"))} --model ${JSON.stringify(required(answers, "DEFAULT_MODEL"))} --system-prompt-file ${JSON.stringify(`/root/${instanceId}-default-role-prompt.md`)} --tools-json null
|
||||
${selectedSkills ? `INSTANCE_ID=${JSON.stringify(instanceId)} ENV_FILE=${JSON.stringify(envPath)} HUB_DIR=${JSON.stringify(releaseHub)} bash ${JSON.stringify(`${releaseHub}/deploy/agent_config.sh`)} set-role-skills --organization ${JSON.stringify(orgId)} --role ${JSON.stringify(required(answers, "DEFAULT_ROLE_ID"))} --skills ${JSON.stringify(selectedSkills)}
|
||||
` : "# No skills selected in the wizard; set-role-skills remains an explicit operator step.\n"}INSTANCE_ID=${JSON.stringify(instanceId)} ENV_FILE=${JSON.stringify(envPath)} HUB_DIR=${JSON.stringify(releaseHub)} bash ${JSON.stringify(`${releaseHub}/deploy/agent_config.sh`)} list --organization ${JSON.stringify(orgId)}
|
||||
\`\`\`
|
||||
|
||||
Changing a role's model, system prompt, tools or skill selection archives that
|
||||
role's existing sessions by design. Finish this setup before inviting Alpha users.
|
||||
`;
|
||||
|
||||
async function privateWrite(name, contents) {
|
||||
const path = resolve(outputDir, name);
|
||||
await writeFile(path, contents, { encoding: "utf8", mode: 0o600 });
|
||||
await chmod(path, 0o600);
|
||||
}
|
||||
|
||||
await privateWrite("platform.env", platformEnv);
|
||||
await privateWrite("bootstrap.json", `${JSON.stringify(bootstrap, null, 2)}\n`);
|
||||
await privateWrite("deploy.env", deployEnv);
|
||||
await privateWrite("nginx.conf", nginx);
|
||||
await privateWrite("default-role-prompt.md", defaultRolePrompt);
|
||||
await privateWrite("OPERATE.md", `${operate}${roleInstructions}`);
|
||||
|
||||
console.log(`Rendered private Silo bundle: ${outputDir}`);
|
||||
Executable
+27
@@ -0,0 +1,27 @@
|
||||
#!/usr/bin/env node
|
||||
|
||||
const chunks = [];
|
||||
for await (const chunk of process.stdin) chunks.push(chunk);
|
||||
const [appId, appSecret] = Buffer.concat(chunks).toString("utf8").split("\0");
|
||||
if (!appId || !appSecret) throw new Error("Feishu App ID and App Secret are required on stdin");
|
||||
|
||||
const tokenResponse = await fetch("https://open.feishu.cn/open-apis/auth/v3/tenant_access_token/internal", {
|
||||
method: "POST",
|
||||
headers: { "content-type": "application/json; charset=utf-8" },
|
||||
body: JSON.stringify({ app_id: appId, app_secret: appSecret }),
|
||||
});
|
||||
if (!tokenResponse.ok) throw new Error(`Feishu token request failed: HTTP ${tokenResponse.status}`);
|
||||
const tokenPayload = await tokenResponse.json();
|
||||
if (tokenPayload.code !== 0 || typeof tokenPayload.tenant_access_token !== "string") {
|
||||
throw new Error(`Feishu token request failed: ${JSON.stringify(tokenPayload)}`);
|
||||
}
|
||||
|
||||
const botResponse = await fetch("https://open.feishu.cn/open-apis/bot/v3/info", {
|
||||
headers: { authorization: `Bearer ${tokenPayload.tenant_access_token}` },
|
||||
});
|
||||
if (!botResponse.ok) throw new Error(`Feishu bot info request failed: HTTP ${botResponse.status}`);
|
||||
const botPayload = await botResponse.json();
|
||||
if (botPayload.code !== 0 || typeof botPayload.bot?.open_id !== "string" || !botPayload.bot.open_id) {
|
||||
throw new Error(`Feishu bot info request failed: ${JSON.stringify(botPayload)}`);
|
||||
}
|
||||
process.stdout.write(botPayload.bot.open_id);
|
||||
Generated
+2
-2
@@ -1,12 +1,12 @@
|
||||
{
|
||||
"name": "@paradigm/hub",
|
||||
"version": "0.0.10",
|
||||
"version": "0.0.20",
|
||||
"lockfileVersion": 3,
|
||||
"requires": true,
|
||||
"packages": {
|
||||
"": {
|
||||
"name": "@paradigm/hub",
|
||||
"version": "0.0.10",
|
||||
"version": "0.0.20",
|
||||
"dependencies": {
|
||||
"@anthropic-ai/claude-agent-sdk": "^0.3.202",
|
||||
"@fastify/cookie": "^11.0.2",
|
||||
|
||||
+1
-1
@@ -1,6 +1,6 @@
|
||||
{
|
||||
"name": "@paradigm/hub",
|
||||
"version": "0.0.10",
|
||||
"version": "0.0.20",
|
||||
"private": true,
|
||||
"type": "module",
|
||||
"engines": {
|
||||
|
||||
@@ -5,7 +5,7 @@ import { randomBytes } from "node:crypto";
|
||||
import type { PrismaClient } from "@prisma/client";
|
||||
import type { FastifyInstance, FastifyReply, FastifyRequest } from "fastify";
|
||||
import { resolveActiveFeishuApplication } from "../../connections/feishuApplicationConnections.js";
|
||||
import { upsertScopedFeishuIdentity } from "../../feishu/identityNamespace.js";
|
||||
import { upsertScopedFeishuIdentityInTransaction } from "../../feishu/identityNamespace.js";
|
||||
import type { LocalSecretEnvelope } from "../../security/secretEnvelope.js";
|
||||
import {
|
||||
buildAuthorizeUrl,
|
||||
@@ -164,16 +164,54 @@ export async function registerAuthRoutes(app: FastifyInstance, config: AuthRoute
|
||||
const feishuUser = await exchangeCodeForUser(oauthConfig, code);
|
||||
let userId: string;
|
||||
if (statePayload.connectionId !== undefined && statePayload.organizationId !== undefined) {
|
||||
const identity = await upsertScopedFeishuIdentity(config.prisma, {
|
||||
connectionId: statePayload.connectionId,
|
||||
openId: feishuUser.openId,
|
||||
...(feishuUser.unionId !== undefined ? { unionId: feishuUser.unionId } : {}),
|
||||
displayName: feishuUser.displayName,
|
||||
...(feishuUser.avatarUrl !== null ? { avatarUrl: feishuUser.avatarUrl } : {}),
|
||||
const connectionId = statePayload.connectionId;
|
||||
const organizationId = statePayload.organizationId;
|
||||
const identity = await config.prisma.$transaction(async (tx) => {
|
||||
const resolved = await upsertScopedFeishuIdentityInTransaction(tx, {
|
||||
connectionId,
|
||||
expectedOrganizationId: organizationId,
|
||||
openId: feishuUser.openId,
|
||||
...(feishuUser.unionId !== undefined ? { unionId: feishuUser.unionId } : {}),
|
||||
displayName: feishuUser.displayName,
|
||||
...(feishuUser.avatarUrl !== null ? { avatarUrl: feishuUser.avatarUrl } : {}),
|
||||
});
|
||||
const activeMembership = await tx.organizationMembership.findFirst({
|
||||
where: {
|
||||
organizationId,
|
||||
userId: resolved.userId,
|
||||
revokedAt: null,
|
||||
},
|
||||
select: { id: true },
|
||||
});
|
||||
if (activeMembership === null) {
|
||||
const revokedMembership = await tx.organizationMembership.findFirst({
|
||||
where: {
|
||||
organizationId,
|
||||
userId: resolved.userId,
|
||||
revokedAt: { not: null },
|
||||
},
|
||||
select: { id: true },
|
||||
});
|
||||
if (revokedMembership === null) {
|
||||
await tx.organizationMembership.create({
|
||||
data: {
|
||||
organizationId,
|
||||
userId: resolved.userId,
|
||||
role: "MEMBER",
|
||||
},
|
||||
});
|
||||
await tx.auditEntry.create({
|
||||
data: {
|
||||
organizationId,
|
||||
actorUserId: resolved.userId,
|
||||
action: "organization_member.oauth_auto_joined",
|
||||
metadata: { connectionId: resolved.connectionId, role: "MEMBER" },
|
||||
},
|
||||
});
|
||||
}
|
||||
}
|
||||
return resolved;
|
||||
});
|
||||
if (identity.organizationId !== statePayload.organizationId) {
|
||||
throw new HttpError(400, "bad_request", "OAuth identity Organization scope mismatch");
|
||||
}
|
||||
userId = identity.userId;
|
||||
setSessionCookie(reply, config, {
|
||||
userId,
|
||||
@@ -235,6 +273,34 @@ export async function registerAuthRoutes(app: FastifyInstance, config: AuthRoute
|
||||
return reply.status(204).send();
|
||||
});
|
||||
|
||||
app.get("/auth/feishu/complete", async (request, reply) => {
|
||||
const query = request.query as { org?: string };
|
||||
const organizationName = typeof query.org === "string" && query.org.trim() !== ""
|
||||
? query.org.trim()
|
||||
: "当前组织";
|
||||
return reply.type("text/html").send(`<!doctype html>
|
||||
<html lang="zh-CN">
|
||||
<head>
|
||||
<meta charset="utf-8"/>
|
||||
<meta name="viewport" content="width=device-width, initial-scale=1"/>
|
||||
<title>Educraft 登录成功</title>
|
||||
<style>
|
||||
body{font-family:system-ui,sans-serif;display:flex;min-height:100vh;align-items:center;justify-content:center;margin:0;background:#f6f7f9;color:#1a1a1a}
|
||||
.card{background:#fff;padding:2rem 2.5rem;border-radius:12px;box-shadow:0 8px 24px rgba(0,0,0,.08);max-width:25rem;text-align:center}
|
||||
.ok{font-size:3rem;margin:0 0 .5rem}.hint{color:#646a73;line-height:1.6}
|
||||
</style>
|
||||
</head>
|
||||
<body>
|
||||
<main class="card">
|
||||
<p class="ok">✅</p>
|
||||
<h1>登录并加入组织成功</h1>
|
||||
<p>你已加入 ${escapeHtml(organizationName)}。</p>
|
||||
<p class="hint">现在可以关闭本页面，返回飞书群再次 @机器人继续使用。</p>
|
||||
</main>
|
||||
</body>
|
||||
</html>`);
|
||||
});
|
||||
|
||||
app.get("/api/me", async (request, reply) => {
|
||||
try {
|
||||
const auth = await requireSession(request, reply, guardDeps);
|
||||
@@ -363,10 +429,13 @@ async function resolvePostLoginRedirect(
|
||||
revokedAt: null,
|
||||
organization: { status: "ACTIVE" },
|
||||
},
|
||||
select: { organization: { select: { slug: true } } },
|
||||
select: { organization: { select: { slug: true, name: true } } },
|
||||
});
|
||||
if (intended === null) return "/admin?error=not_an_active_org_member";
|
||||
const orgRoot = `/admin/org/${intended.organization.slug}`;
|
||||
if (returnTo === "/admin") {
|
||||
return `/auth/feishu/complete?org=${encodeURIComponent(intended.organization.name)}`;
|
||||
}
|
||||
return returnTo === orgRoot || returnTo.startsWith(`${orgRoot}/`) ? returnTo : orgRoot;
|
||||
}
|
||||
if (returnTo !== "/admin" && returnTo.startsWith("/admin")) {
|
||||
|
||||
+69
-10
@@ -35,7 +35,6 @@ import type { RuntimeSettings } from "../settings/runtime.js";
|
||||
import { currentLockRunId, releaseLock } from "../lock.js";
|
||||
import { createPermissionAuthorizer, type AuthorizationDecision, type PermissionAuthorizer } from "../permission.js";
|
||||
import { writeAudit } from "../audit.js";
|
||||
import { formatRunCostLine } from "../agent/cost.js";
|
||||
import { createAgentSdkStderrSink } from "../agent/diagnostics.js";
|
||||
import { InactiveOrganizationError, lockActiveOrganization } from "../org/status.js";
|
||||
import { StreamingAgentCard } from "./card/streaming-card.js";
|
||||
@@ -85,6 +84,10 @@ interface TriggerDeps {
|
||||
readonly messageBatcherOptions?: MessageBatcherOptions | undefined;
|
||||
readonly triggerQueue?: TriggerQueue | undefined;
|
||||
readonly projectWorkspaceRoot: string;
|
||||
/** Public origin used to build the Silo Organization's Feishu OAuth entrypoint. */
|
||||
readonly publicBaseUrl: string;
|
||||
/** The single Organization this Alpha Silo is fail-closed to serve. */
|
||||
readonly siloOrganizationId: string;
|
||||
/** Alpha Silo policy: never acknowledge work into the process-local queue. */
|
||||
readonly rejectWhenBusy?: boolean | undefined;
|
||||
readonly resourceLimits?: {
|
||||
@@ -133,6 +136,9 @@ export interface TriggerHandler {
|
||||
export function makeTriggerHandler(deps: TriggerDeps): TriggerHandler {
|
||||
const projectWorkspaceRoot = deps.projectWorkspaceRoot.trim();
|
||||
if (projectWorkspaceRoot === "") throw new Error("projectWorkspaceRoot is required");
|
||||
const publicBaseUrl = parsePublicBaseUrl(deps.publicBaseUrl);
|
||||
const siloOrganizationId = deps.siloOrganizationId.trim();
|
||||
if (siloOrganizationId === "") throw new Error("siloOrganizationId is required");
|
||||
const authorizer = deps.authorizer ?? createPermissionAuthorizer(deps.prisma);
|
||||
const runAgent = deps.runAgent ?? defaultRunAgent;
|
||||
const approvalManager = new ApprovalManager();
|
||||
@@ -543,7 +549,7 @@ export function makeTriggerHandler(deps: TriggerDeps): TriggerHandler {
|
||||
: result.status === "failed" && result.error !== undefined
|
||||
? `\u5904\u7406\u5931\u8D25: ${result.error}`
|
||||
: result.text;
|
||||
await card.finish(finalText, { interrupted, footerText: formatRunCostLine(result.costUsd) });
|
||||
await card.finish(finalText, { interrupted });
|
||||
const metadataPatch = sessionMetadataPatch(result.sdkSessionId);
|
||||
if (metadataPatch !== null) {
|
||||
await deps.prisma.agentSession.update({
|
||||
@@ -936,6 +942,15 @@ export function makeTriggerHandler(deps: TriggerDeps): TriggerHandler {
|
||||
await sendText(rt, chatId, "无法识别发送者,拒绝触发。", sendOptionsForTriggerMessage(msg));
|
||||
return;
|
||||
}
|
||||
const organizationResolution = await resolveSingleActiveOrganizationForFeishuUser(senderOpenId);
|
||||
if (organizationResolution.status === "error" && organizationResolution.reason !== "organization_unavailable") {
|
||||
deps.logger.info(
|
||||
{ projectId, senderOpenId, reason: organizationResolution.reason },
|
||||
"feishu trigger: actor onboarding required before project authorization",
|
||||
);
|
||||
await sendText(rt, chatId, organizationResolution.message, sendOptionsForTriggerMessage(msg));
|
||||
return;
|
||||
}
|
||||
const actor = { feishuOpenId: senderOpenId, chatId };
|
||||
const triggerDecision = await authorizer.can({
|
||||
actor,
|
||||
@@ -1083,17 +1098,33 @@ export function makeTriggerHandler(deps: TriggerDeps): TriggerHandler {
|
||||
readonly organizationName: string;
|
||||
readonly role: "OWNER" | "ADMIN" | "MEMBER";
|
||||
}
|
||||
| { readonly status: "error"; readonly message: string }
|
||||
| {
|
||||
readonly status: "error";
|
||||
readonly reason: "identity_missing" | "membership_missing" | "organization_unavailable";
|
||||
readonly message: string;
|
||||
}
|
||||
> {
|
||||
const siloOrganization = await deps.prisma.organization.findFirst({
|
||||
where: { id: siloOrganizationId, status: "ACTIVE" },
|
||||
select: { id: true, slug: true },
|
||||
});
|
||||
if (siloOrganization === null) {
|
||||
return {
|
||||
status: "error",
|
||||
reason: "organization_unavailable",
|
||||
message: "组织当前不可用，请联系 Educraft 运维人员。",
|
||||
};
|
||||
}
|
||||
const identity = await deps.prisma.feishuUserIdentity.findFirst({
|
||||
where: {
|
||||
openId: feishuOpenId,
|
||||
connection: { status: "ACTIVE", organization: { status: "ACTIVE" } },
|
||||
connection: { status: "ACTIVE", organizationId: siloOrganization.id },
|
||||
},
|
||||
select: {
|
||||
user: { select: { organizationMemberships: {
|
||||
where: {
|
||||
revokedAt: null,
|
||||
organizationId: siloOrganization.id,
|
||||
organization: { status: "ACTIVE" },
|
||||
},
|
||||
select: {
|
||||
@@ -1109,19 +1140,34 @@ export function makeTriggerHandler(deps: TriggerDeps): TriggerHandler {
|
||||
where: { feishuOpenId },
|
||||
select: {
|
||||
organizationMemberships: {
|
||||
where: { revokedAt: null, organization: { status: "ACTIVE" } },
|
||||
where: {
|
||||
revokedAt: null,
|
||||
organizationId: siloOrganization.id,
|
||||
organization: { status: "ACTIVE" },
|
||||
},
|
||||
select: { role: true, organization: { select: { id: true, name: true } } },
|
||||
orderBy: { createdAt: "asc" },
|
||||
},
|
||||
},
|
||||
})
|
||||
: null);
|
||||
if (user === null) return { status: "error", message: "请先登录并加入组织后，再绑定项目。" };
|
||||
if (user.organizationMemberships.length === 0) {
|
||||
return { status: "error", message: "你还不属于任何可用组织，请联系组织管理员。" };
|
||||
if (user === null) {
|
||||
const loginUrl = new URL(
|
||||
`/auth/feishu/${encodeURIComponent(siloOrganization.slug)}`,
|
||||
publicBaseUrl,
|
||||
).toString();
|
||||
return {
|
||||
status: "error",
|
||||
reason: "identity_missing",
|
||||
message: `请先通过飞书登录并加入组织：${loginUrl}\n完成后返回群聊重试。`,
|
||||
};
|
||||
}
|
||||
if (user.organizationMemberships.length > 1) {
|
||||
return { status: "error", message: "你属于多个组织。请先从组织后台选择项目绑定，或等待多组织选择入口。" };
|
||||
if (user.organizationMemberships.length === 0) {
|
||||
return {
|
||||
status: "error",
|
||||
reason: "membership_missing",
|
||||
message: "你尚未加入该组织，或成员资格已被移除。请联系组织管理员。",
|
||||
};
|
||||
}
|
||||
const membership = user.organizationMemberships[0]!;
|
||||
return {
|
||||
@@ -1184,6 +1230,19 @@ export function makeTriggerHandler(deps: TriggerDeps): TriggerHandler {
|
||||
return Object.assign(onMessage, { onCardAction, approvalManager });
|
||||
}
|
||||
|
||||
function parsePublicBaseUrl(raw: string): URL {
|
||||
const value = raw.trim();
|
||||
if (value === "") throw new Error("publicBaseUrl is required");
|
||||
const url = new URL(value);
|
||||
if (url.protocol !== "http:" && url.protocol !== "https:") {
|
||||
throw new Error("publicBaseUrl must use http or https");
|
||||
}
|
||||
if (url.username !== "" || url.password !== "" || url.search !== "" || url.hash !== "" || url.pathname !== "/") {
|
||||
throw new Error("publicBaseUrl must be an origin without credentials, path, query, or fragment");
|
||||
}
|
||||
return url;
|
||||
}
|
||||
|
||||
interface SessionMetadata {
|
||||
readonly claudeSessionId?: string | undefined;
|
||||
}
|
||||
|
||||
@@ -160,6 +160,8 @@ export async function startHub(): Promise<void> {
|
||||
settings: runtimeSettings,
|
||||
logger: app.log,
|
||||
projectWorkspaceRoot,
|
||||
publicBaseUrl,
|
||||
siloOrganizationId: siloOrganization.id,
|
||||
rejectWhenBusy: true,
|
||||
resourceLimits: { maxFilesPerMessage, maxBytesPerFile },
|
||||
allowLegacyFeishuIdentity: false,
|
||||
|
||||
@@ -267,9 +267,6 @@ describe("admin auth + org API guards", () => {
|
||||
openId: "ou_scoped_user",
|
||||
displayName: "Invited User",
|
||||
});
|
||||
await prisma.organizationMembership.create({
|
||||
data: { organizationId: DEFAULT_ORG_ID, userId: identity.userId, role: "ADMIN" },
|
||||
});
|
||||
await seedTestOrganization("org_scoped_other", "scoped-other");
|
||||
await prisma.organizationMembership.create({
|
||||
data: { organizationId: "org_scoped_other", userId: identity.userId, role: "ADMIN" },
|
||||
@@ -317,7 +314,7 @@ describe("admin auth + org API guards", () => {
|
||||
expect(me.statusCode).toBe(200);
|
||||
expect(me.json()).toMatchObject({
|
||||
user: { id: identity.userId, displayName: "Scoped User" },
|
||||
organizations: [expect.objectContaining({ slug: "test-default", role: "ADMIN" })],
|
||||
organizations: [expect.objectContaining({ slug: "test-default", role: "MEMBER" })],
|
||||
});
|
||||
expect((me.json() as { organizations: unknown[] }).organizations).toHaveLength(1);
|
||||
const crossOrganization = await app.inject({
|
||||
@@ -331,6 +328,32 @@ describe("admin auth + org API guards", () => {
|
||||
where: { id: identity.identityId },
|
||||
select: { unionId: true },
|
||||
})).resolves.toEqual({ unionId: "on_scoped_union" });
|
||||
await expect(prisma.auditEntry.count({
|
||||
where: {
|
||||
organizationId: DEFAULT_ORG_ID,
|
||||
actorUserId: identity.userId,
|
||||
action: "organization_member.oauth_auto_joined",
|
||||
},
|
||||
})).resolves.toBe(1);
|
||||
|
||||
const defaultStart = await app.inject({ method: "GET", url: "/auth/feishu/test-default" });
|
||||
const defaultAuthorize = new URL(String(defaultStart.headers.location));
|
||||
const defaultState = defaultAuthorize.searchParams.get("state");
|
||||
expect(defaultState).not.toBeNull();
|
||||
const defaultCallback = await app.inject({
|
||||
method: "GET",
|
||||
url: `/auth/feishu/callback?code=ok&state=${encodeURIComponent(defaultState!)}`,
|
||||
headers: { cookie: cookiePair(defaultStart.headers["set-cookie"], OAUTH_STATE_COOKIE_NAME) },
|
||||
});
|
||||
expect(defaultCallback.statusCode).toBe(302);
|
||||
expect(defaultCallback.headers.location).toBe(
|
||||
"/auth/feishu/complete?org=Test%20Default%20Organization",
|
||||
);
|
||||
const complete = await app.inject({ method: "GET", url: defaultCallback.headers.location! });
|
||||
expect(complete.statusCode).toBe(200);
|
||||
expect(complete.headers["content-type"]).toContain("text/html");
|
||||
expect(complete.body).toContain("登录并加入组织成功");
|
||||
expect(complete.body).toContain("Test Default Organization");
|
||||
|
||||
await connections.disable({ organizationId: DEFAULT_ORG_ID, actorUserId: "scoped-owner" });
|
||||
const revoked = await app.inject({ method: "GET", url: "/api/me", headers: { cookie: sessionCookie } });
|
||||
@@ -340,6 +363,65 @@ describe("admin auth + org API guards", () => {
|
||||
}
|
||||
});
|
||||
|
||||
it("does not restore a revoked Organization membership during scoped OAuth", async () => {
|
||||
await seedUser("revoked-owner", "legacy_revoked_owner", "OWNER");
|
||||
const connections = new FeishuApplicationConnectionService(prisma, testSecretEnvelope, async () => {});
|
||||
const connection = await connections.rotateCustomerApplication({
|
||||
organizationId: DEFAULT_ORG_ID,
|
||||
actorUserId: "revoked-owner",
|
||||
appId: "cli_revoked_oauth",
|
||||
appSecret: "revoked-oauth-secret",
|
||||
botOpenId: "ou_revoked_bot",
|
||||
});
|
||||
const identity = await upsertScopedFeishuIdentity(prisma, {
|
||||
connectionId: connection.id,
|
||||
openId: "ou_revoked_user",
|
||||
displayName: "Revoked User",
|
||||
});
|
||||
await prisma.organizationMembership.create({
|
||||
data: {
|
||||
organizationId: DEFAULT_ORG_ID,
|
||||
userId: identity.userId,
|
||||
role: "MEMBER",
|
||||
revokedAt: new Date(),
|
||||
},
|
||||
});
|
||||
const fetchImpl = vi.fn(async (input: RequestInfo | URL) => {
|
||||
const url = String(input);
|
||||
if (url.includes("/oauth/token")) {
|
||||
return Response.json({ code: 0, access_token: "revoked-user-token" });
|
||||
}
|
||||
if (url.includes("/user_info")) {
|
||||
return Response.json({
|
||||
code: 0,
|
||||
data: { open_id: "ou_revoked_user", name: "Revoked User" },
|
||||
});
|
||||
}
|
||||
throw new Error(`unexpected ${url}`);
|
||||
});
|
||||
const app = await buildApp(fetchImpl as unknown as typeof fetch);
|
||||
try {
|
||||
const start = await app.inject({ method: "GET", url: "/auth/feishu/test-default" });
|
||||
const authorize = new URL(String(start.headers.location));
|
||||
const state = authorize.searchParams.get("state");
|
||||
expect(state).not.toBeNull();
|
||||
const callback = await app.inject({
|
||||
method: "GET",
|
||||
url: `/auth/feishu/callback?code=ok&state=${encodeURIComponent(state!)}`,
|
||||
headers: { cookie: cookiePair(start.headers["set-cookie"], OAUTH_STATE_COOKIE_NAME) },
|
||||
});
|
||||
expect(callback.statusCode).toBe(302);
|
||||
await expect(prisma.organizationMembership.count({
|
||||
where: { organizationId: DEFAULT_ORG_ID, userId: identity.userId, revokedAt: null },
|
||||
})).resolves.toBe(0);
|
||||
await expect(prisma.auditEntry.count({
|
||||
where: { action: "organization_member.oauth_auto_joined", actorUserId: identity.userId },
|
||||
})).resolves.toBe(0);
|
||||
} finally {
|
||||
await app.close();
|
||||
}
|
||||
});
|
||||
|
||||
it("unknown org slug returns 404 for admin", async () => {
|
||||
await seedUser("u-admin", "ou_admin", "ADMIN");
|
||||
const app = await buildApp();
|
||||
|
||||
@@ -3,7 +3,15 @@ import { tmpdir } from "node:os";
|
||||
import { dirname, join } from "node:path";
|
||||
import { Readable } from "node:stream";
|
||||
import { describe, it, expect, beforeEach, afterEach, afterAll, vi } from "vitest";
|
||||
import { DEFAULT_ORG_ID, prisma, resetDb, mockFeishuRuntime, seedProject, silentLogger } from "./helpers.js";
|
||||
import {
|
||||
DEFAULT_ORG_ID,
|
||||
prisma,
|
||||
resetDb,
|
||||
mockFeishuRuntime,
|
||||
seedProject,
|
||||
seedTestOrganization,
|
||||
silentLogger,
|
||||
} from "./helpers.js";
|
||||
import { InMemoryModelRegistry } from "../../src/agent/models.js";
|
||||
import { createSlashCommandRegistry } from "../../src/feishu/slashCommands.js";
|
||||
import { makeTriggerHandler as makeProductionTriggerHandler, extractPrompt } from "../../src/feishu/trigger.js";
|
||||
@@ -24,6 +32,8 @@ type TestTriggerDeps = Omit<Parameters<typeof makeProductionTriggerHandler>[0],
|
||||
function makeTriggerHandler(deps: TestTriggerDeps): ReturnType<typeof makeProductionTriggerHandler> {
|
||||
return makeProductionTriggerHandler({
|
||||
projectWorkspaceRoot: "/tmp",
|
||||
publicBaseUrl: "https://educraft.example.test",
|
||||
siloOrganizationId: DEFAULT_ORG_ID,
|
||||
allowLegacyFeishuIdentity: true,
|
||||
...deps,
|
||||
});
|
||||
@@ -158,7 +168,8 @@ describe("trigger full lifecycle (integration)", () => {
|
||||
msgType: "interactive",
|
||||
replyInThread: undefined,
|
||||
});
|
||||
expect(rt.sentTexts.some((text) => text.includes("mock response") && text.includes("本次成本: $0.0023"))).toBe(true);
|
||||
expect(rt.sentTexts.some((text) => text.includes("mock response"))).toBe(true);
|
||||
expect(rt.sentTexts.some((text) => text.includes("本次成本"))).toBe(false);
|
||||
expect(runAgentCalls).toHaveLength(1);
|
||||
expect(runAgentCalls[0]?.providerProxyEnv).toMatchObject({
|
||||
ANTHROPIC_BASE_URL: "http://127.0.0.1:12345",
|
||||
@@ -386,6 +397,18 @@ describe("trigger full lifecycle (integration)", () => {
|
||||
role: "EDIT",
|
||||
},
|
||||
});
|
||||
await prisma.user.createMany({
|
||||
data: [
|
||||
{ id: "u-speaker-alice", feishuOpenId: "ou_alice", displayName: "Alice" },
|
||||
{ id: "u-speaker-bob", feishuOpenId: "ou_bob", displayName: "Bob" },
|
||||
],
|
||||
});
|
||||
await prisma.organizationMembership.createMany({
|
||||
data: [
|
||||
{ organizationId: DEFAULT_ORG_ID, userId: "u-speaker-alice", role: "MEMBER" },
|
||||
{ organizationId: DEFAULT_ORG_ID, userId: "u-speaker-bob", role: "MEMBER" },
|
||||
],
|
||||
});
|
||||
const trigger = makeTriggerHandler({ prisma, settings, logger: silentLogger, runAgent, messageBatcherOptions: { maxMessages: 1 } });
|
||||
|
||||
await trigger(makeEvent("chat-speaker", "@_user_1 Alice 的需求", "ou_alice"), rt);
|
||||
@@ -626,6 +649,66 @@ describe("trigger full lifecycle (integration)", () => {
|
||||
expect(runs).toHaveLength(0);
|
||||
});
|
||||
|
||||
it("gives an unknown user the scoped login URL in an already-bound chat", async () => {
|
||||
await seedProject("proj-bound-unknown", "chat-bound-unknown");
|
||||
const trigger = makeTriggerHandler({
|
||||
prisma,
|
||||
settings,
|
||||
logger: silentLogger,
|
||||
runAgent,
|
||||
allowLegacyFeishuIdentity: false,
|
||||
messageBatcherOptions: { maxMessages: 1 },
|
||||
});
|
||||
|
||||
await trigger(makeEvent("chat-bound-unknown", "@_user_1 写教案", "ou_bound_unknown"), rt);
|
||||
|
||||
expect(rt.sentTexts).toContain(
|
||||
"请先通过飞书登录并加入组织：https://educraft.example.test/auth/feishu/test-default\n" +
|
||||
"完成后返回群聊重试。",
|
||||
);
|
||||
expect(rt.sentTexts).not.toContain("无权限触发。");
|
||||
expect(runAgentCalls).toHaveLength(0);
|
||||
});
|
||||
|
||||
it("tells a logged-in non-member to contact the administrator in an already-bound chat", async () => {
|
||||
await seedProject("proj-bound-non-member", "chat-bound-non-member");
|
||||
await seedScopedIdentityWithoutMembership("bound-non-member", "ou_bound_non_member");
|
||||
const trigger = makeTriggerHandler({
|
||||
prisma,
|
||||
settings,
|
||||
logger: silentLogger,
|
||||
runAgent,
|
||||
allowLegacyFeishuIdentity: false,
|
||||
messageBatcherOptions: { maxMessages: 1 },
|
||||
});
|
||||
|
||||
await trigger(makeEvent("chat-bound-non-member", "@_user_1 写教案", "ou_bound_non_member"), rt);
|
||||
|
||||
expect(rt.sentTexts).toContain(
|
||||
"你尚未加入该组织，或成员资格已被移除。请联系组织管理员。",
|
||||
);
|
||||
expect(rt.sentTexts).not.toContain("无权限触发。");
|
||||
expect(runAgentCalls).toHaveLength(0);
|
||||
});
|
||||
|
||||
it("keeps generic project denial for an Organization member without project permission", async () => {
|
||||
await seedProject("proj-bound-read-only", "chat-bound-read-only", { role: "READ" });
|
||||
const trigger = makeTriggerHandler({
|
||||
prisma,
|
||||
settings,
|
||||
logger: silentLogger,
|
||||
runAgent,
|
||||
messageBatcherOptions: { maxMessages: 1 },
|
||||
});
|
||||
|
||||
await trigger(makeEvent("chat-bound-read-only", "@_user_1 写教案"), rt);
|
||||
|
||||
expect(rt.sentTexts).toContain("无权限触发。");
|
||||
expect(rt.sentTexts.join("\n")).not.toContain("/auth/feishu/");
|
||||
expect(rt.sentTexts.join("\n")).not.toContain("尚未加入该组织");
|
||||
expect(runAgentCalls).toHaveLength(0);
|
||||
});
|
||||
|
||||
it.each(["SUSPENDED", "ARCHIVED"] as const)(
|
||||
"rejects triggers and resume commands when the organization is %s",
|
||||
async (status) => {
|
||||
@@ -922,18 +1005,62 @@ describe("trigger full lifecycle (integration)", () => {
|
||||
await expect(readdir(join(workspaceRoot, ".cph-staging"))).resolves.toEqual([]);
|
||||
});
|
||||
|
||||
it("does not create a run for unbound chats and asks unknown users to log in", async () => {
|
||||
it("does not create a run for unbound chats and gives unknown users the scoped login URL", async () => {
|
||||
await seedProject("proj-4", "chat-4");
|
||||
const trigger = makeTriggerHandler({ prisma, settings, logger: silentLogger, runAgent, messageBatcherOptions: { maxMessages: 1 } });
|
||||
|
||||
await trigger(makeEvent("chat-UNKNOWN", "@_user_1 写教案", "ou_unknown_user"), rt);
|
||||
|
||||
expect(rt.sentTexts).toContain("请先登录并加入组织后，再绑定项目。");
|
||||
expect(rt.sentTexts).toContain(
|
||||
"请先通过飞书登录并加入组织：https://educraft.example.test/auth/feishu/test-default\n" +
|
||||
"完成后返回群聊重试。",
|
||||
);
|
||||
expect(rt.sentCards).toHaveLength(0);
|
||||
const runs = await prisma.agentRun.findMany();
|
||||
expect(runs).toHaveLength(0);
|
||||
});
|
||||
|
||||
it("distinguishes a scoped Feishu identity that has not joined the Silo Organization", async () => {
|
||||
await seedScopedIdentityWithoutMembership("unbound-non-member", "ou_logged_in_not_member");
|
||||
const trigger = makeTriggerHandler({
|
||||
prisma,
|
||||
settings,
|
||||
logger: silentLogger,
|
||||
runAgent,
|
||||
allowLegacyFeishuIdentity: false,
|
||||
messageBatcherOptions: { maxMessages: 1 },
|
||||
});
|
||||
|
||||
await trigger(makeEvent("chat-unbound", "@_user_1 写教案", "ou_logged_in_not_member"), rt);
|
||||
|
||||
expect(rt.sentTexts).toContain(
|
||||
"你尚未加入该组织，或成员资格已被移除。请联系组织管理员。",
|
||||
);
|
||||
expect(rt.sentTexts.join("\n")).not.toContain("/auth/feishu/");
|
||||
await expect(prisma.agentRun.count()).resolves.toBe(0);
|
||||
});
|
||||
|
||||
it("encodes the configured Organization slug in the OAuth login URL", async () => {
|
||||
const encodedOrgId = "org_url_encoding";
|
||||
await seedTestOrganization(encodedOrgId, "school east/数学?");
|
||||
const trigger = makeTriggerHandler({
|
||||
prisma,
|
||||
settings,
|
||||
logger: silentLogger,
|
||||
runAgent,
|
||||
siloOrganizationId: encodedOrgId,
|
||||
publicBaseUrl: "https://school.example.test/",
|
||||
messageBatcherOptions: { maxMessages: 1 },
|
||||
});
|
||||
|
||||
await trigger(makeEvent("chat-unbound", "@_user_1 写教案", "ou_unknown_encoded"), rt);
|
||||
|
||||
expect(rt.sentTexts.join("\n")).toContain(
|
||||
"https://school.example.test/auth/feishu/school%20east%2F%E6%95%B0%E5%AD%A6%3F",
|
||||
);
|
||||
expect(rt.sentTexts.join("\n")).not.toContain("school east/数学?");
|
||||
});
|
||||
|
||||
it("ignores messages without @bot mention", async () => {
|
||||
await seedProject("proj-5", "chat-5");
|
||||
const trigger = makeTriggerHandler({ prisma, settings, logger: silentLogger, runAgent, messageBatcherOptions: { maxMessages: 1 } });
|
||||
@@ -1430,6 +1557,28 @@ async function seedOnboardingUser(id: string, feishuOpenId: string, role: "OWNER
|
||||
});
|
||||
}
|
||||
|
||||
async function seedScopedIdentityWithoutMembership(id: string, openId: string): Promise<void> {
|
||||
const connectionId = `feishu-connection-${id}`;
|
||||
await prisma.organizationFeishuApplicationConnection.create({
|
||||
data: {
|
||||
id: connectionId,
|
||||
organizationId: DEFAULT_ORG_ID,
|
||||
appIdentityFingerprint: `fingerprint-${id}`,
|
||||
status: "ACTIVE",
|
||||
},
|
||||
});
|
||||
await prisma.user.create({
|
||||
data: {
|
||||
id: `user-${id}`,
|
||||
displayName: "Logged in user",
|
||||
feishuOpenId: `legacy-${openId}`,
|
||||
feishuIdentities: {
|
||||
create: { connectionId, openId },
|
||||
},
|
||||
},
|
||||
});
|
||||
}
|
||||
|
||||
async function tempWorkspaceRoot(): Promise<string> {
|
||||
const root = await mkdtemp(join(tmpdir(), "cph-trigger-onboarding-"));
|
||||
workspaceRoots.push(root);
|
||||
|
||||
@@ -110,6 +110,8 @@ describe("Feishu approval cards", () => {
|
||||
logger: silentLogger(),
|
||||
authorizer: allowAllAuthorizer(),
|
||||
projectWorkspaceRoot: "/tmp",
|
||||
publicBaseUrl: "https://educraft.example.test",
|
||||
siloOrganizationId: "org_test_default",
|
||||
runAgent: async () => ({
|
||||
status: "completed",
|
||||
text: "",
|
||||
|
||||
@@ -103,6 +103,8 @@ async function triggerWithRunAgent(
|
||||
logger: rt.logger,
|
||||
authorizer: allowAllAuthorizer(),
|
||||
projectWorkspaceRoot: "/tmp",
|
||||
publicBaseUrl: "https://educraft.example.test",
|
||||
siloOrganizationId: "org_test_default",
|
||||
runAgent,
|
||||
messageBatcherOptions: { maxMessages: 1 },
|
||||
});
|
||||
@@ -254,6 +256,19 @@ function mockPrisma(): PrismaClient {
|
||||
const session = { id: "session-1", metadata: {} };
|
||||
|
||||
const client = {
|
||||
organization: {
|
||||
findFirst: vi.fn(async () => ({ id: "org_test_default", slug: "test-default" })),
|
||||
},
|
||||
feishuUserIdentity: {
|
||||
findFirst: vi.fn(async () => ({
|
||||
user: {
|
||||
organizationMemberships: [{
|
||||
role: "OWNER",
|
||||
organization: { id: "org_test_default", name: "Test Organization" },
|
||||
}],
|
||||
},
|
||||
})),
|
||||
},
|
||||
feishuEventReceipt: {
|
||||
findUnique: vi.fn(async () => null),
|
||||
create: vi.fn(async () => ({ id: "receipt-1" })),
|
||||
|
||||
+1
-1
@@ -49,7 +49,7 @@ agent 不得用预训练先验脑补本领域(领域很新,无先验);prose 是
|
||||
|
||||
### 命名
|
||||
|
||||
- **模块 / 命名空间**:PascalCase,对应分层,如 `Spec.System.Run`、`Spec.Courseware.Validity`。
|
||||
- **模块 / 命名空间**:PascalCase,对应分层,如 `Spec.System.Agent.Run`、`Spec.Courseware.Validity`。
|
||||
- **类型**:PascalCase。
|
||||
- **谓词 / `Prop`**:用意图清晰的命名,如 `Legal…`、`ValidTransition`、`Can…`。
|
||||
- **文件粒度**:原则上"一个带独立不变式的概念一个文件"。
|
||||
|
||||
@@ -16,6 +16,6 @@ import Spec.Courseware.Open
|
||||
- **`Check`** —— checker 语义:`Severity` + 6 类诊断 + **合法 lesson = 无 error 级
|
||||
诊断**(模型外设施诊断以抽象谓词 + `Oracle` 表示);检查管线的 5 阶段、序、compile
|
||||
门控。
|
||||
- **`Open`** —— 留白骨架(核心关系 OPEN,已 surface 不臆造):题库 `QuestionBank`、
|
||||
- **`Open`** —— OPEN 骨架(核心关系 OPEN,已 surface):题库 `QuestionBank`、
|
||||
课程编排 `Course`。
|
||||
-/
|
||||
|
||||
@@ -6,7 +6,7 @@ import Spec.Courseware.Export.Render
|
||||
|
||||
产品里"站在 Lean 位置"的 rule-based checker,语义在此沉淀(ADR-0010,经 ADR-0012
|
||||
修订)。它对 lesson 提诊断,每条有**分类**(`DiagKind`)与**严重级别**(`Severity`)。
|
||||
本模块:钉级别类型(二分);钉 7 类诊断各自的含义与级别,并把"**合法 lesson = 无
|
||||
定级别类型(二分);定 7 类诊断各自的含义与级别,并把"**合法 lesson = 无
|
||||
error 级诊断**"建成判定(ADR-0005 deferred 的"完整合法判定"的回填);对**模型外设施**
|
||||
型诊断(typst 编过否、数据合 schema 否)用**抽象谓词 + `Oracle` 实现边界**表示——契约
|
||||
说"存在这条诊断、什么意思、什么级别",真值由实现提供,不在 Lean 内计算(不内嵌 typst
|
||||
@@ -50,7 +50,7 @@ inductive DiagKind where
|
||||
|
||||
/-- 每类诊断的**严重级别**(`PINNED`, ADR-0010)。六类 `error`(阻断);**唯
|
||||
`renderIgnored` 为 `warning`**——ADR-0005 种子规则"缺渲染 ⇒ warning,不阻断导出"。
|
||||
钉成全函数使"哪类阻断"成为可引用、可对齐的事实(实现侧 `DiagCode` 级别据此对齐)。 -/
|
||||
全函数使"哪类阻断"成为可引用、可对齐的事实(实现侧 `DiagCode` 级别据此对齐)。 -/
|
||||
def DiagKind.severity : DiagKind → Severity
|
||||
| .partPathMissing => .error
|
||||
| .unknownKind => .error
|
||||
|
||||
@@ -5,8 +5,8 @@ import Spec.Courseware.Check.Diagnostic
|
||||
|
||||
checker 的 `check` 按**固定顺序**跑五个阶段,逐阶段收集诊断;`compile` 阶段有**门控**。
|
||||
顺序与门控是契约——它决定用户看到哪些诊断(藏在缺文件背后的语法错,在文件补齐前不
|
||||
显示,这是有意的)。每阶段的**算法**不进 Lean(宪法第 5 条深度上限):只钉**阶段、序、
|
||||
门控**。阶段对应上游模块:`load`←`cph-model`;`structural`←part 路径/未知 kind;
|
||||
显示,这是有意的)。每阶段的**算法**不进 Lean(深度上限:只定**阶段、序、
|
||||
门控**)。阶段对应上游模块:`load`←`cph-model`;`structural`←part 路径/未知 kind;
|
||||
`schema`←`cph-schema`;`compile`←`cph-typst`(模型外设施);`coverage`←`renderIgnored`。
|
||||
-/
|
||||
|
||||
|
||||
@@ -2,7 +2,7 @@
|
||||
# Artifact —— export target 的产物(ADR-0009 / 0011)
|
||||
|
||||
ADR-0009:一个 export target 是**一次 build**,产出一个**有类型的产物**。ADR-0011
|
||||
钉死:产物是**带字段的 ADT**——"产物到底指什么"(单文件落在哪 / 一棵树产出哪些文件)
|
||||
固定:产物是**带字段的 ADT**——"产物到底指什么"(单文件落在哪 / 一棵树产出哪些文件)
|
||||
是不好猜的领域语义,必须写进字段 + doc,而非抹成两个空构造子。路径/glob 用 `String`
|
||||
承载并由 doc 赋义(它们就是文本),不复刻文件系统类型。
|
||||
-/
|
||||
|
||||
@@ -4,7 +4,7 @@ import Spec.Courseware.Export.Artifact
|
||||
/-!
|
||||
# Render —— export target = artifact + 有序 typed steps(ADR-0009 / 0011)
|
||||
|
||||
ADR-0009:export target 是一次 build,产出一个有类型的 `Artifact`。ADR-0011 钉死 build
|
||||
ADR-0009:export target 是一次 build,产出一个有类型的 `Artifact`。ADR-0011 固定 build
|
||||
的**形状**:一个 target 是 `artifact` + 一串**有序 typed step**。
|
||||
|
||||
- `typstCompile template` —— 把**模板文件**(如 `exports/student.typ`)编译成产物。它是
|
||||
@@ -20,7 +20,7 @@ ADR-0009:export target 是一次 build,产出一个有类型的 `Artifact`。ADR
|
||||
|
||||
**shell step 的执行语义(ADR-0013)。** `shell` 不再只是占位:它**会被执行**,语义是把
|
||||
`run` 交给平台 shell、以**工程根为工作目录**运行,产物由被调外部工具自己写出(框架不装配
|
||||
内容)。三条边界是真分歧点,故钉契约:
|
||||
内容)。三条边界是真分歧点,故定为契约:
|
||||
1. **opt-in by construction** —— 任意命令执行只在用户**显式** build 一个 shell target 时发生,
|
||||
绝不在 `check` 里跑。`check` 只校验结构(lesson 是否合法),不执行外部工具、不验其产物。
|
||||
2. **失败归属** —— shell step 退出非零是一次 **build-过程失败**,不是 lesson 的合法性缺陷;
|
||||
@@ -46,7 +46,7 @@ namespace Spec.Courseware
|
||||
variable (P : Primitives)
|
||||
|
||||
/-- 一个 build **step**(`PINNED` typed, ADR-0011;可扩展)。MVP 仅一个 `typstCompile`;
|
||||
`steps` 是 list 因为 FileTree / 第三方 build 会需多步。刻意不把模板内部、shell 命令的
|
||||
`steps` 是 list 因为 FileTree / 第三方 build 会需多步。不把模板内部、shell 命令的
|
||||
解析结构写进来(实现细节, ADR-0011 OPEN)。 -/
|
||||
inductive Step where
|
||||
/-- 编译模板文件 `template`(相对工程根)成产物;框架注入 manifest。typed 的理由:
|
||||
|
||||
@@ -7,7 +7,7 @@ import Spec.Courseware.Model.Info
|
||||
/-!
|
||||
# Courseware.Model —— 工程文件的内容模型
|
||||
|
||||
留白基元(`Primitives`)、富内容锚点(`RichContent`)、原子单位(`Element`)、单节课
|
||||
基元(`Primitives`)、富内容锚点(`RichContent`)、原子单位(`Element`)、单节课
|
||||
(`Lesson`)、课时元信息(`Info`:canonical author 为列表 vs `RawInfo` 撰写态)。
|
||||
决策出处 ADR-0005 / 0006 / 0008。
|
||||
-/
|
||||
|
||||
@@ -3,7 +3,7 @@ import Spec.Courseware.Model.Primitives
|
||||
/-!
|
||||
# Element —— 课程内容的原子单位
|
||||
|
||||
ADR-0005:element 实例 = 一个 kind 标签 + 符合该 kind schema 的数据。本模块把它编码成
|
||||
ADR-0005:element 实例 = 一个 kind 标签 + 符合该 kind schema 的数据。把它编码成
|
||||
依赖结构,使"数据必须匹配其 kind"成为类型层面的事实而非运行时校验。
|
||||
-/
|
||||
|
||||
|
||||
@@ -5,7 +5,7 @@
|
||||
基数**是一个真分歧点:一节课可由多人(教研组)署名,故 canonical 模型里 author 是一个
|
||||
**有序列表**,不是单值或可选单值。
|
||||
|
||||
另有一条值得钉的模式:on-disk 的**撰写态**(用户实际填写的形态)是**语法糖**——单作者可写
|
||||
另一条模式:on-disk 的**撰写态**(用户实际填写的形态)是**语法糖**——单作者可写
|
||||
`author = "…"`,多作者写 `author = ["…", "…"]`——但这个"字符串或数组"的二态**只活在加载
|
||||
边界**:`RawInfo` 经归一化折叠成 canonical `Info`,其后不再出现。canonical 接收端始终是
|
||||
`List String`,raw 形式不泄漏进模型其余部分。这正是 `Info`(canonical)与 `RawInfo`
|
||||
@@ -24,7 +24,7 @@ inductive RawAuthor where
|
||||
| many (names : List String)
|
||||
|
||||
/-- raw 作者归一化为**有序作者列表**(`PINNED`, ADR-0008)。单作者 ⇒ 单元素列表;数组
|
||||
⇒ 原样。这条钉死"canonical 接收端始终是 `List String`"。 -/
|
||||
⇒ 原样。canonical 接收端始终是 `List String`。 -/
|
||||
def RawAuthor.normalize : RawAuthor → List String
|
||||
| .one n => [n]
|
||||
| .many ns => ns
|
||||
|
||||
@@ -1,26 +1,26 @@
|
||||
/-!
|
||||
# Primitives —— Courseware 契约的留白基元
|
||||
# Primitives —— Courseware 契约的基元
|
||||
|
||||
课程工程文件模型(ADR-0005)依赖一组基元:element kind 怎么标识、某 kind 的数据
|
||||
schema 是什么、export target 怎么标识。收口成载体 `Primitives`,让模型在其上参数化
|
||||
——契约谈得了 element / lesson / 渲染**之间的关系**,而把每个基元的**内部表示**留给
|
||||
实现。注意:某基元语义已 PINNED(如 schema 形态由 ADR-0006 钉死)与其表示进 Lean
|
||||
实现。注意:某基元语义已 PINNED(如 schema 形态由 ADR-0006 固定)与其表示进 Lean
|
||||
是两回事——JSON Schema / typst 的内部结构属实现细节,不入 Lean,故基元在此仍以抽象
|
||||
类型承载。富内容的 prose 母本见 `Courseware.RichContent`。
|
||||
类型承载。富内容的母本见 `Courseware.RichContent`。
|
||||
-/
|
||||
|
||||
namespace Spec.Courseware
|
||||
|
||||
/-- Courseware 契约基元载体(关系 `PINNED`, ADR-0005;各基元表示留给实现, ADR-0006)。 -/
|
||||
structure Primitives where
|
||||
/-- element kind 标识(`PINNED` **开放宇宙**, ADR-0005;表示 `OPEN`)。刻意用抽象
|
||||
/-- element kind 标识(`PINNED` **开放宇宙**, ADR-0005;表示 `OPEN`)。用抽象
|
||||
类型而非 `inductive`:ADR-0005 决定 kind 是开放可扩展宇宙(stdlib + 第三方),
|
||||
封闭枚举会违背它——此处开放是**已决策的**(区别于 `RunState` 的"尚未封闭")。 -/
|
||||
KindId : Type
|
||||
/-- 某 kind 的合法数据类型(`PINNED` 依赖关系, ADR-0005;schema 形态 `PINNED`
|
||||
ADR-0006,表示仍抽象)。以 kind 为索引:`ElementData k` 即"符合 `k` schema 的
|
||||
数据"。schema 形态(声明式 JSON Schema + `content` 叶子 = typst 源)是 ADR-0006
|
||||
钉死的,但属 JSON/typst 内部结构、实现细节,不进 Lean;契约只锚定"数据符合
|
||||
数据"。schema 形态(声明式 JSON Schema + `content` 叶子 = typst 源)由 ADR-0006
|
||||
固定,但属 JSON/typst 内部结构、实现细节,不进 Lean;契约只锚定"数据符合
|
||||
kind schema"这条关系,故此处仍是抽象类型。 -/
|
||||
ElementData : KindId → Type
|
||||
/-- export target 标识(`PINNED` 角色, ADR-0005;表示 `OPEN`)。一个 target 是一次
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
/-!
|
||||
# RichContent —— 富内容(ADR-0006 的 prose 母本)
|
||||
# RichContent —— 富内容(ADR-0006 的母本)
|
||||
|
||||
ADR-0006:element schema 的"叶子"可以是 `content` 类型,其值是一段**源文本**,
|
||||
按其 **format** 决定语义(ADR-0015)。两种 format:
|
||||
@@ -13,7 +13,7 @@ ADR-0006:element schema 的"叶子"可以是 `content` 类型,其值是一段**
|
||||
的一等文件,坐落在一个**虚拟路径**上;相对 import 限本工程路径结构内 + `@package`(不跨工程)。markdown format
|
||||
的富内容不参与 typst 求值,但同样由一个虚拟路径定位(供 markdown 装配 step 按序读取,见 `Export/Render`)。
|
||||
|
||||
本模块只立 prose 锚点 + 最小抽象签名:typst 的 `Content`/`Module` 内部结构、JSON Schema 形状、format 的
|
||||
只立锚点 + 最小抽象签名:typst 的 `Content`/`Module` 内部结构、JSON Schema 形状、format 的
|
||||
具体判别属实现细节,不进 Lean,只承诺"富内容由一个虚拟路径定位"+"叶子带 format"这两条关系。
|
||||
-/
|
||||
|
||||
@@ -33,8 +33,8 @@ inductive ContentFormat where
|
||||
| markdown
|
||||
|
||||
/-- 对一段富内容的**引用**:它坐落在某个虚拟路径上(`PINNED` 关系, ADR-0006),并带一个
|
||||
**format**(`PINNED`, ADR-0015)。刻意**不**建模源文本、不建模求值出的 `Content`(那是实现侧的事);
|
||||
只钉"富内容经由一个 `VPath` 定位 + 带 format",作为 `Primitives.ElementData` 里 `content` 叶子的语义锚点。 -/
|
||||
**format**(`PINNED`, ADR-0015)。不建模源文本、不建模求值出的 `Content`(那是实现侧的事);
|
||||
"富内容经由一个 `VPath` 定位 + 带 format",作为 `Primitives.ElementData` 里 `content` 叶子的语义锚点。 -/
|
||||
structure RichContentRef where
|
||||
/-- 该富内容所在的虚拟路径(ADR-0006;落盘后为真实相对路径, ADR-0007)。 -/
|
||||
vpath : VPath
|
||||
|
||||
@@ -2,8 +2,8 @@ import Spec.Courseware.Open.QuestionBank
|
||||
import Spec.Courseware.Open.Course
|
||||
|
||||
/-!
|
||||
# Courseware.Open —— 留白骨架(核心关系 OPEN)
|
||||
# Courseware.Open —— OPEN 骨架(核心关系)
|
||||
|
||||
题库与 element 的关系(`QuestionBank`)、课程编排规则(`Course`)。两者均为已 surface
|
||||
但未决策的分歧点,按宪法第 2 条不臆造,待专门 ADR 落定。
|
||||
但未决策的 OPEN 分歧点,待专门 ADR 落定。
|
||||
-/
|
||||
|
||||
@@ -5,6 +5,6 @@ ADR-0005:工程文件的粒度是**单节课**;course / 单元**不是**工程
|
||||
**编排**。但"编排"的具体规则未决策:有序列表还是带层级(单元 → 课)的树?lesson 被
|
||||
引用还是被包含?跨 lesson 有无约束(目标覆盖、前后置)?这些都是 `OPEN`。
|
||||
|
||||
按宪法第 2 条本模块**不臆造**编排结构——不建 `Course := List Lesson`(那会偷偷承诺
|
||||
此处不替它选解——不建 `Course := List Lesson`(那会偷偷承诺
|
||||
"扁平有序、无层级")。只在此 surface:课程编排待专门 ADR。本文件当前不引入任何承诺性声明。
|
||||
-/
|
||||
|
||||
@@ -5,6 +5,6 @@
|
||||
典型的可复用单元,lesson 会引用它。但**题库与 element 的关系尚未决策**,且用户明确
|
||||
指出"纯引用可能不够"——element 内联题目数据 / lesson 持指向题库条目的引用 / 两者并存?
|
||||
|
||||
这是一个 `OPEN` 分歧点。按宪法第 2 条本模块**不替它选解**——不建 `QuestionRef` 也不建
|
||||
这是一个 `OPEN` 分歧点。此处不替它选解——不建 `QuestionRef` 也不建
|
||||
内联结构,只在此 surface。待专门 ADR 落定后再填。本文件当前不引入任何承诺性声明。
|
||||
-/
|
||||
|
||||
+17
-7
@@ -1,10 +1,10 @@
|
||||
/-!
|
||||
# Prelude —— System 层共享标识符
|
||||
|
||||
平台层反复引用一组标识符(项目、run、session、principal、chat、platform identity/audit)。其内部表示从未被决策
|
||||
(UUID / 复合键、principal 子类型学),也非分歧点,故收口成 opaque 载体
|
||||
`Identifiers`,System 各模块在其上参数化——契约谈得了"锁 owner 是哪个 run"这类
|
||||
**关系**,却不对标识符表示作承诺。
|
||||
平台层引用一组标识符(项目、run、session、principal、chat、platform identity/audit)。
|
||||
其内部表示从未被决策(UUID / 复合键、principal 子类型学),也非分歧点,故收口成 opaque
|
||||
载体 `Identifiers`,System 各模块在其上参数化——契约谈得了"锁 owner 是哪个 run"这类
|
||||
关系,却不对标识符表示作承诺。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
@@ -15,23 +15,33 @@ structure Identifiers where
|
||||
ProjectId : Type
|
||||
/-- SaaS 租户/组织标识(`OPEN` 表示;ADR-0020 tenant root)。 -/
|
||||
OrganizationId : Type
|
||||
/-- 租户层用户标识(`OPEN` 表示;独立实体,非飞书身份派生;见 `Hierarchy.User`)。 -/
|
||||
UserId : Type
|
||||
/-- 飞书用户 open_id(`OPEN` 表示;单应用作用域内唯一)。 -/
|
||||
FeishuOpenId : Type
|
||||
/-- 飞书 user_id(`OPEN` 表示;租户内唯一,换 app 不变)。 -/
|
||||
FeishuUserId : Type
|
||||
/-- 飞书企业应用 app_id(`OPEN` 表示)。 -/
|
||||
FeishuAppId : Type
|
||||
/-- 飞书 app_secret 信封引用(`OPEN` 表示;ADR-0024)。 -/
|
||||
FeishuAppSecretRef : Type
|
||||
/-- Hub teacher team 标识(`OPEN` 表示;ADR-0020 org-scoped team)。 -/
|
||||
TeamId : Type
|
||||
/-- 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 项目
|
||||
记忆/锚点重建,不由 session 自带。同 provider/model 内可跨多 run 复用, ADR-0002)。 -/
|
||||
SessionId : Type
|
||||
/-- 权限主体标识(`OPEN` 表示及其子类型学;ADR-0004 的 user/chat/department/…
|
||||
子类型学未定且非本层分歧点,纯 plumbing,故只留 opaque 键)。 -/
|
||||
子类型学未定且非分歧点,故只留 opaque 键)。 -/
|
||||
Principal : Type
|
||||
/-- 飞书项目群 chat 标识(`OPEN` 表示;ADR-0001 协作空间、ADR-0003 锚点引用、
|
||||
ADR-0004 `feishu_chat` principal 三处共用同一实体。独立成载体而非 `Principal` 子
|
||||
类型——principal 子类型学 OPEN 见上,本层不预设"chat 是 principal 的哪种子型")。 -/
|
||||
类型——principal 子类型学 OPEN,这里不预设"chat 是 principal 的哪种子型")。 -/
|
||||
ChatId : Type
|
||||
/-- 平台管理员身份标识(`OPEN` 表示;ADR-0023,不复用客户 `User` 标识)。 -/
|
||||
PlatformIdentityId : Type
|
||||
|
||||
+22
-14
@@ -1,41 +1,49 @@
|
||||
import Spec.System.Hierarchy
|
||||
import Spec.System.ProjectGroup
|
||||
import Spec.System.Organization
|
||||
import Spec.System.User
|
||||
import Spec.System.Connections
|
||||
import Spec.System.ProjectWorkspace
|
||||
import Spec.System.Capacity
|
||||
import Spec.System.PlatformAdministration
|
||||
import Spec.System.Run
|
||||
import Spec.System.Agent.Run
|
||||
import Spec.System.Agent.AgentRole
|
||||
import Spec.System.Agent.Memory
|
||||
import Spec.System.Agent.AgentSurface
|
||||
import Spec.System.Lock
|
||||
import Spec.System.Memory
|
||||
import Spec.System.AgentSurface
|
||||
import Spec.System.Permission
|
||||
import Spec.System.PermissionGrant
|
||||
import Spec.System.Audit
|
||||
/-!
|
||||
# System —— Hub 平台层契约
|
||||
|
||||
协作与执行的平台:项目、飞书群、AgentRun、锁、权限、审计、按需上下文。likec4
|
||||
(`docs/architecture/likec4/`)已画出这一层的**结构**;本层只补 likec4 画不出的
|
||||
**语义分歧点**:
|
||||
协作与执行的平台:项目、飞书群、AgentRun、锁、权限、审计、按需上下文。
|
||||
likec4 已画出结构;这里补语义:
|
||||
|
||||
- `Hierarchy` —— 三层主体:平台 → 组织 → 用户。
|
||||
- `User` —— 用户创建路径(管理员直接创建;飞书注册 `OPEN`)。
|
||||
- `Connections` —— 外部连接:提供商枚举(当前仅飞书) + 绑定/信息类型。
|
||||
- `ProjectGroup` —— project↔飞书群 1:1 长生命周期绑定(ADR-0001);群是协作空间,不持锁。
|
||||
- `Organization` —— SaaS tenant root(ADR-0020);project/team 单归属,TEAM grant 不跨 org;
|
||||
connection secret 使用本地主密钥信封与 fail-closed resolver(ADR-0024)。
|
||||
- `Organization` —— SaaS 租户(ADR-0020);project/team 单归属,TEAM grant 不跨 org;
|
||||
connection secret 信封与 fail-closed resolver(ADR-0024);
|
||||
owner/admin/member(`OrganizationRole`)及其管理规则(最后所有者保护)。
|
||||
- `ProjectWorkspace` —— org 后台 project explorer:folder 是透明组织节点,project 仍是权限边界
|
||||
(ADR-0021)。
|
||||
- `Capacity` —— platform ceiling 与 org policy 的分层限制、持久 admission request 状态和
|
||||
平台紧急工作负载制动(ADR-0022)。
|
||||
- `PlatformAdministration` —— 独立平台身份/会话、单一管理员角色、绑定邀请、最后管理员
|
||||
保护、fail-closed 平台审计与离线 emergency grant(ADR-0023)。
|
||||
- `AgentRole` —— org-scoped agent 角色配置 + 技能(ADR-0017/0018)。
|
||||
- `Run` —— AgentRun 状态与终止判定(状态集合完整性 OPEN)。
|
||||
- `Lock` —— 锁 owner=run(ADR-0002),及"持锁者必为非终止 run"的核心不变式。
|
||||
- `Memory` —— 按需上下文:锚点类别(ADR-0003)+ MCP 工具按 run/project 上下文授权的不变式。
|
||||
- `Memory` —— 按需上下文:锚点类别(ADR-0003)+ MCP 工具按 run/project 上下文授权。
|
||||
- `AgentSurface` —— agent 执行面被 run 的工作区所界定(ADR-0018);与 Lock 正交——
|
||||
Lock 限定并发,Surface 限定波及面。机制 OPEN。
|
||||
- `Permission` —— read⊂edit⊂manage 角色格、能力推导、单调性;force-release 在格外。
|
||||
- `PermissionGrant` —— grant(resource×principal×role)与 settings(六 policy 旋钮)结构
|
||||
(ADR-0004);role-capability 与 settings-policy 的组合规则 OPEN。
|
||||
- `Audit` —— customer Project/Run 审计有意从简(内容多为 plumbing,OPEN);Platform
|
||||
Audit 由 `PlatformAdministration` 独立钉死。
|
||||
- `Permission` —— read⊂edit⊂manage 角色体系、能力推导、单调性;force-release 在格外。
|
||||
- `PermissionGrant` —— grant(resource×principal×role)与 settings(六 policy 旋钮)
|
||||
(ADR-0004);组合规则 OPEN。
|
||||
- `Audit` —— customer Project/Run 审计从简(内容 OPEN);Platform Audit 由
|
||||
`PlatformAdministration` 独立承载。
|
||||
|
||||
标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004, 0018, 0020..0024。
|
||||
-/
|
||||
|
||||
@@ -0,0 +1,60 @@
|
||||
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
|
||||
@@ -0,0 +1,40 @@
|
||||
import Spec.Prelude
|
||||
import Spec.System.Agent.Run
|
||||
|
||||
/-!
|
||||
# AgentSurface —— Agent 执行面边界(ADR-0018)
|
||||
|
||||
Agent 在一次 run 内发起的文件操作,其路径必须落在该 run 所属 project 的工作区目录内
|
||||
(ADR-0007)。逃逸即越权,拒绝。
|
||||
|
||||
与 `Lock`(ADR-0002)正交:Lock 限定并发(谁在改),Surface 限定波及面(能改到哪)。
|
||||
二者都按 run × project 作用域。
|
||||
|
||||
shell 面的边界(命令的文件效果同样不得逃逸工作区)是同一不变式的推论。机制
|
||||
——路径校验、OS 级沙箱、SDK 权限钩子,或其组合——`OPEN`(ADR-0018)。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
variable (I : Identifiers) (Path : Type)
|
||||
|
||||
/-- Agent 在一次 run 内发起的文件操作(`PINNED` 关系, ADR-0018)。由某 run 发起、
|
||||
指向某路径;是否越权由下方 `Authorized` 约束。 -/
|
||||
structure AgentFileOp where
|
||||
/-- 发起操作的 run(授权上下文主体, ADR-0018;与 `Lock` 同作用域 run × project)。 -/
|
||||
run : I.RunId
|
||||
/-- 操作目标路径(`PINNED`, ADR-0018)。 -/
|
||||
path : Path
|
||||
|
||||
|
||||
/-- 工作区边界良构:run 的文件操作路径必须落在该 run 所属 project 的工作区目录内
|
||||
(`PINNED` 安全不变式, ADR-0018)。`runWorkspace` 与 `pathWithin` 由平台提供
|
||||
(表示 `OPEN`);本谓词约束"操作路径必须以 run 的工作区为根",杜绝 agent 越权读写
|
||||
宿主任意文件。 -/
|
||||
def AgentFileOp.Authorized
|
||||
(op : AgentFileOp I Path)
|
||||
(runWorkspace : I.RunId → Option Path)
|
||||
(pathWithin : Path → Path → Prop) : Prop :=
|
||||
∃ w, runWorkspace op.run = some w ∧ pathWithin op.path w
|
||||
|
||||
end Spec.System
|
||||
@@ -3,13 +3,13 @@ import Spec.Prelude
|
||||
/-!
|
||||
# Memory —— 按需上下文:锚点与项目记忆(ADR-0003)
|
||||
|
||||
ADR-0003:Hub **只存锚点与项目记忆**,不存全量飞书消息历史;Claude 需要更多上下文时经
|
||||
飞书 API 按需读取。本模块刻画所存锚点的**类别**(ADR 列定,枚举完整性 OPEN——ADR 是
|
||||
"例如"式列举,新增类别不违反契约),并钉死一条 likec4 画不出的安全不变式:**MCP 工具
|
||||
按 run/project 上下文授权,Claude 不得传任意 chat id**(ADR-0003 Consequences 末条)。
|
||||
ADR-0003:Hub 只存锚点与项目记忆,不存全量飞书消息历史;Claude 需要更多上下文时经
|
||||
飞书 API 按需读取。这里刻画所存锚点的类别(ADR 列定,枚举完整性 OPEN),并约束
|
||||
一条安全不变式:MCP 工具按 run/project 上下文授权,Claude 不得传任意 chat id
|
||||
(ADR-0003 Consequences 末条)。
|
||||
|
||||
"chat id 与 project 绑定"这一锚点类别由 `ProjectGroup.GroupBinding`(ADR-0001)权威承载,
|
||||
本模块不重复声明,只覆盖其余飞书侧指针(触发消息、状态卡片、回复、线程)。
|
||||
这里只覆盖其余飞书侧指针(触发消息、状态卡片、回复、线程)。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
@@ -17,9 +17,8 @@ namespace Spec.System
|
||||
variable (I : Identifiers)
|
||||
variable (MessageId CardId : Type)
|
||||
|
||||
/-- 上下文锚点(`PINNED` 类别, ADR-0003 列定;**枚举完整性 `OPEN`**——ADR 是"例如"式
|
||||
列举,实现若需新类别须 surface,不得默认本枚举已穷尽)。承载 Hub 保留的飞书侧最小指针,
|
||||
而非消息正文。 -/
|
||||
/-- 上下文锚点(`PINNED` 类别, ADR-0003;枚举完整性 `OPEN`——ADR 是"例如"式列举,
|
||||
实现若需新类别须 surface)。承载 Hub 保留的飞书侧最小指针,而非消息正文。 -/
|
||||
inductive Anchor where
|
||||
/-- 触发某次 run 的消息(`PINNED` 类别, ADR-0003 "trigger message id")。 -/
|
||||
| triggerMessage : MessageId → Anchor
|
||||
@@ -35,13 +34,11 @@ MCP tools to read … through Feishu APIs")。 -/
|
||||
structure McpReadRequest where
|
||||
/-- 发起请求的 run(授权上下文主体, ADR-0003)。 -/
|
||||
run : I.RunId
|
||||
/-- 请求读取的 chat(是否允许越界由下方 `Authorized` 钉死:不允许)。 -/
|
||||
/-- 请求读取的 chat(授权由下方 `Authorized` 约束:不允许越界)。 -/
|
||||
chat : I.ChatId
|
||||
|
||||
/-- 请求获授权:其 chat 必须等于该 run 所属 project 的绑定群(`PINNED` 安全不变式,
|
||||
ADR-0003 Consequences "MCP tools must authorize by run/project context; Claude cannot
|
||||
pass arbitrary chat ids")。`runProject`/`boundChat` 由平台提供(表示 `OPEN`);本谓词只
|
||||
钉死"chat 必须匹配 run 的 project 绑定",杜绝 Claude 传任意 chat id 越权读取。 -/
|
||||
ADR-0003)。"chat 必须匹配 run 的 project 绑定",杜绝 Claude 传任意 chat id。 -/
|
||||
def McpReadRequest.Authorized
|
||||
(req : McpReadRequest I)
|
||||
(runProject : I.RunId → Option I.ProjectId)
|
||||
@@ -1,16 +1,16 @@
|
||||
/-!
|
||||
# Run —— AgentRun 状态机
|
||||
|
||||
一次 `@Claude` 创建一个 `AgentRun`(ADR-0001),它在终止时释放项目锁(ADR-0002)。
|
||||
合法转移关系在任何 ADR / likec4 散文里都未定下,故本模块只刻画**状态**与**终止
|
||||
判定**(后者是 Lock 排他不变式的依赖),不臆造转移边。
|
||||
一次 `@bot` 创建一个 `AgentRun`(ADR-0001),它在终止时释放项目锁(ADR-0002)。
|
||||
转移关系在任何 ADR 里都未定,这里只刻画状态与终止判定(后者是 Lock 排他不变式的
|
||||
依赖),不定义转移边。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
/-- AgentRun 运行状态(状态名 `PINNED`, ADR-0001..0003, ADR-0022 + likec4;
|
||||
**完整性 `OPEN`**——散文从未声明"状态恰好这些";实现若需新状态(如 pending)须
|
||||
surface,不得默认本枚举已穷尽)。终止态见 `RunState.Terminal`。 -/
|
||||
/-- AgentRun 运行状态(状态名 `PINNED`, ADR-0001..0003, ADR-0022;完整性 `OPEN`
|
||||
——ADR 从未声明"状态就是这些";实现若需新状态(如 pending)须 surface)。终止态
|
||||
见 `RunState.Terminal`。 -/
|
||||
inductive RunState where
|
||||
| active
|
||||
| waitingForUser
|
||||
@@ -1,44 +0,0 @@
|
||||
import Spec.Prelude
|
||||
import Spec.System.Run
|
||||
|
||||
/-!
|
||||
# AgentSurface —— Agent 执行面边界(ADR-0018)
|
||||
|
||||
ADR-0001/0002/0004 覆盖"协作治理"直到 `triggerAgent`:谁能触发一次 run。但触发之后
|
||||
agent 在执行层面能干什么——读哪些文件、跑什么命令——任何 ADR / 散文都未定。ADR-0017
|
||||
落地时采用 Claude Code SDK 的 `bypassPermissions` + 全量 Read/Write/Bash/Glob/Grep,
|
||||
agent 的文件与 shell 面对宿主**无界**:spec 与 ADR 均未钉死边界。本模块补这一层。
|
||||
|
||||
钉死的不变式:agent 在一次 run 内发起的文件操作,其路径必须落在该 run 所属 project
|
||||
的工作区目录内(ADR-0007:工程文件是目录树;此 ADR 固定"agent 操作落在该树内")。
|
||||
逃逸即越权,拒绝。与 `Lock`(ADR-0002)正交:Lock 限定**并发**(谁在改),Surface
|
||||
限定**波及面**(能改到哪)。二者都按 run × project 作用域。
|
||||
|
||||
shell 面的边界(命令的文件效果同样不得逃逸工作区)是同一不变式的推论,但**机制**
|
||||
——路径校验工具包装、OS 级沙箱(bubblewrap/容器)、SDK 权限钩子,或其组合——`OPEN`
|
||||
(ADR-0018)。契约钉死不变式,不钉死机制。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
variable (I : Identifiers) (Path : Type)
|
||||
|
||||
/-- Agent 在一次 run 内发起的文件操作(`PINNED` 关系, ADR-0018)。由某 run 发起、
|
||||
指向某路径;是否越权由下方 `Authorized` 钉死。 -/
|
||||
structure AgentFileOp where
|
||||
/-- 发起操作的 run(授权上下文主体, ADR-0018;与 `Lock` 同作用域 run × project)。 -/
|
||||
run : I.RunId
|
||||
/-- 操作目标路径(`PINNED` 字段, ADR-0018)。 -/
|
||||
path : Path
|
||||
|
||||
/-- 工作区边界良构:run 的文件操作路径必须落在该 run 所属 project 的工作区目录内
|
||||
(`PINNED` 平台核心安全不变式, ADR-0018)。`runWorkspace` 与 `pathWithin` 均由平台提供
|
||||
(表示 `OPEN`——路径如何表示、"在内"如何判定是纯 plumbing,非本层分歧点);本谓词只
|
||||
钉死"操作路径必须以 run 的工作区为根",杜绝 agent 越权读写宿主任意文件。 -/
|
||||
def AgentFileOp.Authorized
|
||||
(op : AgentFileOp I Path)
|
||||
(runWorkspace : I.RunId → Option Path)
|
||||
(pathWithin : Path → Path → Prop) : Prop :=
|
||||
∃ w, runWorkspace op.run = some w ∧ pathWithin op.path w
|
||||
|
||||
end Spec.System
|
||||
@@ -1,21 +1,18 @@
|
||||
import Spec.Prelude
|
||||
|
||||
/-!
|
||||
# Audit —— Project/Run 审计日志(有意从简)
|
||||
# Audit —— Project/Run 审计日志
|
||||
|
||||
likec4 把 `AuditLog` 列为实体(`AgentRun -> AuditLog 'records lifecycle events'`),
|
||||
但**审计记录里装什么**(事件 schema、保留策略、可查询维度)在任何 ADR / 散文里都
|
||||
未决策,且大多是 plumbing——按分歧点测试不入契约。故本模块刻意几乎为空:只固定
|
||||
"审计以 run 为主体记录其生命周期事件"这一条已决策关系,其余 `OPEN`(留白本身是
|
||||
契约的一部分:承诺此处尚无答案、勿填)。
|
||||
审计记录里装什么(事件 schema、保留策略、可查询维度)在任何 ADR 里都未决策,
|
||||
且大多是实现细节。这里只固定"审计以 run 为主体记录其生命周期事件"这一条已决策
|
||||
关系,其余 `OPEN`。ADR-0023 的 Platform Audit 是另一个控制面,见
|
||||
`Spec.System.PlatformAdministration`,不复用本结构。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
/-- 审计条目的最小骨架(关系 `PINNED` / 内容 `OPEN`, likec4)。只承诺"一条审计记录
|
||||
关联到某个 run";事件类型、时间、actor、详情等字段 `OPEN`,待真实分歧点出现时由
|
||||
对应 ADR 落定。ADR-0023 的 Platform Audit 是另一个 fail-closed 控制面,见
|
||||
`Spec.System.PlatformAdministration`,不复用本结构。 -/
|
||||
关联到某个 run";事件类型、时间、actor、详情等字段 `OPEN`。 -/
|
||||
structure AuditEntry (I : Identifiers) where
|
||||
/-- 该审计条目所属的 run(`PINNED` 关系, likec4)。 -/
|
||||
run : I.RunId
|
||||
|
||||
@@ -4,8 +4,8 @@ import Spec.Prelude
|
||||
# Capacity —— SaaS capacity admission and abuse controls (ADR-0022)
|
||||
|
||||
初始生产服务共享有限的单机资源,但不能让一个 Organization 垄断容量或让无界输入拖垮
|
||||
其他租户。ADR-0022 钉死分层限制、持久 admission、显式背压和紧急制动的领域语义;
|
||||
具体数值必须由生产式容量测试校准,因此保持 `OPEN`,不得把未经验证的数字冒充契约。
|
||||
其他租户。ADR-0022 定义分层限制、持久 admission、显式背压和紧急制动;具体数值由
|
||||
生产式容量测试校准,保持 `OPEN`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
@@ -0,0 +1,24 @@
|
||||
import Spec.System.Connections.Prelude
|
||||
import Spec.System.Connections.Feishu
|
||||
|
||||
/-!
|
||||
# Connections —— 连接绑定与用户信息
|
||||
|
||||
组织/用户的外部连接。提供商枚举见 `Connections.Prelude`;
|
||||
飞书具体类型见 `Connections.Feishu`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
|
||||
/-- 组织连接绑定(`PINNED`)。 -/
|
||||
inductive ConnectionBinding (I : Identifiers) where
|
||||
/-- 飞书(`PINNED`)。 -/
|
||||
| feishu : FeishuAppBinding I → ConnectionBinding I
|
||||
|
||||
/-- 用户连接信息(`PINNED`)。 -/
|
||||
inductive ConnectionProfile (I : Identifiers) where
|
||||
/-- 飞书(`PINNED`)。 -/
|
||||
| feishu : FeishuProfile I → ConnectionProfile I
|
||||
|
||||
end Spec.System
|
||||
@@ -0,0 +1,31 @@
|
||||
import Spec.Prelude
|
||||
|
||||
/-!
|
||||
# Feishu —— 飞书连接
|
||||
|
||||
组织绑定一个飞书企业应用(1:1)。用户经此应用登录、调飞书 API。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
variable (I : Identifiers)
|
||||
|
||||
/-- 组织的飞书应用绑定(`PINNED`, 1:1)。 -/
|
||||
structure FeishuAppBinding where
|
||||
/-- 飞书企业应用 app_id(`OPEN` 表示)。 -/
|
||||
appId : I.FeishuAppId
|
||||
/-- app_secret 信封引用(`PINNED`, ADR-0024)。 -/
|
||||
appSecretEnvelope : I.FeishuAppSecretRef
|
||||
|
||||
/-- 用户的飞书信息(`PINNED`)。 -/
|
||||
structure FeishuProfile where
|
||||
/-- 应用内身份(`OPEN`);调 API 的直接句柄,换应用即变。 -/
|
||||
openId : I.FeishuOpenId
|
||||
/-- 租户内身份(`OPEN`);换应用不变,比 open_id 稳定。 -/
|
||||
userId : I.FeishuUserId
|
||||
/-- 显示名(`OPEN`)。 -/
|
||||
name : Option String
|
||||
/-- 头像 URL(`OPEN`)。 -/
|
||||
avatarUrl : Option String
|
||||
|
||||
end Spec.System
|
||||
@@ -0,0 +1,15 @@
|
||||
/-!
|
||||
# Connections.Prelude —— 连接提供商
|
||||
|
||||
用户/组织的外部身份连接。当前仅 IdP 类别(飞书)。
|
||||
模型 provider connection 是独立概念,见 `Spec.System.Organization`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
/-- 连接提供商(`PINNED`;当前仅飞书,未来可扩展钉钉/企微)。 -/
|
||||
inductive ConnectionProvider where
|
||||
/-- 飞书(`PINNED`)。 -/
|
||||
| feishu
|
||||
|
||||
end Spec.System
|
||||
@@ -0,0 +1,46 @@
|
||||
import Spec.Prelude
|
||||
import Spec.System.Connections
|
||||
|
||||
/-!
|
||||
# Hierarchy —— 主体层级
|
||||
|
||||
整个服务中的主体: 平台 → 组织(租户)→ 用户。
|
||||
|
||||
- **平台**(Platform): SaaS 提供方实体
|
||||
|
||||
- **组织**(Organization): SaaS 租户
|
||||
|
||||
- **用户**(User): 租户内的独立实体
|
||||
|
||||
**术语**: "管理员"一词在文档中不单独出现，避免跨层歧义。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
variable (I : Identifiers)
|
||||
/-- 平台(`PINNED`, SaaS 提供方)。只有一个,独立于组织。管理面见 `PlatformAdministration`(ADR-0023)。 -/
|
||||
structure Platform where
|
||||
/-- 平台自有飞书应用(`PINNED`, ADR-0023)。 -/
|
||||
application : I.PlatformFeishuApplicationId
|
||||
/-- 组织(`PINNED`, ADR-0020)。project/team 必须归属且仅归属一个 org。
|
||||
外部连接见 `Connections`。角色/tenancy/凭据见 `Spec.System.Organization`。 -/
|
||||
structure Organization where
|
||||
/-- 组织标识(`OPEN` 表示)。 -/
|
||||
id : I.OrganizationId
|
||||
/-- 外部连接(`PINNED`)。 -/
|
||||
connections : List (ConnectionBinding I)
|
||||
|
||||
/-- 用户(`PINNED`, 租户层独立实体)。必属一个组织。外部连接见 `Connections`。 -/
|
||||
structure User where
|
||||
/-- 用户标识(`OPEN` 表示;组织内唯一,不可改;登录用)。 -/
|
||||
id : I.UserId
|
||||
/-- 所属组织(`PINNED`, ADR-0020)。 -/
|
||||
organization : I.OrganizationId
|
||||
/-- 显示名(`PINNED`, 可改)。 -/
|
||||
displayName : String
|
||||
/-- 密码哈希(`OPEN` 表示;id + 密码登录)。 -/
|
||||
passwordHash : String
|
||||
/-- 外部连接(`PINNED`)。 -/
|
||||
connections : List (ConnectionProfile I)
|
||||
|
||||
end Spec.System
|
||||
+10
-13
@@ -1,35 +1,32 @@
|
||||
import Spec.Prelude
|
||||
import Spec.System.Run
|
||||
import Spec.System.Agent.Run
|
||||
|
||||
/-!
|
||||
# Lock —— 项目锁与排他不变式
|
||||
|
||||
ADR-0002 的核心:防止并发 Claude 同改一个项目,锁的 **owner 是当前 `AgentRun`**
|
||||
(不是 teacher / chat / session)。本模块把这条决策编码进类型,并钉死那条
|
||||
likec4 画不出的语义不变式——**持锁者必为非终止 run**。
|
||||
ADR-0002:防止并发 agent 同改一个项目,锁的 owner 是当前 `AgentRun`(不是
|
||||
teacher / chat / session)。持锁者必为非终止 run。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
variable (I : Identifiers)
|
||||
|
||||
/-- 项目级锁(`PINNED`, ADR-0002)。`owner : RunId`(非 SessionId/Principal)从类型
|
||||
上编码"lock owner = run_id":锁不可能被 session / teacher 持有。 -/
|
||||
/-- 项目级锁(`PINNED`, ADR-0002)。`owner : RunId`从类型上编码"lock owner = run_id":
|
||||
锁不可能被 session / teacher 持有。 -/
|
||||
structure ProjectAgentLock where
|
||||
/-- 作用域:项目级(`PINNED`, ADR-0002 `scope = project_id`)。 -/
|
||||
/-- 作用域:项目级(`PINNED`, ADR-0002)。 -/
|
||||
scope : I.ProjectId
|
||||
/-- 持有者:一个 run(`PINNED`, ADR-0002 `owner = run_id`)。 -/
|
||||
/-- 持有者:一个 run(`PINNED`, ADR-0002)。 -/
|
||||
owner : I.RunId
|
||||
|
||||
/-- 锁表:每项目当前持锁 run(`PINNED` 排他性, ADR-0002)。`ProjectId → Option RunId`
|
||||
的结构**本身**即排他——不可能为同一项目登记两个并发 owner。 -/
|
||||
的结构本身即排他——不可能为同一项目登记两个并发 owner。 -/
|
||||
def LockTable := I.ProjectId → Option I.RunId
|
||||
|
||||
/-- 锁表良构:**持锁者必为非终止 run**(`PINNED` 平台核心不变式, ADR-0002)。
|
||||
/-- 锁表良构:持锁者必为非终止 run(`PINNED`, ADR-0002)。
|
||||
|
||||
"锁在 run 终止时释放"的逻辑等价物:若 `p` 的锁被 `r` 持有,则 `r` 不在终止态。这条
|
||||
把 Lock 与 Run 耦合起来——likec4 能画"run owns lock while running",画不出"终止即
|
||||
必须释放"这个约束;它正是契约相对结构图的增量。 -/
|
||||
若 `p` 的锁被 `r` 持有,则 `r` 不在终止态。锁在 run 终止时释放。 -/
|
||||
def LockTable.WellFormed
|
||||
(lt : LockTable I) (statusOf : I.RunId → RunState) : Prop :=
|
||||
∀ p r, lt p = some r → ¬ (statusOf r).Terminal
|
||||
|
||||
@@ -1,18 +1,12 @@
|
||||
import Spec.Prelude
|
||||
|
||||
/-!
|
||||
# Organization —— SaaS tenant root (ADR-0020, ADR-0024)
|
||||
# Organization —— SaaS 租户 (ADR-0020, ADR-0024)
|
||||
|
||||
ADR-0020:Hub 长期按 SaaS 形态演进,`Organization` 是客户侧 tenant root。
|
||||
`Project` 与 `Team` 都必须归属且只归属一个 organization;team 对 project 的授权
|
||||
必须在同一 organization 内。平台运营控制面(platform staff / break-glass / 账单)
|
||||
不复用 project 的 `read/edit/manage` 角色格,而是另一个控制面。
|
||||
|
||||
本模块只钉死会造成实现分歧的不变量:tenant root 存在、project/team 单归属、team grant
|
||||
不得跨 org,以及 model provider connection 的凭据归属模式。用户身份、外部目录
|
||||
provider 细节仍为 `OPEN`;平台控制面身份/角色/审计已由 ADR-0023 与
|
||||
`Spec.System.PlatformAdministration` 独立决定。连接凭据的本地主密钥信封、不可变版本、
|
||||
writer authority 与 fail-closed resolver 由 ADR-0024 固定。
|
||||
组织就是租户。project/team 必须归属且仅归属一个 org;team→project grant 必须同 org。
|
||||
组织实体见 `Hierarchy.Organization`;用户见 `Spec.System.User`;平台控制面见
|
||||
`PlatformAdministration`(ADR-0023)。凭据信封见 ADR-0024。Agent 角色配置见
|
||||
`Spec.System.Agent.AgentRole`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
@@ -41,19 +35,17 @@ structure TeamProjectGrantScope where
|
||||
project : I.ProjectId
|
||||
/-- 获得授权的 team principal(`PINNED`, ADR-0020)。 -/
|
||||
team : I.TeamId
|
||||
|
||||
/-- Team-project grant 是良构的 iff project 与 team 解析到同一 organization
|
||||
(`PINNED`, ADR-0020)。`projectOrg`/`teamOrg` 由平台提供(表示 `OPEN`);本谓词钉死
|
||||
跨 org team grant 必须被拒绝。 -/
|
||||
(`PINNED`, ADR-0020)。`projectOrg`/`teamOrg` 由平台提供(表示 `OPEN`);跨 org
|
||||
team grant 必须被拒绝。 -/
|
||||
def TeamProjectGrantScope.WellScoped
|
||||
(grant : TeamProjectGrantScope I)
|
||||
(projectOrg : I.ProjectId → Option I.OrganizationId)
|
||||
(teamOrg : I.TeamId → Option I.OrganizationId) : Prop :=
|
||||
∃ o, projectOrg grant.project = some o ∧ teamOrg grant.team = some o
|
||||
|
||||
/-- Organization 的 model provider 凭据归属模式(`PINNED`, ADR-0021):BYOK 由 org
|
||||
管理员提供和管理;platform-managed 由平台管理员为该 org 单独提供和管理。两种模式
|
||||
都不允许无关 org 共用 process-global provider key。模式切换过程仍为 `OPEN`。 -/
|
||||
/- BYOK 由组织所有者/管理员管理;platform-managed 由平台管理员管理。两种模式都不允许
|
||||
跨 org 共用 process-global key。模式切换 `OPEN`。 -/
|
||||
inductive ProviderCredentialMode where
|
||||
| byok
|
||||
| platformManaged
|
||||
@@ -78,7 +70,7 @@ inductive OrganizationConnectionStatus where
|
||||
|
||||
/-- Organization secret version 的信封绑定上下文(`PINNED`, ADR-0024):认证附加数据必须
|
||||
同时绑定 organization、connection、secret version 与 purpose,因此密文不能跨行、跨 org、
|
||||
跨 connection 或跨用途替换。各标识符的数据库表示属于 plumbing,这里保持 opaque。 -/
|
||||
跨 connection 或跨用途替换。各标识符的数据库表示为实现细节,这里保持 opaque。 -/
|
||||
structure OrganizationSecretBinding
|
||||
(OrganizationId ConnectionId SecretVersionId Purpose : Type) where
|
||||
/-- secret 所属 organization(`PINNED`, ADR-0024)。 -/
|
||||
@@ -104,4 +96,34 @@ def OrganizationSecretResolvable
|
||||
organizationActive && connectionActive &&
|
||||
(binding.organization == requestedOrganization) && authenticatedEnvelope
|
||||
|
||||
|
||||
/-- 组织成员角色(`PINNED` 封闭三档)。与项目层 `Role`、平台层 `PlatformRole` 互不相交。 -/
|
||||
inductive OrganizationRole where
|
||||
/-- 组织所有者(`PINNED`):bootstrap,独家管 owner 群体,受最后所有者保护。 -/
|
||||
| owner
|
||||
/-- 组织管理员(`PINNED`):管成员/policy/BYOK,不能管 owner 群体。 -/
|
||||
| admin
|
||||
/-- 组织成员(`PINNED`):普通成员。 -/
|
||||
| member
|
||||
|
||||
/-- 组织成员关系(`PINNED`)。 -/
|
||||
structure OrganizationMembership where
|
||||
/-- 成员(`PINNED`;独立实体,见 `Hierarchy.User`)。 -/
|
||||
user : I.UserId
|
||||
/-- 组织(`PINNED`)。 -/
|
||||
organization : I.OrganizationId
|
||||
/-- 角色(`PINNED`)。 -/
|
||||
role : OrganizationRole
|
||||
|
||||
/-- 只有组织所有者能管 owner 群体(`PINNED`)。 -/
|
||||
def CanManageOwnerGroup (actorRole : OrganizationRole) : Prop :=
|
||||
actorRole = .owner
|
||||
|
||||
/-- 最后所有者保护(`PINNED`):撤销 owner 时同 org 必须还有一个不同的 owner。 -/
|
||||
def LastOwnerProtected
|
||||
(target : OrganizationMembership I)
|
||||
(otherOwnersInOrg : List I.UserId) : Prop :=
|
||||
target.role ≠ .owner ∨
|
||||
∃ other, other ∈ otherOwnersInOrg ∧ other ≠ target.user
|
||||
|
||||
end Spec.System
|
||||
|
||||
@@ -5,8 +5,7 @@ import Spec.Prelude
|
||||
|
||||
ADR-0004:权限走"飞书云文档式"——grant(`resource + principal + role`)与 settings
|
||||
分离;role 取自封闭的 `read / edit / manage`,且 **read ⊂ edit ⊂ manage** 累积赋能;
|
||||
强制释放锁是 **admin-only**,在 role 体系之外。本模块把这套结构与"高 role 含低
|
||||
role 全部能力"的单调性钉死。
|
||||
强制释放锁是 **admin-only**,在 role 体系之外。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
@@ -4,16 +4,14 @@ import Spec.System.Permission
|
||||
/-!
|
||||
# PermissionGrant —— 授权与设置(ADR-0004)
|
||||
|
||||
ADR-0004 的"飞书云文档式"权限:**grant**(`resource × principal × role`)与 **settings**
|
||||
(各 policy 旋钮)分离;role 决定"谁能"(能力,见 `Permission`),settings 决定"此资源
|
||||
是否开某类操作"(策略)。本模块把 grant/settings 的结构钉死——`Permission` 已落 role 能
|
||||
力格,本模块补"授权如何挂到资源/主体上"。
|
||||
ADR-0004 的"飞书云文档式"权限:grant(`resource × principal × role`)与 settings
|
||||
(各 policy 旋钮)分离;role 决定能力(见 `Permission`),settings 决定"此资源是否
|
||||
开某类操作"。
|
||||
|
||||
principal 子类型学(user/chat/department/…)与各 policy 值域均为 `OPEN`(ADR 未定,非本
|
||||
层分歧点)。**role-capability 与 settings-policy 如何组合成最终授权决策**亦 `OPEN`——
|
||||
ADR-0004 把二者列为分离的闸,但未明文规定组合规则(AND?settings 能否超出 role?),实现
|
||||
须 surface,不得默认。ADR-0020 另行钉死 TEAM principal 授权 PROJECT resource 时必须
|
||||
同 organization;该 tenant well-scopedness 见 `Spec.System.Organization`。
|
||||
principal 子类型学(user/chat/department/…)与各 policy 值域 `OPEN`。role-capability
|
||||
与 settings-policy 如何组合成最终授权决策亦 `OPEN`——ADR-0004 把二者列为分离的闸,
|
||||
但未明文规定组合规则。ADR-0020 约束 TEAM principal 授权 PROJECT resource 时必须同
|
||||
organization,见 `Spec.System.Organization`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
@@ -45,9 +43,8 @@ structure PermissionGrant where
|
||||
role : Role
|
||||
|
||||
/-- 资源策略设置(`PINNED` 结构 + 六旋钮, ADR-0004 `PermissionSettings`):与 grant 分离,
|
||||
控制"此资源是否开某类操作"。六旋钮由 ADR 逐字列名;各旋钮值域 `OPEN`(ADR 未定,非本层
|
||||
分歧点)。共享同一 opaque `Policy` 类型:契约只钉死"旋钮存在且相互独立",不钉死"各旋钮
|
||||
值域互异"——值域是实现/后续 ADR 的事。 -/
|
||||
控制"此资源是否开某类操作"。六旋钮由 ADR 逐字列名;各旋钮值域 `OPEN`(ADR 未定)。
|
||||
共享同一 opaque `Policy` 类型:契约只约束"旋钮存在且相互独立";值域是实现/后续 ADR 的事。 -/
|
||||
structure PermissionSettings where
|
||||
/-- 设置所属资源(`PINNED`, ADR-0004)。 -/
|
||||
resource : Resource I ArtifactId
|
||||
|
||||
@@ -8,8 +8,8 @@ import Spec.Prelude
|
||||
单一平级管理员角色、绑定身份的 invitation、可撤销服务端 session、mutation 与平台审计
|
||||
同成同败、最后管理员保护,以及无常驻账号的双因子离线恢复。
|
||||
|
||||
本模块只钉死这些会导致安全边界分歧的语义。cookie 属性、token hash、具体 TTL、审计
|
||||
字段表示/保留期、recovery key 介质和 CLI/SQL 机制仍为 `OPEN`,由对应实现决策承载。
|
||||
这些安全边界语义见下。cookie 属性、token hash、具体 TTL、审计
|
||||
字段表示/保留期、recovery key 介质和 CLI/SQL 机制 `OPEN`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
@@ -3,26 +3,23 @@ import Spec.Prelude
|
||||
/-!
|
||||
# ProjectGroup —— 飞书项目群作为协作空间(ADR-0001)
|
||||
|
||||
ADR-0001 的核心:一个 project 对应一个**长生命周期**飞书项目群;群是协作空间,**不是锁
|
||||
owner**(锁归 `AgentRun`,见 `Lock` / ADR-0002),不是临时处理 session。群可在无 Claude
|
||||
处理时保持开启;教师离群/静音与项目权限、与 Claude 生命周期相互独立。本模块钉死
|
||||
project↔group 的**active**一对一绑定——likec4 画得出"project has group",画不出"恰好一个、
|
||||
且群不持锁"。
|
||||
一个 project 对应一个长生命周期飞书项目群;群是协作空间,不持锁(锁归 `AgentRun`,
|
||||
见 `Lock` / ADR-0002)。群可在无 agent 处理时保持开启;教师离群/静音与项目权限、
|
||||
与 agent 生命周期相互独立。
|
||||
|
||||
**绑定历史(`PINNED`, ADR-0021):** active binding 严格 1:1;实现可以保留 archived
|
||||
historical binding rows 供审计/纠错,但 `GroupBinding` 谓词只刻画当前 active 快照。
|
||||
群解散/不可达的自动化处理仍为 `OPEN`;pilot 纠错由 org admin 显式归档绑定。
|
||||
**绑定历史(`PINNED`, ADR-0021):** active binding 严格 1:1;实现可保留 archived
|
||||
historical binding rows 供审计,但 `GroupBinding` 谓词只刻画当前 active 快照。
|
||||
群解散/不可达的自动化处理 `OPEN`;pilot 纠错由 org admin 显式归档绑定。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
variable (I : Identifiers)
|
||||
|
||||
/-- 飞书项目群(`PINNED` 长生命周期协作空间, ADR-0001)。承载 project 与飞书 chat 的绑定;
|
||||
**不是锁 owner**(锁归 `AgentRun`,见 `Lock`);不是临时 session。 -/
|
||||
/-- 飞书项目群(`PINNED` 长生命周期协作空间, ADR-0001)。承载 project 与飞书 chat 的
|
||||
绑定;不持锁(锁归 `AgentRun`,见 `Lock`)。 -/
|
||||
structure ProjectGroup where
|
||||
/-- 群对应的飞书 chat(`PINNED` 关系, ADR-0001 "one project has one Feishu project
|
||||
group";chat 标识见 `Identifiers.ChatId`)。 -/
|
||||
/-- 群对应的飞书 chat(`PINNED` 关系, ADR-0001;chat 标识见 `Identifiers.ChatId`)。 -/
|
||||
chat : I.ChatId
|
||||
|
||||
/-- 项目↔active 群绑定表(`PINNED` 每项目至多一个 active 群, ADR-0001/0021)。
|
||||
@@ -30,9 +27,9 @@ structure ProjectGroup where
|
||||
自带);良构补另一半——单射。 -/
|
||||
def GroupBinding := I.ProjectId → Option I.ChatId
|
||||
|
||||
/-- Active 绑定良构:**单射**——不同 project 不绑同一 active chat(`PINNED` 1:1 的另一半,
|
||||
ADR-0001/0021)。"每 project 至多一个群"由 `Option` 结构自带;这条钉死"每群至多属于一个
|
||||
project"。archived historical bindings 不在本快照不变式内。 -/
|
||||
/-- Active 绑定良构:单射——不同 project 不绑同一 active chat(`PINNED`, ADR-0001/0021)。
|
||||
"每 project 至多一个群"由 `Option` 结构自带;这条约束"每群至多属于一个 project"。
|
||||
archived historical bindings 不在本快照不变式内。 -/
|
||||
def GroupBinding.WellFormed (b : GroupBinding I) : Prop :=
|
||||
∀ p₁ p₂ c, b p₁ = some c → b p₂ = some c → p₁ = p₂
|
||||
|
||||
|
||||
@@ -3,12 +3,11 @@ import Spec.Prelude
|
||||
/-!
|
||||
# ProjectWorkspace —— project explorer 与飞书建项入口(ADR-0021)
|
||||
|
||||
ADR-0021 把 org 后台里的"文件管理器式"项目管理收口为透明 folder + project:
|
||||
folder 只负责导航、排序、层级与用量聚合,当前不是权限资源。project 仍是授权边界。
|
||||
org 后台里的"文件管理器式"项目管理:folder 只负责导航、排序、层级与用量聚合,当前
|
||||
不是权限资源。project 仍是授权边界。
|
||||
|
||||
本模块只钉死会影响实现分歧的不变量:folder/project 同 org、folder 不参与权限、普通成员
|
||||
从飞书群创建 project 必须受 org policy 控制。folder visibility/team policy/继承授权仍为
|
||||
未来扩展,不得在当前实现中半隐式加入。
|
||||
不变量:folder/project 同 org、folder 不参与权限、普通成员从飞书群创建 project 受
|
||||
org policy 控制。folder visibility/team policy/继承授权 `OPEN`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
@@ -39,7 +38,7 @@ def ProjectFolderPlacement.WellScoped
|
||||
∃ o, projectOrg placement.project = some o ∧ folderOrg placement.folder = some o
|
||||
|
||||
/-- Folder 当前透明(`PINNED`, ADR-0021):folder 不是权限资源,不持有 grants,移动 project
|
||||
不改变 project 自身授权。未来 folder policy 若出现,必须新增显式语义而不是复用本谓词。 -/
|
||||
不改变 project 自身授权。未来 folder policy 若出现,须新增显式语义。 -/
|
||||
structure FolderTransparent where
|
||||
/-- 透明性命题本身;字段存在是为了让 contract 明确可引用(`PINNED`, ADR-0021)。 -/
|
||||
current : True
|
||||
|
||||
@@ -0,0 +1,12 @@
|
||||
import Spec.Prelude
|
||||
|
||||
/-!
|
||||
# User —— 用户创建路径
|
||||
|
||||
用户实体见 `Hierarchy.User`;外部连接见 `Spec.System.Connections`。
|
||||
|
||||
用户创建当前只定义管理员直接创建;飞书自助注册→管理员审批 `OPEN`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
end Spec.System
|
||||
Reference in New Issue
Block a user