forked from EduCraft/curriculum-project-hub
Compare commits
1 Commits
| Author | SHA1 | Date | |
|---|---|---|---|
 sjfhsjfh
|
73e9d258d6
|
@@ -11,8 +11,5 @@
|
||||
# regenerable, not for VCS. The embedded engine mounts cph-render directly.
|
||||
render/vendor/local-packages/
|
||||
|
||||
# Node (hub/ TS workspace and any future JS package)
|
||||
node_modules/
|
||||
|
||||
# OS / editor
|
||||
.DS_Store
|
||||
|
||||
@@ -1,74 +1,74 @@
|
||||
# curriculum-project-hub
|
||||
|
||||
教研生产的数字化解决方案。核心思路:课程像 DAW / 剪辑软件那样有一个**结构化的工程文件**;coding agent 协助编辑它;一个 rule-based checker(类编译器)校验其合法性并给出 helpful fix hint。目标是把教研从一次性的文档,沉淀成**可累积、可校验、可复用的资产**。
|
||||
教研生产的数字化解决方案。核心思路:课程像 DAW / 剪辑软件那样有一个结构化的工程文件;
|
||||
LLM assistant 协助编辑它;一个 rule-based checker 校验其合法性并给出有用的诊断。
|
||||
|
||||
这是一个 **monorepo**。它的组织方式本身就表达了一条原则:**`spec/` 是上游的语义母本,其余部件是向它对齐的实现。**
|
||||
LLM 提效,但判不了一节课合不合法(它不能真去跑 typst、不能可靠地断言数据合不合
|
||||
schema);checker 真跑工具、给确定性诊断,补上这块。两者一起才是完整闭环。目标是把教研
|
||||
从一次性的文档,变成可累积、可校验、可复用的资产。
|
||||
|
||||
## 安装 `cph` 命令行
|
||||
这是一个 monorepo。组织方式本身就表达了一条原则:`spec/` 是上游的语义母本,其余部件是
|
||||
向它对齐的实现。
|
||||
|
||||
当前版本 **0.0.2**。从源码安装(本仓库根目录):
|
||||
## 安装 `cph`
|
||||
|
||||
从源码安装(本仓库根目录):
|
||||
|
||||
```sh
|
||||
cargo install --path crates/cph-cli --locked
|
||||
```
|
||||
|
||||
`render` 包已嵌入二进制(build.rs 编译期拷入 + `include_dir!`),所以装好后**无需任何环境变量、不依赖源码树**即可用。渲染包按版本解压到 per-user cache(`~/.cache/cph/render-<version>/` 或 macOS `~/Library/Caches/cph/...`);开发时可设 `CPH_RENDER_DIR` 指向 live `render/` 目录覆盖。
|
||||
`render` 包已嵌入二进制,装好后无需任何环境变量、不依赖源码树即可用。开发时可设
|
||||
`CPH_RENDER_DIR` 指向 live `render/` 目录覆盖。
|
||||
|
||||
```sh
|
||||
cph --version # cph 0.0.2
|
||||
cph check <工程目录> # 校验合法性(7 类诊断)
|
||||
cph check <工程目录> # 校验合法性
|
||||
cph build <工程目录> --target student -o build/student.pdf # 渲讲义 PDF
|
||||
cph completions zsh > ~/.zfunc/_cph # shell 补全(可选)
|
||||
```
|
||||
|
||||
**版本契约(ADR-0016):** 教研工程文件根放一个 `.cph-version` 文件,内容为它面向的 cph 版本(如 `0.0.2`)。`cph` 加载时比对自身版本,不相容则报 `E-CPH-VERSION` error 并拒绝(当前判定为版本完全相等;后续可放宽为 semver 区间,只改一处谓词)。`examples/` 与本仓 fixture 已带该文件作为迁移起点;缺文件的工程暂时跳过此检查(OPEN)。
|
||||
|
||||
Shell 补全(可选):
|
||||
|
||||
```sh
|
||||
cph completions zsh > ~/.zfunc/_cph # 或 bash/fish/powershell/elvish
|
||||
```
|
||||
工程文件根放一个 `.cph-version` 文件,声明它面向的 cph 版本;`cph` 加载时比对自身版本,
|
||||
不相容则拒绝(版本契约,ADR-0016)。
|
||||
|
||||
## 仓库布局
|
||||
|
||||
```
|
||||
README.md ← 本文件:总览 + 宪法(下面 5 条)
|
||||
CLAUDE.md ← 全局 agent 操作手册(管整个 repo)
|
||||
docs/adr/ ← 系统级架构决策记录(跨部件,被 spec 契约引用)
|
||||
spec/ ← Lean 语义母本(自包含的 Lean 工程)。见 spec/README.md
|
||||
Cargo.toml ← 仓库级 cargo workspace(实现部件共用,便于跨部件复用 crate)
|
||||
crates/ ← 实现:rule-based checker(向 spec 对齐)。见 crates/README.md
|
||||
cph-diag / cph-model / cph-schema / cph-typst ← 可复用基础(模型/校验/typst 引擎)
|
||||
cph-check / cph-cli ← checker 本体 + `cph` 命令行
|
||||
render/ ← typst 渲染包 cph-render(母本的渲染后端之一,ADR-0005)
|
||||
examples/ ← 样例工程文件(如 TH-141),流水线的真实输入
|
||||
(hub/ exporter/ …) ← 将来的其他部件,平级于 spec/。尚未创建
|
||||
```
|
||||
`spec/` 是 Lean 语义母本(自包含 Lean 工程,见 `spec/README.md`);`crates/` 是实现
|
||||
(rule-based checker,向 spec 对齐,见 `crates/README.md`);`render/` 是 typst 渲染包;
|
||||
`examples/` 是样例工程文件;`docs/adr/` 是架构决策记录,被 spec 引用。
|
||||
|
||||
`spec/` 与实现部件**物理分离、平级共存**:谁是上游、谁向谁对齐,一眼可见。
|
||||
实现部件共用一个仓库根的 cargo workspace,使基础 crate(模型、typst 引擎)能被
|
||||
未来部件(如 exporter)复用,而非各自重造。
|
||||
`spec/` 与实现部件物理分离、平级共存:谁是上游、谁向谁对齐,一眼可见。实现部件共用一个
|
||||
仓库根的 cargo workspace,使基础 crate 能被未来部件复用。
|
||||
|
||||
## 宪法
|
||||
|
||||
这 5 条是 `spec/` 这份语义母本的定位与约束,是本仓库一切工作的前提。
|
||||
|
||||
1. **角色——Lean 是研发侧的上游参照。**
|
||||
`spec/` 用 Lean 编写,是开发者(领域专家)与 coding agent **共用**的 spec 工具,用来沉淀产品各部件的**语义**。它**不进入产品运行时**——产品里"站在 Lean 这个位置"的那个 checker 用什么技术实现,尚未决定;但那个东西的语义,先在 `spec/` 里固定下来。
|
||||
`spec/` 用 Lean 写,是开发者和 coding assistant 共用的 spec 工具,用来沉淀产品各部件
|
||||
的语义。它不进产品运行时——运行时那个 checker 用什么技术实现还没定,但它的语义先在
|
||||
`spec/` 里固定下来。
|
||||
|
||||
2. **对齐机制——Lean 只做上游参照。**
|
||||
不做 extract / codegen,不派生 conformance test,CI 里**没有** spec→实现的 gate。实现对齐 spec,由"开发者 review + agent 巡逻 diff"这个人肉环节承载。
|
||||
(CI 里的 `spec check` 只验 spec **自身**能否 type-check,即契约内部良构,不是 spec↔实现的对齐检查。)
|
||||
不做 extract / codegen,不派生 conformance test,CI 里没有 spec→实现的 gate。实现对齐
|
||||
spec,靠开发者 review 和 agent 巡逻 diff 这个人肉环节承载。(CI 里的 spec check 只验
|
||||
spec 自身能否 type-check,即契约内部良构,不是 spec↔实现对齐检查。)
|
||||
|
||||
3. **资产性 —— 由 review 纪律承载,无机器兜底。**
|
||||
这份仓库给你的是"精确、自洽、机器验内部良构的语义共识",**不是**"实现正确性保证"。spec 与实现之间那道缝,是我们自愿用人来守的——清醒地守,它就是资产;放任实现漂移而不回头同步,它就退化成最贵的过期文档。
|
||||
3. **资产性——由核对纪律承载,无机器兜底。**
|
||||
这份仓库给的是精确、自洽、机器验过内部良构的语义共识,不是实现正确性的保证。spec 与
|
||||
实现是否一致,没有自动闸门,要靠人工或 coding assistant 不定期(或每次改动后)核对;
|
||||
坚持核对,它就是有用的参照,否则只会变成过期的文档。
|
||||
|
||||
4. **形态——它是人机共识的契约。**
|
||||
契约必须**自包含**:凡契约未明文规定的,开发者与 agent 双方都不该假设。这比"文档"严格——type checker 会逼这份契约在结构上无洞。
|
||||
契约必须自包含:凡契约未明文规定的,开发者与 agent 双方都不该假设。这比"文档"严格——
|
||||
type checker 会逼这份契约在结构上无洞。
|
||||
|
||||
5. **深度判据——只收录分歧点。**
|
||||
一条语义该不该写进 Lean,取决于一句话:**"不写明,开发者与 agent 会不会各自做出不同假设?"** 会 → 进契约;显然的东西 / 纯 plumbing / 普通 CRUD 字段 → 不进(写进去只稀释信噪比、增加维护面)。
|
||||
深度上限不是 Lean 的表达力,而是**你愿意在每次实现变更时手动回头同步的量**——写得比你能维护的更深,多出来的部分会率先过期、反过来误导实现。
|
||||
一条语义该不该写进 Lean,取决于一句话:不写明,开发者与 agent 会不会各自做出不同
|
||||
假设?会,就进契约;显然的东西、纯基础设施、普通 CRUD 字段,不进(写进去只稀释信噪比、
|
||||
增加维护面)。深度上限不是 Lean 的表达力,而是你愿意在每次实现变更时手动回头同步的量。
|
||||
进了之后钉到多细,见 `spec/README.md` 的取舍判据。
|
||||
|
||||
## CI
|
||||
|
||||
`.gitea/workflows/spec-check.yml` 在每次 push / PR 时于 `spec/` 下跑 `lake build`,确保契约始终 type-check 通过(从第一天起就是"绿"的)。这是良构 gate,见宪法第 2 条。
|
||||
每次 push / PR 在 `spec/` 下跑 `lake build`,确保契约始终 type-check 通过。这是良构 gate,
|
||||
见宪法第 2 条。
|
||||
|
||||
@@ -1,50 +0,0 @@
|
||||
# ADR 0017: AgentSession Is Provider-Bound
|
||||
|
||||
## Status
|
||||
|
||||
Accepted.
|
||||
|
||||
## Context
|
||||
|
||||
ADR-0002 says a long-lived `AgentSession` can be reused by many runs, but never
|
||||
addressed the provider/model dimension. The agent layer is provider-agnostic
|
||||
(ADR-0001..0003 never required Claude specifically; the `@Claude` trigger name
|
||||
is a product brand, not a provider commitment). In practice the Hub routes
|
||||
model calls through an OpenAI-compatible client (e.g. OpenRouter), so a run may
|
||||
target different models — and the motivation for multi-model is **role-based
|
||||
routing**: drafting, reviewing, and triage suit different models.
|
||||
|
||||
That raises the question ADR-0002 left open: when a teacher switches model
|
||||
mid-project, does the `AgentSession` carry live context across the switch, or
|
||||
is it bound to a single provider/model?
|
||||
|
||||
## Decision
|
||||
|
||||
An `AgentSession` is **provider/model-bound**. A model or provider switch
|
||||
starts a new `AgentSession`. The `AgentSession` does not carry live context
|
||||
across a switch.
|
||||
|
||||
Cross-session continuity is not the session's job — it is carried by ADR-0003's
|
||||
project memory and anchors, which the Hub reads on demand when seeding a new
|
||||
run. This keeps B consistent with ADR-0003 ("the Hub avoids becoming a full
|
||||
chat history store"): session continuity and history continuity are the same
|
||||
mechanism, both via memory/anchors, never via a live cross-provider session.
|
||||
|
||||
Per-run model selection (the run carries its model) is the switching point.
|
||||
|
||||
## Consequences
|
||||
|
||||
- Switching model mid-project = new session; the new run seeds from project
|
||||
memory/anchors (ADR-0003), not the prior session's live context.
|
||||
- The agent layer is provider-agnostic: model calls go through an
|
||||
OpenAI-compatible client, and the tool-calling loop is delegated to the
|
||||
Vercel AI SDK (`generateText` + `tool`). The provider seam is the SDK's
|
||||
`LanguageModel` interface, not a hand-rolled loop; swapping provider is
|
||||
swapping the `createOpenAICompatible` factory, not rewriting the loop. No
|
||||
hard dependency on a single-vendor agent SDK.
|
||||
- Role-based model routing (different run kinds default to different models) is
|
||||
a product/admin configuration concern, not a spec invariant.
|
||||
- "AgentSession reused by many runs" (ADR-0002) holds *within* one
|
||||
provider/model; it does not span a switch.
|
||||
- The `@Claude` trigger name remains the product mention brand regardless of the
|
||||
backing model.
|
||||
@@ -1,23 +0,0 @@
|
||||
# Hub runtime configuration. Copy to .env and fill in.
|
||||
|
||||
# PostgreSQL connection string. Used by Prisma and the Hub server.
|
||||
DATABASE_URL="postgresql://paradigm:paradigm@127.0.0.1:5432/paradigm"
|
||||
|
||||
# OpenRouter (or any OpenAI-compatible) API key + base URL.
|
||||
# The Hub's agent layer is provider-agnostic (ADR-0017); this points the
|
||||
# OpenAI-compatible client at OpenRouter by default.
|
||||
OPENROUTER_API_KEY=""
|
||||
# Optional: override the base URL (e.g. direct vendor API, local gateway).
|
||||
# OPENROUTER_BASE_URL="https://openrouter.ai/api/v1"
|
||||
|
||||
# Hub server port. Defaults to 8788.
|
||||
PORT=8788
|
||||
|
||||
# Feishu (lark) bot credentials. The bot receives @mentions in project groups.
|
||||
FEISHU_APP_ID=""
|
||||
FEISHU_APP_SECRET=""
|
||||
FEISHU_BOT_OPEN_ID=""
|
||||
|
||||
# Path to the `cph` binary (the Courseware-side checker, ADR-0016).
|
||||
# Defaults to `cph` on PATH if unset.
|
||||
# CPH_BIN="/usr/local/bin/cph"
|
||||
@@ -1,6 +0,0 @@
|
||||
node_modules/
|
||||
dist/
|
||||
*.log
|
||||
.env
|
||||
.env.*
|
||||
!.env.example
|
||||
@@ -1,21 +0,0 @@
|
||||
[Unit]
|
||||
Description=Curriculum Project Hub (Feishu agent + cph)
|
||||
After=network-online.target postgresql.service
|
||||
Wants=network-online.target
|
||||
|
||||
[Service]
|
||||
Type=simple
|
||||
User=__SERVICE_USER__
|
||||
WorkingDirectory=__HUB_DIR__
|
||||
EnvironmentFile=__ENV_FILE__
|
||||
# Run prisma migrations before each start, then launch the Hub.
|
||||
ExecStartPre=__NODE_BIN__ __HUB_DIR__/node_modules/prisma/build/index.js migrate deploy --schema __HUB_DIR__/prisma/schema.prisma
|
||||
ExecStart=__NODE_BIN__ __HUB_DIR__/dist/server.js
|
||||
Restart=on-failure
|
||||
RestartSec=5
|
||||
# Graceful shutdown: lark ws close + in-flight runs.
|
||||
KillSignal=SIGTERM
|
||||
TimeoutStopSec=30
|
||||
|
||||
[Install]
|
||||
WantedBy=multi-user.target
|
||||
@@ -1,47 +0,0 @@
|
||||
#!/usr/bin/env bash
|
||||
# Deploy the Hub to a host: rsync the repo, install deps, build, restart service.
|
||||
#
|
||||
# Configure these env vars (e.g. in CI secrets):
|
||||
# PLATFORM_DEPLOY_HOST required
|
||||
# PLATFORM_DEPLOY_SSH_KEY required (private key for the deploy user)
|
||||
# PLATFORM_DEPLOY_USER optional, defaults to deploy
|
||||
# PLATFORM_DEPLOY_PORT optional, defaults to 22
|
||||
# PLATFORM_DEPLOY_BASE optional, defaults to /srv/curriculum-project-hub
|
||||
#
|
||||
# The target host must have Node.js, npm, rsync, PostgreSQL, systemd, and a
|
||||
# writable $PLATFORM_DEPLOY_BASE. Use a dedicated `deploy` user that has
|
||||
# passwordless sudo for:
|
||||
# systemctl restart cph-hub.service
|
||||
# systemctl is-active --quiet cph-hub.service
|
||||
set -euo pipefail
|
||||
|
||||
HOST="${PLATFORM_DEPLOY_HOST:?PLATFORM_DEPLOY_HOST required}"
|
||||
SSH_KEY="${PLATFORM_DEPLOY_SSH_KEY:?PLATFORM_DEPLOY_SSH_KEY required}"
|
||||
DEPLOY_USER="${PLATFORM_DEPLOY_USER:-deploy}"
|
||||
PORT="${PLATFORM_DEPLOY_PORT:-22}"
|
||||
BASE="${PLATFORM_DEPLOY_BASE:-/srv/curriculum-project-hub}"
|
||||
HUB_DIR="$BASE/hub"
|
||||
SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
|
||||
REPO_ROOT="$(cd "$SCRIPT_DIR/../.." && pwd)"
|
||||
|
||||
SSH_OPTS=(-i "$SSH_KEY" -p "$PORT" -o StrictHostKeyChecking=accept-new)
|
||||
|
||||
# 1. Rsync the hub/ directory (exclude node_modules/dist, they rebuild on host).
|
||||
rsync -az --delete \
|
||||
--exclude node_modules --exclude dist --exclude .env \
|
||||
-e "ssh ${SSH_OPTS[*]}" \
|
||||
"$REPO_ROOT/hub/" "$DEPLOY_USER@$HOST:$HUB_DIR/"
|
||||
|
||||
# 2. Install deps + build on the host.
|
||||
ssh "${SSH_OPTS[@]}" "$DEPLOY_USER@$HOST" "cd '$HUB_DIR' && npm ci && npm run build"
|
||||
|
||||
# 3. Ensure the service is installed (idempotent), then restart.
|
||||
ssh "${SSH_OPTS[@]}" "$DEPLOY_USER@$HOST" "
|
||||
BASE='$BASE' HUB_DIR='$HUB_DIR' bash '$HUB_DIR/deploy/install_service.sh' || true
|
||||
sudo systemctl restart cph-hub.service
|
||||
sleep 2
|
||||
sudo systemctl is-active --quiet cph-hub.service || { echo 'service failed to start'; exit 1; }
|
||||
curl -sf http://127.0.0.1:8788/api/healthz || { echo 'healthz failed'; exit 1; }
|
||||
"
|
||||
|
||||
echo "Deployed cph-hub to $HOST ($HUB_DIR)"
|
||||
@@ -1,62 +0,0 @@
|
||||
#!/usr/bin/env bash
|
||||
# Install the cph-hub systemd service on a host. Idempotent.
|
||||
#
|
||||
# Prerequisites already on the host: Node.js, npm, PostgreSQL, systemd.
|
||||
# The Hub repo is expected at HUB_DIR (default /srv/curriculum-project-hub/hub)
|
||||
# with `npm ci` + `npm run build` already run by deploy_platform.sh.
|
||||
#
|
||||
# Usage:
|
||||
# sudo BASE=/srv/curriculum-project-hub bash deploy/install_service.sh
|
||||
set -euo pipefail
|
||||
|
||||
BASE="${BASE:-/srv/curriculum-project-hub}"
|
||||
HUB_DIR="${HUB_DIR:-$BASE/hub}"
|
||||
SERVICE_USER="${SERVICE_USER:-root}"
|
||||
HOST="${HOST:-127.0.0.1}"
|
||||
PORT="${PORT:-8788}"
|
||||
ENV_FILE="${ENV_FILE:-$BASE/.secrets/platform.env}"
|
||||
NODE_BIN="${NODE_BIN:-$(command -v node || true)}"
|
||||
|
||||
if [ -z "$NODE_BIN" ]; then
|
||||
echo "node must be on PATH, or set NODE_BIN." >&2
|
||||
exit 1
|
||||
fi
|
||||
if [ ! -d "$HUB_DIR" ]; then
|
||||
echo "HUB_DIR not found: $HUB_DIR (set HUB_DIR or clone the repo there)." >&2
|
||||
exit 1
|
||||
fi
|
||||
if [ ! -f "$HUB_DIR/dist/server.js" ]; then
|
||||
echo "build missing: run 'npm ci && npm run build' in $HUB_DIR first." >&2
|
||||
exit 1
|
||||
fi
|
||||
|
||||
# Seed the env file if absent. Secrets stay on the server, never in the repo.
|
||||
if [ ! -f "$ENV_FILE" ]; then
|
||||
install -d -m 0700 "$(dirname "$ENV_FILE")"
|
||||
cat >"$ENV_FILE" <<EOF
|
||||
NODE_ENV=production
|
||||
DATABASE_URL=postgresql://paradigm:change-me@127.0.0.1:5432/paradigm
|
||||
OPENROUTER_API_KEY=
|
||||
FEISHU_APP_ID=
|
||||
FEISHU_APP_SECRET=
|
||||
FEISHU_BOT_OPEN_ID=
|
||||
PORT=$PORT
|
||||
HOST=$HOST
|
||||
EOF
|
||||
echo "Seeded $ENV_FILE — edit it to fill in OPENROUTER_API_KEY and Feishu creds, then re-run."
|
||||
exit 0
|
||||
fi
|
||||
|
||||
# Render the unit with concrete paths.
|
||||
UNIT=/etc/systemd/system/cph-hub.service
|
||||
sed \
|
||||
-e "s|__SERVICE_USER__|$SERVICE_USER|g" \
|
||||
-e "s|__HUB_DIR__|$HUB_DIR|g" \
|
||||
-e "s|__ENV_FILE__|$ENV_FILE|g" \
|
||||
-e "s|__NODE_BIN__|$NODE_BIN|g" \
|
||||
"$HUB_DIR/deploy/cph-hub.service" >"$UNIT"
|
||||
|
||||
systemctl daemon-reload
|
||||
systemctl enable cph-hub.service
|
||||
echo "Installed cph-hub.service. Start with: systemctl start cph-hub"
|
||||
echo "Check health: curl http://127.0.0.1:$PORT/api/healthz"
|
||||
Generated
-3558
File diff suppressed because it is too large
Load Diff
@@ -1,38 +0,0 @@
|
||||
{
|
||||
"name": "@paradigm/hub",
|
||||
"version": "0.0.0",
|
||||
"private": true,
|
||||
"type": "module",
|
||||
"engines": {
|
||||
"node": ">=20"
|
||||
},
|
||||
"dependencies": {
|
||||
"@ai-sdk/openai-compatible": "^3.0.5",
|
||||
"@fastify/cookie": "^11.0.2",
|
||||
"@larksuiteoapi/node-sdk": "^1.66.1",
|
||||
"@prisma/client": "^6.19.3",
|
||||
"ai": "^7.0.16",
|
||||
"dotenv": "^17.4.2",
|
||||
"fastify": "^5.8.5",
|
||||
"zod": "^4.4.3"
|
||||
},
|
||||
"devDependencies": {
|
||||
"prisma": "^6.19.3",
|
||||
"tsx": "^4.19.0",
|
||||
"typescript": "^5.7.0",
|
||||
"vitest": "^4.1.10"
|
||||
},
|
||||
"description": "Curriculum Project Hub — Feishu-group collaboration + provider-agnostic agent runtime. Aligns to spec/System (ADR-0001..0004, 0017).",
|
||||
"scripts": {
|
||||
"dev": "tsx watch src/server.ts",
|
||||
"build": "tsc -p tsconfig.json",
|
||||
"start": "node dist/server.js",
|
||||
"check": "tsc -p tsconfig.json --noEmit",
|
||||
"prisma:generate": "prisma generate --schema prisma/schema.prisma",
|
||||
"prisma:validate": "DATABASE_URL=${DATABASE_URL:-postgresql://stub:stub@127.0.0.1:5432/stub} prisma validate --schema prisma/schema.prisma",
|
||||
"prisma:migrate": "DATABASE_URL=${DATABASE_URL:-postgresql://paradigm:paradigm@127.0.0.1:5432/paradigm} prisma migrate deploy --schema prisma/schema.prisma",
|
||||
"deploy": "bash deploy/deploy_platform.sh",
|
||||
"test": "vitest run",
|
||||
"test:watch": "vitest"
|
||||
}
|
||||
}
|
||||
@@ -1,271 +0,0 @@
|
||||
-- CreateEnum
|
||||
CREATE TYPE "PlatformRole" AS ENUM ('ADMIN', 'TEACHER');
|
||||
|
||||
-- CreateEnum
|
||||
CREATE TYPE "AgentRunStatus" AS ENUM ('ACTIVE', 'WAITING_FOR_USER', 'COMPLETED', 'FAILED', 'TIMED_OUT', 'CANCELED');
|
||||
|
||||
-- CreateEnum
|
||||
CREATE TYPE "AgentEntrypoint" AS ENUM ('FEISHU', 'WEB', 'CLI');
|
||||
|
||||
-- CreateEnum
|
||||
CREATE TYPE "PermissionRole" AS ENUM ('READ', 'EDIT', 'MANAGE');
|
||||
|
||||
-- CreateEnum
|
||||
CREATE TYPE "PermissionResourceType" AS ENUM ('PROJECT', 'ARTIFACT', 'PROJECT_GROUP');
|
||||
|
||||
-- CreateTable
|
||||
CREATE TABLE "User" (
|
||||
"id" TEXT NOT NULL,
|
||||
"feishuOpenId" TEXT NOT NULL,
|
||||
"displayName" TEXT NOT NULL,
|
||||
"avatarUrl" TEXT,
|
||||
"createdAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
|
||||
"updatedAt" TIMESTAMP(3) NOT NULL,
|
||||
|
||||
CONSTRAINT "User_pkey" PRIMARY KEY ("id")
|
||||
);
|
||||
|
||||
-- CreateTable
|
||||
CREATE TABLE "PlatformRoleAssignment" (
|
||||
"id" TEXT NOT NULL,
|
||||
"userId" TEXT NOT NULL,
|
||||
"role" "PlatformRole" NOT NULL,
|
||||
"createdAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
|
||||
"revokedAt" TIMESTAMP(3),
|
||||
|
||||
CONSTRAINT "PlatformRoleAssignment_pkey" PRIMARY KEY ("id")
|
||||
);
|
||||
|
||||
-- CreateTable
|
||||
CREATE TABLE "Project" (
|
||||
"id" TEXT NOT NULL,
|
||||
"name" TEXT NOT NULL,
|
||||
"workspaceDir" TEXT NOT NULL,
|
||||
"createdByUserId" TEXT,
|
||||
"createdAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
|
||||
"updatedAt" TIMESTAMP(3) NOT NULL,
|
||||
"archivedAt" TIMESTAMP(3),
|
||||
|
||||
CONSTRAINT "Project_pkey" PRIMARY KEY ("id")
|
||||
);
|
||||
|
||||
-- CreateTable
|
||||
CREATE TABLE "ProjectGroupBinding" (
|
||||
"id" TEXT NOT NULL,
|
||||
"projectId" TEXT NOT NULL,
|
||||
"chatId" TEXT NOT NULL,
|
||||
"createdByUserId" TEXT,
|
||||
"createdAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
|
||||
"updatedAt" TIMESTAMP(3) NOT NULL,
|
||||
|
||||
CONSTRAINT "ProjectGroupBinding_pkey" PRIMARY KEY ("id")
|
||||
);
|
||||
|
||||
-- CreateTable
|
||||
CREATE TABLE "AgentSession" (
|
||||
"id" TEXT NOT NULL,
|
||||
"projectId" TEXT NOT NULL,
|
||||
"provider" TEXT NOT NULL,
|
||||
"model" TEXT NOT NULL,
|
||||
"title" TEXT,
|
||||
"metadata" JSONB NOT NULL,
|
||||
"createdAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
|
||||
"updatedAt" TIMESTAMP(3) NOT NULL,
|
||||
"archivedAt" TIMESTAMP(3),
|
||||
|
||||
CONSTRAINT "AgentSession_pkey" PRIMARY KEY ("id")
|
||||
);
|
||||
|
||||
-- CreateTable
|
||||
CREATE TABLE "AgentRun" (
|
||||
"id" TEXT NOT NULL,
|
||||
"projectId" TEXT NOT NULL,
|
||||
"sessionId" TEXT,
|
||||
"requestedByUserId" TEXT,
|
||||
"entrypoint" "AgentEntrypoint" NOT NULL,
|
||||
"status" "AgentRunStatus" NOT NULL DEFAULT 'ACTIVE',
|
||||
"prompt" TEXT NOT NULL,
|
||||
"model" TEXT NOT NULL,
|
||||
"provider" TEXT NOT NULL,
|
||||
"summary" TEXT,
|
||||
"inputTokens" INTEGER,
|
||||
"outputTokens" INTEGER,
|
||||
"metadata" JSONB NOT NULL,
|
||||
"error" TEXT,
|
||||
"startedAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
|
||||
"finishedAt" TIMESTAMP(3),
|
||||
"updatedAt" TIMESTAMP(3) NOT NULL,
|
||||
|
||||
CONSTRAINT "AgentRun_pkey" PRIMARY KEY ("id")
|
||||
);
|
||||
|
||||
-- CreateTable
|
||||
CREATE TABLE "ProjectAgentLock" (
|
||||
"projectId" TEXT NOT NULL,
|
||||
"runId" TEXT NOT NULL,
|
||||
"holderUserId" TEXT,
|
||||
"acquiredAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
|
||||
"expiresAt" TIMESTAMP(3),
|
||||
|
||||
CONSTRAINT "ProjectAgentLock_pkey" PRIMARY KEY ("projectId")
|
||||
);
|
||||
|
||||
-- CreateTable
|
||||
CREATE TABLE "PermissionGrant" (
|
||||
"id" TEXT NOT NULL,
|
||||
"resourceType" "PermissionResourceType" NOT NULL,
|
||||
"resourceId" TEXT NOT NULL,
|
||||
"principal" TEXT NOT NULL,
|
||||
"role" "PermissionRole" NOT NULL,
|
||||
"createdByUserId" TEXT,
|
||||
"createdAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
|
||||
"revokedAt" TIMESTAMP(3),
|
||||
|
||||
CONSTRAINT "PermissionGrant_pkey" PRIMARY KEY ("id")
|
||||
);
|
||||
|
||||
-- CreateTable
|
||||
CREATE TABLE "PermissionSettings" (
|
||||
"id" TEXT NOT NULL,
|
||||
"resourceType" "PermissionResourceType" NOT NULL,
|
||||
"resourceId" TEXT NOT NULL,
|
||||
"externalShare" TEXT NOT NULL,
|
||||
"comment" TEXT NOT NULL,
|
||||
"copyDownload" TEXT NOT NULL,
|
||||
"collaboratorMgmt" TEXT NOT NULL,
|
||||
"agentTrigger" TEXT NOT NULL,
|
||||
"agentCancel" TEXT NOT NULL,
|
||||
"createdAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
|
||||
"updatedAt" TIMESTAMP(3) NOT NULL,
|
||||
|
||||
CONSTRAINT "PermissionSettings_pkey" PRIMARY KEY ("id")
|
||||
);
|
||||
|
||||
-- CreateTable
|
||||
CREATE TABLE "AuditEntry" (
|
||||
"id" TEXT NOT NULL,
|
||||
"runId" TEXT,
|
||||
"actorUserId" TEXT,
|
||||
"action" TEXT NOT NULL,
|
||||
"metadata" JSONB NOT NULL,
|
||||
"createdAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
|
||||
|
||||
CONSTRAINT "AuditEntry_pkey" PRIMARY KEY ("id")
|
||||
);
|
||||
|
||||
-- CreateIndex
|
||||
CREATE UNIQUE INDEX "User_feishuOpenId_key" ON "User"("feishuOpenId");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE INDEX "PlatformRoleAssignment_userId_revokedAt_idx" ON "PlatformRoleAssignment"("userId", "revokedAt");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE INDEX "PlatformRoleAssignment_role_revokedAt_idx" ON "PlatformRoleAssignment"("role", "revokedAt");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE INDEX "Project_archivedAt_idx" ON "Project"("archivedAt");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE UNIQUE INDEX "ProjectGroupBinding_projectId_key" ON "ProjectGroupBinding"("projectId");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE UNIQUE INDEX "ProjectGroupBinding_chatId_key" ON "ProjectGroupBinding"("chatId");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE INDEX "ProjectGroupBinding_chatId_idx" ON "ProjectGroupBinding"("chatId");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE INDEX "AgentSession_projectId_archivedAt_idx" ON "AgentSession"("projectId", "archivedAt");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE INDEX "AgentSession_provider_model_idx" ON "AgentSession"("provider", "model");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE INDEX "AgentSession_updatedAt_idx" ON "AgentSession"("updatedAt");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE INDEX "AgentRun_projectId_status_idx" ON "AgentRun"("projectId", "status");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE INDEX "AgentRun_sessionId_idx" ON "AgentRun"("sessionId");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE INDEX "AgentRun_requestedByUserId_idx" ON "AgentRun"("requestedByUserId");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE INDEX "AgentRun_updatedAt_idx" ON "AgentRun"("updatedAt");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE UNIQUE INDEX "ProjectAgentLock_runId_key" ON "ProjectAgentLock"("runId");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE INDEX "ProjectAgentLock_expiresAt_idx" ON "ProjectAgentLock"("expiresAt");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE INDEX "PermissionGrant_resourceType_resourceId_revokedAt_idx" ON "PermissionGrant"("resourceType", "resourceId", "revokedAt");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE INDEX "PermissionGrant_principal_revokedAt_idx" ON "PermissionGrant"("principal", "revokedAt");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE UNIQUE INDEX "PermissionGrant_resourceType_resourceId_principal_role_revo_key" ON "PermissionGrant"("resourceType", "resourceId", "principal", "role", "revokedAt");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE INDEX "PermissionSettings_resourceType_resourceId_idx" ON "PermissionSettings"("resourceType", "resourceId");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE UNIQUE INDEX "PermissionSettings_resourceType_resourceId_key" ON "PermissionSettings"("resourceType", "resourceId");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE INDEX "AuditEntry_runId_idx" ON "AuditEntry"("runId");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE INDEX "AuditEntry_actorUserId_idx" ON "AuditEntry"("actorUserId");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE INDEX "AuditEntry_createdAt_idx" ON "AuditEntry"("createdAt");
|
||||
|
||||
-- AddForeignKey
|
||||
ALTER TABLE "PlatformRoleAssignment" ADD CONSTRAINT "PlatformRoleAssignment_userId_fkey" FOREIGN KEY ("userId") REFERENCES "User"("id") ON DELETE CASCADE ON UPDATE CASCADE;
|
||||
|
||||
-- AddForeignKey
|
||||
ALTER TABLE "Project" ADD CONSTRAINT "Project_createdByUserId_fkey" FOREIGN KEY ("createdByUserId") REFERENCES "User"("id") ON DELETE SET NULL ON UPDATE CASCADE;
|
||||
|
||||
-- AddForeignKey
|
||||
ALTER TABLE "ProjectGroupBinding" ADD CONSTRAINT "ProjectGroupBinding_projectId_fkey" FOREIGN KEY ("projectId") REFERENCES "Project"("id") ON DELETE CASCADE ON UPDATE CASCADE;
|
||||
|
||||
-- AddForeignKey
|
||||
ALTER TABLE "ProjectGroupBinding" ADD CONSTRAINT "ProjectGroupBinding_createdByUserId_fkey" FOREIGN KEY ("createdByUserId") REFERENCES "User"("id") ON DELETE SET NULL ON UPDATE CASCADE;
|
||||
|
||||
-- AddForeignKey
|
||||
ALTER TABLE "AgentSession" ADD CONSTRAINT "AgentSession_projectId_fkey" FOREIGN KEY ("projectId") REFERENCES "Project"("id") ON DELETE CASCADE ON UPDATE CASCADE;
|
||||
|
||||
-- AddForeignKey
|
||||
ALTER TABLE "AgentRun" ADD CONSTRAINT "AgentRun_projectId_fkey" FOREIGN KEY ("projectId") REFERENCES "Project"("id") ON DELETE CASCADE ON UPDATE CASCADE;
|
||||
|
||||
-- AddForeignKey
|
||||
ALTER TABLE "AgentRun" ADD CONSTRAINT "AgentRun_sessionId_fkey" FOREIGN KEY ("sessionId") REFERENCES "AgentSession"("id") ON DELETE SET NULL ON UPDATE CASCADE;
|
||||
|
||||
-- AddForeignKey
|
||||
ALTER TABLE "AgentRun" ADD CONSTRAINT "AgentRun_requestedByUserId_fkey" FOREIGN KEY ("requestedByUserId") REFERENCES "User"("id") ON DELETE SET NULL ON UPDATE CASCADE;
|
||||
|
||||
-- AddForeignKey
|
||||
ALTER TABLE "ProjectAgentLock" ADD CONSTRAINT "ProjectAgentLock_projectId_fkey" FOREIGN KEY ("projectId") REFERENCES "Project"("id") ON DELETE CASCADE ON UPDATE CASCADE;
|
||||
|
||||
-- AddForeignKey
|
||||
ALTER TABLE "ProjectAgentLock" ADD CONSTRAINT "ProjectAgentLock_runId_fkey" FOREIGN KEY ("runId") REFERENCES "AgentRun"("id") ON DELETE CASCADE ON UPDATE CASCADE;
|
||||
|
||||
-- AddForeignKey
|
||||
ALTER TABLE "ProjectAgentLock" ADD CONSTRAINT "ProjectAgentLock_holderUserId_fkey" FOREIGN KEY ("holderUserId") REFERENCES "User"("id") ON DELETE SET NULL ON UPDATE CASCADE;
|
||||
|
||||
-- AddForeignKey
|
||||
ALTER TABLE "PermissionGrant" ADD CONSTRAINT "PermissionGrant_resourceId_fkey" FOREIGN KEY ("resourceId") REFERENCES "Project"("id") ON DELETE CASCADE ON UPDATE CASCADE;
|
||||
|
||||
-- AddForeignKey
|
||||
ALTER TABLE "PermissionGrant" ADD CONSTRAINT "PermissionGrant_createdByUserId_fkey" FOREIGN KEY ("createdByUserId") REFERENCES "User"("id") ON DELETE SET NULL ON UPDATE CASCADE;
|
||||
|
||||
-- AddForeignKey
|
||||
ALTER TABLE "PermissionSettings" ADD CONSTRAINT "PermissionSettings_resourceId_fkey" FOREIGN KEY ("resourceId") REFERENCES "Project"("id") ON DELETE CASCADE ON UPDATE CASCADE;
|
||||
|
||||
-- AddForeignKey
|
||||
ALTER TABLE "AuditEntry" ADD CONSTRAINT "AuditEntry_actorUserId_fkey" FOREIGN KEY ("actorUserId") REFERENCES "User"("id") ON DELETE SET NULL ON UPDATE CASCADE;
|
||||
@@ -1,27 +0,0 @@
|
||||
-- CreateTable
|
||||
CREATE TABLE "RoleTriggerGrant" (
|
||||
"id" TEXT NOT NULL,
|
||||
"projectId" TEXT NOT NULL,
|
||||
"roleId" TEXT NOT NULL,
|
||||
"principal" TEXT NOT NULL,
|
||||
"createdByUserId" TEXT,
|
||||
"createdAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
|
||||
"revokedAt" TIMESTAMP(3),
|
||||
|
||||
CONSTRAINT "RoleTriggerGrant_pkey" PRIMARY KEY ("id")
|
||||
);
|
||||
|
||||
-- CreateIndex
|
||||
CREATE INDEX "RoleTriggerGrant_projectId_roleId_revokedAt_idx" ON "RoleTriggerGrant"("projectId", "roleId", "revokedAt");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE INDEX "RoleTriggerGrant_principal_revokedAt_idx" ON "RoleTriggerGrant"("principal", "revokedAt");
|
||||
|
||||
-- CreateIndex
|
||||
CREATE UNIQUE INDEX "RoleTriggerGrant_projectId_roleId_principal_revokedAt_key" ON "RoleTriggerGrant"("projectId", "roleId", "principal", "revokedAt");
|
||||
|
||||
-- AddForeignKey
|
||||
ALTER TABLE "RoleTriggerGrant" ADD CONSTRAINT "RoleTriggerGrant_projectId_fkey" FOREIGN KEY ("projectId") REFERENCES "Project"("id") ON DELETE CASCADE ON UPDATE CASCADE;
|
||||
|
||||
-- AddForeignKey
|
||||
ALTER TABLE "RoleTriggerGrant" ADD CONSTRAINT "RoleTriggerGrant_createdByUserId_fkey" FOREIGN KEY ("createdByUserId") REFERENCES "User"("id") ON DELETE SET NULL ON UPDATE CASCADE;
|
||||
@@ -1,23 +0,0 @@
|
||||
-- FeishuEventReceipt: idempotency for inbound ws events (at-least-once redelivery).
|
||||
CREATE TABLE "FeishuEventReceipt" (
|
||||
"id" TEXT NOT NULL,
|
||||
"eventId" TEXT NOT NULL,
|
||||
"eventType" TEXT NOT NULL,
|
||||
"messageId" TEXT,
|
||||
"receivedAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
|
||||
|
||||
CONSTRAINT "FeishuEventReceipt_pkey" PRIMARY KEY ("id")
|
||||
);
|
||||
|
||||
CREATE UNIQUE INDEX "FeishuEventReceipt_eventId_key" ON "FeishuEventReceipt"("eventId");
|
||||
CREATE INDEX "FeishuEventReceipt_eventType_idx" ON "FeishuEventReceipt"("eventType");
|
||||
CREATE INDEX "FeishuEventReceipt_messageId_idx" ON "FeishuEventReceipt"("messageId");
|
||||
CREATE INDEX "FeishuEventReceipt_receivedAt_idx" ON "FeishuEventReceipt"("receivedAt");
|
||||
|
||||
-- AuditEntry: add projectId so audit points before/without a run (permission
|
||||
-- denials, slash commands) are locatable to a project.
|
||||
ALTER TABLE "AuditEntry" ADD COLUMN "projectId" TEXT;
|
||||
|
||||
CREATE INDEX "AuditEntry_projectId_createdAt_idx" ON "AuditEntry"("projectId", "createdAt");
|
||||
|
||||
ALTER TABLE "AuditEntry" ADD CONSTRAINT "AuditEntry_projectId_fkey" FOREIGN KEY ("projectId") REFERENCES "Project"("id") ON DELETE SET NULL ON UPDATE CASCADE;
|
||||
@@ -1,3 +0,0 @@
|
||||
# Please do not edit this file manually
|
||||
# It should be added in your version-control system (e.g., Git)
|
||||
provider = "postgresql"
|
||||
@@ -1,333 +0,0 @@
|
||||
// Prisma schema for Curriculum Project Hub.
|
||||
//
|
||||
// Aligns to spec/System (ADR-0001..0004, 0017). Key divergences from the
|
||||
// legacy teaching-material-host-service schema, each deliberate:
|
||||
//
|
||||
// - No AgentSession.claudeSessionId. ADR-0017: session is provider/model-
|
||||
// bound, not Claude-bound; `provider`+`model` replace it. Switching model
|
||||
// = new session, so the unique constraint is on the session id alone.
|
||||
// - PermissionRole enum = read/edit/manage (ADR-0004 capability lattice),
|
||||
// distinct from platform UserRole (admin/teacher) — legacy conflated them.
|
||||
// - ProjectGroupBinding is project→chat only (ADR-0001 1:1); legacy mixed
|
||||
// user/chat targets into one binding table.
|
||||
// - PermissionGrant + PermissionSettings land (ADR-0004), missing in legacy.
|
||||
// - AgentRunStatus adds WAITING_FOR_USER + TIMED_OUT (spec RunState; enum
|
||||
// completeness OPEN — add states without a schema migration war).
|
||||
|
||||
generator client {
|
||||
provider = "prisma-client-js"
|
||||
}
|
||||
|
||||
datasource db {
|
||||
provider = "postgresql"
|
||||
url = env("DATABASE_URL")
|
||||
}
|
||||
|
||||
// --- Platform identity ---------------------------------------------------
|
||||
|
||||
/// A Feishu user known to the Hub. principal sub-typology is OPEN (ADR-0004).
|
||||
model User {
|
||||
id String @id @default(cuid())
|
||||
feishuOpenId String @unique
|
||||
displayName String
|
||||
avatarUrl String?
|
||||
createdAt DateTime @default(now())
|
||||
updatedAt DateTime @updatedAt
|
||||
|
||||
platformRoles PlatformRoleAssignment[]
|
||||
createdProjects Project[] @relation("projectCreator")
|
||||
requestedRuns AgentRun[] @relation("runRequester")
|
||||
heldLocks ProjectAgentLock[] @relation("lockHolder")
|
||||
feishuBindings ProjectGroupBinding[] @relation("bindingCreator")
|
||||
permissionGrants PermissionGrant[] @relation("grantCreator")
|
||||
roleTriggerGrants RoleTriggerGrant[] @relation("roleGrantCreator")
|
||||
auditEntries AuditEntry[] @relation("auditActor")
|
||||
}
|
||||
|
||||
/// Platform-level role (admin/teacher). Distinct from ADR-0004 PermissionRole.
|
||||
/// `admin` is the only override path for force-release (spec RequiresAdmin).
|
||||
model PlatformRoleAssignment {
|
||||
id String @id @default(cuid())
|
||||
userId String
|
||||
role PlatformRole
|
||||
createdAt DateTime @default(now())
|
||||
revokedAt DateTime?
|
||||
|
||||
user User @relation(fields: [userId], references: [id], onDelete: Cascade)
|
||||
|
||||
@@index([userId, revokedAt])
|
||||
@@index([role, revokedAt])
|
||||
}
|
||||
|
||||
enum PlatformRole {
|
||||
ADMIN
|
||||
TEACHER
|
||||
}
|
||||
|
||||
// --- Project & Feishu binding (ADR-0001) ---------------------------------
|
||||
|
||||
model Project {
|
||||
id String @id @default(cuid())
|
||||
name String
|
||||
workspaceDir String
|
||||
createdByUserId String?
|
||||
createdAt DateTime @default(now())
|
||||
updatedAt DateTime @updatedAt
|
||||
archivedAt DateTime?
|
||||
|
||||
createdBy User? @relation("projectCreator", fields: [createdByUserId], references: [id], onDelete: SetNull)
|
||||
groupBinding ProjectGroupBinding?
|
||||
agentSessions AgentSession[]
|
||||
agentRuns AgentRun[]
|
||||
agentLock ProjectAgentLock?
|
||||
permissionGrants PermissionGrant[] @relation("projectGrants")
|
||||
permissionSettings PermissionSettings[] @relation("projectSettings")
|
||||
roleTriggerGrants RoleTriggerGrant[] @relation("projectRoleGrants")
|
||||
auditEntries AuditEntry[] @relation("projectAudit")
|
||||
|
||||
@@index([archivedAt])
|
||||
}
|
||||
|
||||
/// ADR-0001: one project ↔ one Feishu chat (1:1). `chatId` is unique ⇒
|
||||
/// GroupBinding.WellFormed's injectivity half (no two projects bind one chat).
|
||||
/// The "at most one binding per project" half is enforced by the 1:1 relation.
|
||||
/// Group dissolution lifecycle is OPEN (ADR-0001 Consequences) — not modeled
|
||||
/// here; archival is a future policy, not a current column.
|
||||
model ProjectGroupBinding {
|
||||
id String @id @default(cuid())
|
||||
projectId String @unique
|
||||
chatId String @unique
|
||||
createdByUserId String?
|
||||
createdAt DateTime @default(now())
|
||||
updatedAt DateTime @updatedAt
|
||||
|
||||
project Project @relation(fields: [projectId], references: [id], onDelete: Cascade)
|
||||
createdBy User? @relation("bindingCreator", fields: [createdByUserId], references: [id], onDelete: SetNull)
|
||||
|
||||
@@index([chatId])
|
||||
}
|
||||
|
||||
// --- AgentRun, session, lock (ADR-0002, 0017) -----------------------------
|
||||
|
||||
/// ADR-0017: session is provider/model-bound. No claudeSessionId; `provider`
|
||||
/// + `model` capture the binding. Same provider+model ⇒ reuse across runs
|
||||
/// (ADR-0002); a switch ⇒ new session.
|
||||
model AgentSession {
|
||||
id String @id @default(cuid())
|
||||
projectId String
|
||||
provider String
|
||||
model String
|
||||
title String?
|
||||
metadata Json
|
||||
createdAt DateTime @default(now())
|
||||
updatedAt DateTime @updatedAt
|
||||
archivedAt DateTime?
|
||||
|
||||
project Project @relation(fields: [projectId], references: [id], onDelete: Cascade)
|
||||
runs AgentRun[]
|
||||
|
||||
@@index([projectId, archivedAt])
|
||||
@@index([provider, model])
|
||||
@@index([updatedAt])
|
||||
}
|
||||
|
||||
/// spec RunState: active/waitingForUser/completed/failed/timedOut/canceled.
|
||||
/// Enum completeness OPEN (Run.lean:12) — adding a state is a value add, not a
|
||||
/// spec breach. DB mirrors the current enum.
|
||||
enum AgentRunStatus {
|
||||
ACTIVE
|
||||
WAITING_FOR_USER
|
||||
COMPLETED
|
||||
FAILED
|
||||
TIMED_OUT
|
||||
CANCELED
|
||||
}
|
||||
|
||||
enum AgentEntrypoint {
|
||||
FEISHU
|
||||
WEB
|
||||
CLI
|
||||
}
|
||||
|
||||
model AgentRun {
|
||||
id String @id @default(cuid())
|
||||
projectId String
|
||||
sessionId String?
|
||||
requestedByUserId String?
|
||||
entrypoint AgentEntrypoint
|
||||
status AgentRunStatus @default(ACTIVE)
|
||||
prompt String
|
||||
model String
|
||||
provider String
|
||||
summary String?
|
||||
inputTokens Int?
|
||||
outputTokens Int?
|
||||
metadata Json
|
||||
error String?
|
||||
startedAt DateTime @default(now())
|
||||
finishedAt DateTime?
|
||||
updatedAt DateTime @updatedAt
|
||||
|
||||
project Project @relation(fields: [projectId], references: [id], onDelete: Cascade)
|
||||
session AgentSession? @relation(fields: [sessionId], references: [id], onDelete: SetNull)
|
||||
requestedBy User? @relation("runRequester", fields: [requestedByUserId], references: [id], onDelete: SetNull)
|
||||
projectLock ProjectAgentLock?
|
||||
|
||||
@@index([projectId, status])
|
||||
@@index([sessionId])
|
||||
@@index([requestedByUserId])
|
||||
@@index([updatedAt])
|
||||
}
|
||||
|
||||
/// ADR-0002: lock owner = run_id (not session/user/chat). `projectId @id` ⇒
|
||||
/// at most one lock per project (LockTable exclusivity). `runId @unique` ⇒
|
||||
/// a run holds at most one lock. WellFormed (holder is non-terminal) is an
|
||||
/// app-level invariant checked on read/write, not a DB constraint.
|
||||
model ProjectAgentLock {
|
||||
projectId String @id
|
||||
runId String @unique
|
||||
holderUserId String?
|
||||
acquiredAt DateTime @default(now())
|
||||
expiresAt DateTime?
|
||||
|
||||
project Project @relation(fields: [projectId], references: [id], onDelete: Cascade)
|
||||
run AgentRun @relation(fields: [runId], references: [id], onDelete: Cascade)
|
||||
holder User? @relation("lockHolder", fields: [holderUserId], references: [id], onDelete: SetNull)
|
||||
|
||||
@@index([expiresAt])
|
||||
}
|
||||
|
||||
// --- Permission grants & settings (ADR-0004) ----------------------------
|
||||
|
||||
/// ADR-0004 PermissionRole: read ⊂ edit ⊂ manage (capability lattice).
|
||||
/// Distinct from PlatformRole. Force-release is admin-only, outside this
|
||||
/// lattice (spec RequiresAdmin).
|
||||
enum PermissionRole {
|
||||
READ
|
||||
EDIT
|
||||
MANAGE
|
||||
}
|
||||
|
||||
/// ADR-0004 resource_type: project | artifact | project_group. The resource
|
||||
/// id's meaning is determined by its type (artifact id semantics align to the
|
||||
/// Courseware half; OPEN here).
|
||||
enum PermissionResourceType {
|
||||
PROJECT
|
||||
ARTIFACT
|
||||
PROJECT_GROUP
|
||||
}
|
||||
|
||||
/// ADR-0004 PermissionGrant: resource × principal × role.
|
||||
/// `principal` is an opaque string (principal sub-typology OPEN, ADR-0004).
|
||||
/// The compound unique covers "one active grant per (resource, principal, role)"
|
||||
/// — revoked rows keep `revokedAt` set, so a re-grant after revocation is a new
|
||||
/// row, not a conflict.
|
||||
model PermissionGrant {
|
||||
id String @id @default(cuid())
|
||||
resourceType PermissionResourceType
|
||||
resourceId String
|
||||
principal String
|
||||
role PermissionRole
|
||||
createdByUserId String?
|
||||
createdAt DateTime @default(now())
|
||||
revokedAt DateTime?
|
||||
|
||||
project Project? @relation("projectGrants", fields: [resourceId], references: [id], onDelete: Cascade)
|
||||
createdBy User? @relation("grantCreator", fields: [createdByUserId], references: [id], onDelete: SetNull)
|
||||
|
||||
@@unique([resourceType, resourceId, principal, role, revokedAt])
|
||||
@@index([resourceType, resourceId, revokedAt])
|
||||
@@index([principal, revokedAt])
|
||||
}
|
||||
|
||||
/// ADR-0004 PermissionSettings: six policy knobs, values OPEN. Stored as one
|
||||
/// opaque string column each; the enum/value-domain is decided by admin policy,
|
||||
/// not by this schema. `resourceType`+`resourceId` identify the resource.
|
||||
/// Related to Project only when resourceType=PROJECT (null otherwise).
|
||||
model PermissionSettings {
|
||||
id String @id @default(cuid())
|
||||
resourceType PermissionResourceType
|
||||
resourceId String
|
||||
externalShare String
|
||||
comment String
|
||||
copyDownload String
|
||||
collaboratorMgmt String
|
||||
agentTrigger String
|
||||
agentCancel String
|
||||
createdAt DateTime @default(now())
|
||||
updatedAt DateTime @updatedAt
|
||||
|
||||
project Project? @relation("projectSettings", fields: [resourceId], references: [id], onDelete: Cascade)
|
||||
|
||||
@@unique([resourceType, resourceId])
|
||||
@@index([resourceType, resourceId])
|
||||
}
|
||||
|
||||
|
||||
/// Per-role agent trigger grant. Orthogonal to ADR-0004's PermissionGrant:
|
||||
/// ADR-0004 decides "can trigger an agent at all" (triggerAgent capability,
|
||||
/// edit+ role); this table decides "can trigger *which* agent role" (e.g.
|
||||
/// /review vs /draft). Two gates in series — both must pass.
|
||||
///
|
||||
/// `roleId` is an opaque string matching RoleEntry.id (ADR-0017: roles are
|
||||
/// data, not a code enum). `principal` mirrors ADR-0004's opaque principal
|
||||
/// (sub-typology OPEN). A project-scoped row grants the role on that project;
|
||||
/// the compound unique covers "one active grant per (project, principal, role)".
|
||||
/// Revocation via `revokedAt`, same pattern as PermissionGrant.
|
||||
model RoleTriggerGrant {
|
||||
id String @id @default(cuid())
|
||||
projectId String
|
||||
roleId String
|
||||
principal String
|
||||
createdByUserId String?
|
||||
createdAt DateTime @default(now())
|
||||
revokedAt DateTime?
|
||||
|
||||
project Project @relation("projectRoleGrants", fields: [projectId], references: [id], onDelete: Cascade)
|
||||
createdBy User? @relation("roleGrantCreator", fields: [createdByUserId], references: [id], onDelete: SetNull)
|
||||
|
||||
@@unique([projectId, roleId, principal, revokedAt])
|
||||
@@index([projectId, roleId, revokedAt])
|
||||
@@index([principal, revokedAt])
|
||||
}
|
||||
|
||||
// --- Audit (ADR Audit, content OPEN) -------------------------------------
|
||||
|
||||
/// spec AuditEntry: minimal skeleton — one entry relates to a run. Event type,
|
||||
/// actor, timestamp, details are OPEN. This table mirrors that: `runId` is the
|
||||
model AuditEntry {
|
||||
id String @id @default(cuid())
|
||||
runId String?
|
||||
projectId String?
|
||||
actorUserId String?
|
||||
action String
|
||||
metadata Json
|
||||
createdAt DateTime @default(now())
|
||||
|
||||
actor User? @relation("auditActor", fields: [actorUserId], references: [id], onDelete: SetNull)
|
||||
project Project? @relation("projectAudit", fields: [projectId], references: [id], onDelete: SetNull)
|
||||
|
||||
@@index([runId])
|
||||
@@index([projectId, createdAt])
|
||||
@@index([actorUserId])
|
||||
@@index([createdAt])
|
||||
}
|
||||
|
||||
// --- Feishu event dedup --------------------------------------------------
|
||||
|
||||
/// Idempotency receipt for inbound Feishu ws events. The lark ws client may
|
||||
/// redeliver an event (at-least-once); without dedup a duplicate would spawn a
|
||||
/// second AgentRun — the lock would refuse it, but a FAILED run row + a busy
|
||||
/// reply would still leak. `eventId @unique` makes the second insert a no-op
|
||||
/// signal: the handler checks existence before processing.
|
||||
model FeishuEventReceipt {
|
||||
id String @id @default(cuid())
|
||||
eventId String @unique
|
||||
eventType String
|
||||
messageId String?
|
||||
receivedAt DateTime @default(now())
|
||||
|
||||
@@index([eventType])
|
||||
@@index([messageId])
|
||||
@@index([receivedAt])
|
||||
}
|
||||
@@ -1,105 +0,0 @@
|
||||
/**
|
||||
* `cph` subprocess tools - the Hub<->Courseware coupling point.
|
||||
*
|
||||
* The Hub agent does not parse engineering-file models in-process; it calls the
|
||||
* stable `cph` CLI (ADR-0016 version contract). `cph check` validates a
|
||||
* project; `cph build` renders a target artifact. Version compatibility is the
|
||||
* CLI's responsibility - it refuses incompatible `.cph-version` files with a
|
||||
* `cphVersionMismatch` error diagnostic (ADR-0016); the Hub merely runs the
|
||||
* subprocess and returns its stdout/stderr/exit to the model.
|
||||
*
|
||||
* The `cph` binary path is configurable (env `CPH_BIN`, default `cph` on
|
||||
* PATH). All subprocesses run with `cwd = ctx.workspaceDir` so paths in
|
||||
* diagnostics are relative to the project root.
|
||||
*/
|
||||
import { execFile } from "node:child_process";
|
||||
import { promisify } from "node:util";
|
||||
import { tool } from "ai";
|
||||
import { z } from "zod";
|
||||
import type { ToolContext, ToolDefinition } from "./tools.js";
|
||||
|
||||
const execFileAsync = promisify(execFile);
|
||||
|
||||
const CPH_BIN = process.env["CPH_BIN"] ?? "cph";
|
||||
const DEFAULT_TIMEOUT_MS = 120_000;
|
||||
|
||||
interface ExecResult {
|
||||
readonly exitCode: number;
|
||||
readonly stdout: string;
|
||||
readonly stderr: string;
|
||||
}
|
||||
|
||||
async function runCph(args: readonly string[], workspaceDir: string): Promise<ExecResult> {
|
||||
try {
|
||||
const { stdout, stderr } = await execFileAsync(CPH_BIN, args, {
|
||||
cwd: workspaceDir,
|
||||
timeout: DEFAULT_TIMEOUT_MS,
|
||||
maxBuffer: 10 * 1024 * 1024,
|
||||
});
|
||||
return { exitCode: 0, stdout, stderr };
|
||||
} catch (e) {
|
||||
// execFile rejects on non-zero exit; the error carries stdout/stderr/code.
|
||||
const err = e as NodeJS.ErrnoException & { stdout?: string; stderr?: string; code?: number | string };
|
||||
if (err.code === "ENOENT") {
|
||||
return {
|
||||
exitCode: 127,
|
||||
stdout: "",
|
||||
stderr: `cph binary not found at "${CPH_BIN}" (set CPH_BIN env or install cph on PATH)`,
|
||||
};
|
||||
}
|
||||
return {
|
||||
exitCode: typeof err.code === "number" ? err.code : 1,
|
||||
stdout: err.stdout ?? "",
|
||||
stderr: err.stderr ?? "",
|
||||
};
|
||||
}
|
||||
}
|
||||
|
||||
/// `cph check <dir>` - validate a curriculum engineering file. Returns the
|
||||
/// checker's diagnostics (stdout) for the model to act on. Non-zero exit means
|
||||
/// the file has error diagnostics (ADR-0010); the output is still returned,
|
||||
/// not thrown - the model needs to see the diagnostics to fix them.
|
||||
export function cphCheckTool(ctx: ToolContext): ToolDefinition {
|
||||
return tool({
|
||||
description:
|
||||
"Run `cph check` on the project's curriculum engineering file. Returns diagnostics (7 classes: structure/schema/compile/version...). Non-zero exit means error diagnostics present - read the output to fix them.",
|
||||
inputSchema: z.object({
|
||||
path: z.string().describe("Path to the engineering file dir; defaults to the workspace root.").optional(),
|
||||
}),
|
||||
execute: async (args): Promise<string> => {
|
||||
const target = args.path ?? ".";
|
||||
const res = await runCph(["check", target], ctx.workspaceDir);
|
||||
return JSON.stringify({
|
||||
exitCode: res.exitCode,
|
||||
stdout: res.stdout,
|
||||
stderr: res.stderr,
|
||||
});
|
||||
},
|
||||
});
|
||||
}
|
||||
|
||||
/// `cph build <dir> --target <T> -o <out>` - render a target artifact. The
|
||||
/// target (student/teacher/...) determines the build (ADR-0009). Output path
|
||||
/// is relative to the workspace unless absolute.
|
||||
export function cphBuildTool(ctx: ToolContext): ToolDefinition {
|
||||
return tool({
|
||||
description:
|
||||
"Run `cph build` to render a curriculum artifact (e.g. student/teacher PDF). Target selects the build; output names the result file.",
|
||||
inputSchema: z.object({
|
||||
target: z.string().describe("Build target, e.g. 'student', 'teacher'."),
|
||||
path: z.string().describe("Path to the engineering file dir; defaults to the workspace root.").optional(),
|
||||
output: z.string().describe("Output file path (relative to workspace or absolute).").optional(),
|
||||
}),
|
||||
execute: async (args): Promise<string> => {
|
||||
const target = args.path ?? ".";
|
||||
const out = args.output ?? `build/${args.target}.pdf`;
|
||||
const res = await runCph(["build", target, "--target", args.target, "-o", out], ctx.workspaceDir);
|
||||
return JSON.stringify({
|
||||
exitCode: res.exitCode,
|
||||
stdout: res.stdout,
|
||||
stderr: res.stderr,
|
||||
output: out,
|
||||
});
|
||||
},
|
||||
});
|
||||
}
|
||||
@@ -1,105 +0,0 @@
|
||||
/**
|
||||
* Per-run model selection & role-based routing.
|
||||
*
|
||||
* ADR-0017 consequence: role-based model routing (different run kinds default
|
||||
* to different models) is a **product/admin configuration** concern, not a spec
|
||||
* invariant. This registry is the seam for that config; the concrete policy
|
||||
* (which models are admin-enabled, which role maps to which default) is `OPEN`
|
||||
* here — decided by admin settings + ADR, not hard-coded.
|
||||
*/
|
||||
|
||||
/**
|
||||
* A named role preset — the full per-run agent bundle. Roles are **data**, not
|
||||
* a code enum: admin/teachers define them (ADR-0017: role-based routing is
|
||||
* product config, not a spec invariant). `roleId` is an opaque string and
|
||||
* doubles as the slash-command name (`/draft ...`) — the registry holds the
|
||||
* role set, so new roles are added by configuration, not by editing code.
|
||||
*
|
||||
* A role bundles everything that distinguishes one agent persona from another:
|
||||
* model, system prompt, and the tool surface (files / cph / feishu / skills /
|
||||
* mcps). Per-run tool whitelisting is enforced by {@link ToolRegistry.subset};
|
||||
* the model never sees tools outside its role's whitelist, even if it tries to
|
||||
* call them — security does not rely on the system prompt.
|
||||
*/
|
||||
export interface RoleEntry {
|
||||
readonly id: string;
|
||||
/** Human label for the teacher-side switcher UX. */
|
||||
readonly label: string;
|
||||
/** Default model id for runs under this role, if a routing rule is set. */
|
||||
readonly defaultModel: string | undefined;
|
||||
/**
|
||||
* System prompt seeding the agent's persona/instructions. Prepended to the
|
||||
* run's messages only at session start (resume reads it from the transcript,
|
||||
* see runner.ts). `undefined` ⇒ no system prompt (bare run).
|
||||
*/
|
||||
readonly systemPrompt: string | undefined;
|
||||
/**
|
||||
* Tool names this role may use (whitelist). `undefined` ⇒ the full registered
|
||||
* set (back-compat / unrestricted roles). An empty array ⇒ no tools at all.
|
||||
* Names not present in the registry are silently dropped at run setup.
|
||||
*/
|
||||
readonly tools: readonly string[] | undefined;
|
||||
}
|
||||
|
||||
/** A model the admin has enabled for use by the Hub. */
|
||||
export interface ModelEntry {
|
||||
readonly id: string;
|
||||
/** Human label for the teacher-side switcher UX. */
|
||||
readonly label: string;
|
||||
/** True when the model is known to support tool use reliably. */
|
||||
readonly toolCapable: boolean;
|
||||
}
|
||||
|
||||
export interface ModelRegistry {
|
||||
/** All models admin-enabled for this Hub instance. */
|
||||
listModels(): readonly ModelEntry[];
|
||||
/** All role presets currently configured (admin/teacher-defined). */
|
||||
listRoles(): readonly RoleEntry[];
|
||||
/** The role preset with the given id, if any. */
|
||||
role(id: string): RoleEntry | undefined;
|
||||
/** Resolve a model id: explicit request → role default → first enabled. */
|
||||
resolve(requestedModel: string | undefined, roleId: string): string;
|
||||
}
|
||||
|
||||
/**
|
||||
* A simple in-memory registry. Real wiring reads from admin settings / DB; this
|
||||
* is the skeleton seam. Both the model list and the role set are pluggable data
|
||||
* — adding a role is a config change, not a code change.
|
||||
*/
|
||||
export class InMemoryModelRegistry implements ModelRegistry {
|
||||
private readonly models: readonly ModelEntry[];
|
||||
private readonly roles: Map<string, RoleEntry>;
|
||||
|
||||
constructor(models: readonly ModelEntry[], roles: readonly RoleEntry[] = []) {
|
||||
this.models = models;
|
||||
this.roles = new Map(roles.map((r) => [r.id, r]));
|
||||
}
|
||||
|
||||
listModels(): readonly ModelEntry[] {
|
||||
return this.models;
|
||||
}
|
||||
|
||||
listRoles(): readonly RoleEntry[] {
|
||||
return [...this.roles.values()];
|
||||
}
|
||||
|
||||
role(id: string): RoleEntry | undefined {
|
||||
return this.roles.get(id);
|
||||
}
|
||||
|
||||
/**
|
||||
* Resolve a model id for a run. Priority: teacher's explicit request → the
|
||||
* role preset's default → the first admin-enabled model. `roleId` is a string
|
||||
* so unknown roles degrade gracefully to the fallback rather than throwing.
|
||||
*/
|
||||
resolve(requestedModel: string | undefined, roleId: string): string {
|
||||
if (requestedModel !== undefined && this.models.some((m) => m.id === requestedModel)) {
|
||||
return requestedModel;
|
||||
}
|
||||
const role = this.roles.get(roleId);
|
||||
if (role?.defaultModel !== undefined) return role.defaultModel;
|
||||
const first = this.models[0];
|
||||
if (first === undefined) throw new Error("no models enabled for this Hub");
|
||||
return first.id;
|
||||
}
|
||||
}
|
||||
@@ -1,18 +0,0 @@
|
||||
/**
|
||||
* OpenRouter model factory.
|
||||
*
|
||||
* ADR-0017: the agent layer keeps role/model resolution separate from provider
|
||||
* construction. A run carries a resolved model id, and switching model still
|
||||
* means a new provider-bound session.
|
||||
*/
|
||||
import { createOpenAICompatible } from "@ai-sdk/openai-compatible";
|
||||
import type { LanguageModel } from "ai";
|
||||
|
||||
export function createModelFactory(): (modelId: string) => LanguageModel {
|
||||
const provider = createOpenAICompatible({
|
||||
name: "openrouter",
|
||||
baseURL: process.env.OPENROUTER_BASE_URL ?? "https://openrouter.ai/api/v1",
|
||||
headers: { Authorization: `Bearer ${process.env.OPENROUTER_API_KEY ?? ""}` },
|
||||
});
|
||||
return (modelId: string) => provider(modelId);
|
||||
}
|
||||
@@ -1,140 +0,0 @@
|
||||
/**
|
||||
* Provider-bound agent runner.
|
||||
*
|
||||
* The AI SDK owns tool-call dispatch and message folding. The Hub owns the
|
||||
* per-run tool context, role/model selection, transcript persistence, and the
|
||||
* ADR-0017 session boundary: a run is bound to one model. Switching model is a
|
||||
* new run + new session; cross-run continuity is carried by project
|
||||
* memory/anchors (ADR-0003), not by this runner.
|
||||
*/
|
||||
import { generateText, stepCountIs, type LanguageModel, type ModelMessage } from "ai";
|
||||
import type { ToolContext, ToolRegistry } from "./tools.js";
|
||||
import { readTranscript, appendTranscript } from "./transcript.js";
|
||||
|
||||
export type ModelFactory = (modelId: string) => LanguageModel;
|
||||
|
||||
/** What the runner needs about the project to seed and bound a run. */
|
||||
export interface ProjectContext {
|
||||
readonly projectId: string;
|
||||
/** ADR-0001 binding - the chat this project is bound to. */
|
||||
readonly boundChatId: string;
|
||||
/** Absolute path to the curriculum engineering-file workspace. */
|
||||
readonly workspaceDir: string;
|
||||
}
|
||||
|
||||
export interface RunRequest {
|
||||
readonly prompt: string;
|
||||
/** Resolved model id (already chosen by the caller per ADR-0017). */
|
||||
readonly model: string;
|
||||
readonly project: ProjectContext;
|
||||
readonly systemPrompt: string | undefined;
|
||||
/** Iteration cap before the run is returned as `length`. Default 25. */
|
||||
readonly maxIterations?: number;
|
||||
/** Per-role tool whitelist (ADR-0017). Undefined means all registered tools. */
|
||||
readonly toolWhitelist?: readonly string[] | undefined;
|
||||
/** Path to the session transcript JSONL. If set, prior messages are loaded
|
||||
* from it before the run, and new messages are appended after. */
|
||||
readonly transcriptPath?: string;
|
||||
}
|
||||
|
||||
export type RunStatus = "completed" | "length" | "failed";
|
||||
|
||||
export interface RunResult {
|
||||
readonly status: RunStatus;
|
||||
/** Full transcript of the run, for audit (ADR Audit, content OPEN). */
|
||||
readonly messages: readonly ModelMessage[];
|
||||
readonly usage: { inputTokens: number; outputTokens: number };
|
||||
readonly error?: string;
|
||||
}
|
||||
|
||||
const DEFAULT_MAX_ITERATIONS = 25;
|
||||
|
||||
export async function runAgent(
|
||||
modelFactory: ModelFactory,
|
||||
tools: ToolRegistry,
|
||||
req: RunRequest,
|
||||
): Promise<RunResult> {
|
||||
const ctx: ToolContext = {
|
||||
runId: cryptoRandomId(),
|
||||
projectId: req.project.projectId,
|
||||
boundChatId: req.project.boundChatId,
|
||||
workspaceDir: req.project.workspaceDir,
|
||||
};
|
||||
const aiTools = tools.build(ctx, req.toolWhitelist);
|
||||
|
||||
// Load prior session messages from transcript (continuity across @bot calls
|
||||
// in the same session). ADR-0003: session messages != group chat history.
|
||||
let messages: ModelMessage[] = req.transcriptPath !== undefined ? await readTranscript(req.transcriptPath) : [];
|
||||
const loadedCount = messages.length;
|
||||
if (req.systemPrompt !== undefined && messages.length === 0) {
|
||||
// System prompt only at the very start of a session; on resume it's
|
||||
// already in the transcript.
|
||||
messages = [{ role: "system", content: req.systemPrompt }];
|
||||
}
|
||||
messages = [...messages, { role: "user", content: req.prompt }];
|
||||
|
||||
const cap = req.maxIterations ?? DEFAULT_MAX_ITERATIONS;
|
||||
|
||||
try {
|
||||
const result = await generateText({
|
||||
model: modelFactory(req.model),
|
||||
messages,
|
||||
allowSystemInMessages: true,
|
||||
tools: aiTools,
|
||||
stopWhen: stepCountIs(cap),
|
||||
});
|
||||
const allMessages: ModelMessage[] = [...messages, ...result.responseMessages];
|
||||
await appendTranscriptIfSet(req, allMessages, loadedCount);
|
||||
|
||||
const stoppedByStepCap = result.finishReason === "tool-calls" && result.steps.length >= cap;
|
||||
const status: RunStatus =
|
||||
result.finishReason === "stop"
|
||||
? "completed"
|
||||
: result.finishReason === "length" || stoppedByStepCap
|
||||
? "length"
|
||||
: "failed";
|
||||
const error =
|
||||
status === "failed"
|
||||
? `finishReason=${result.finishReason}`
|
||||
: stoppedByStepCap
|
||||
? `exceeded maxIterations=${cap}`
|
||||
: undefined;
|
||||
|
||||
return {
|
||||
status,
|
||||
messages: allMessages,
|
||||
usage: {
|
||||
inputTokens: result.usage.inputTokens ?? 0,
|
||||
outputTokens: result.usage.outputTokens ?? 0,
|
||||
},
|
||||
...(error !== undefined ? { error } : {}),
|
||||
};
|
||||
} catch (e) {
|
||||
await appendTranscriptIfSet(req, messages, loadedCount);
|
||||
return {
|
||||
status: "failed",
|
||||
messages,
|
||||
usage: { inputTokens: 0, outputTokens: 0 },
|
||||
error: e instanceof Error ? e.message : String(e),
|
||||
};
|
||||
}
|
||||
}
|
||||
|
||||
/// Append only the messages produced this run (skip the `loadedCount` prior
|
||||
/// ones already in the file). Errors are swallowed - a transcript write
|
||||
/// failure must not lose the run result.
|
||||
async function appendTranscriptIfSet(req: RunRequest, messages: readonly ModelMessage[], loadedCount: number): Promise<void> {
|
||||
if (req.transcriptPath === undefined) return;
|
||||
const newMessages = messages.slice(loadedCount);
|
||||
if (newMessages.length === 0) return;
|
||||
try {
|
||||
await appendTranscript(req.transcriptPath, newMessages);
|
||||
} catch {
|
||||
// Swallow - transcript is best-effort persistence; the run result is
|
||||
// returned regardless. ADR-0002 lock ensures no concurrent writer.
|
||||
}
|
||||
}
|
||||
|
||||
function cryptoRandomId(): string {
|
||||
return globalThis.crypto.randomUUID();
|
||||
}
|
||||
@@ -1,114 +0,0 @@
|
||||
/**
|
||||
* Tool registry - the agent's narrow, project-scoped tool surface.
|
||||
*
|
||||
* Unlike a general "Claude Code", the Hub agent operates on a curriculum
|
||||
* engineering-file tree (ADR-0007) and reads Feishu context on demand
|
||||
* (ADR-0003). Its tools are therefore bounded:
|
||||
*
|
||||
* - file-tree read/write against the project workspace dir,
|
||||
* - `cph check` / `cph build` subprocess calls (the Courseware-side checker,
|
||||
* coupled only via the stable CLI contract ADR-0016),
|
||||
* - Feishu context reads, which must honor ADR-0003's authorization invariant.
|
||||
*
|
||||
* The AI SDK owns tool-call dispatch; this registry owns Hub-specific tool
|
||||
* construction and per-role whitelisting (ADR-0017).
|
||||
*/
|
||||
import { tool, type Tool } from "ai";
|
||||
import { z } from "zod";
|
||||
|
||||
/** Per-run execution context closed over by every tool execute function. */
|
||||
export interface ToolContext {
|
||||
readonly runId: string;
|
||||
readonly projectId: string;
|
||||
/** ADR-0001: the chat this project is bound to. Feishu reads must stay in it. */
|
||||
readonly boundChatId: string;
|
||||
/** Absolute path to the project's curriculum engineering-file workspace. */
|
||||
readonly workspaceDir: string;
|
||||
}
|
||||
|
||||
export type ToolDefinition = Tool;
|
||||
export type ToolFactory = (ctx: ToolContext) => ToolDefinition;
|
||||
|
||||
export class ToolRegistry {
|
||||
private readonly factories = new Map<string, ToolFactory>();
|
||||
|
||||
register(name: string, factory: ToolFactory): void {
|
||||
if (this.factories.has(name)) {
|
||||
throw new Error(`duplicate tool: ${name}`);
|
||||
}
|
||||
this.factories.set(name, factory);
|
||||
}
|
||||
|
||||
/**
|
||||
* Build the AI SDK `tools` record. If `names` is given, include only those
|
||||
* tools (per-role whitelist, ADR-0017). Names not registered are silently
|
||||
* dropped because role config may name tools a Hub instance does not provide.
|
||||
*/
|
||||
build(ctx: ToolContext, names: readonly string[] | undefined): Record<string, ToolDefinition> {
|
||||
const built: Record<string, ToolDefinition> = {};
|
||||
const selected = names ?? [...this.factories.keys()];
|
||||
for (const name of selected) {
|
||||
const factory = this.factories.get(name);
|
||||
if (factory !== undefined) {
|
||||
built[name] = factory(ctx);
|
||||
}
|
||||
}
|
||||
return built;
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Thrown when a Feishu context read targets a chat other than the run's project's
|
||||
* bound chat. This is the runtime enforcement of ADR-0003's
|
||||
* `McpReadRequest.Authorized`: "Claude cannot pass arbitrary chat ids".
|
||||
*/
|
||||
export class UnauthorizedChatRead extends Error {
|
||||
constructor(
|
||||
readonly requestedChatId: string,
|
||||
readonly boundChatId: string,
|
||||
) {
|
||||
super(
|
||||
`refused Feishu context read: requested chat ${requestedChatId} is not the run's project's bound chat ${boundChatId} (ADR-0003)`,
|
||||
);
|
||||
this.name = "UnauthorizedChatRead";
|
||||
}
|
||||
}
|
||||
|
||||
/** Schema for the Feishu context read tool's arguments. */
|
||||
export interface FeishuContextArgs {
|
||||
readonly chat_id: string;
|
||||
readonly anchor: "trigger_message" | "status_card" | "reply" | "thread";
|
||||
readonly id: string;
|
||||
}
|
||||
|
||||
/**
|
||||
* Build the Feishu context-read tool factory. The execute closure enforces
|
||||
* ADR-0003's invariant before any API call: the requested `chat_id` must equal
|
||||
* `ctx.boundChatId`.
|
||||
*
|
||||
* The actual Feishu API call (read message / reply chain / thread / recent
|
||||
* group messages) is injected as `read`, so the invariant check is separable
|
||||
* from the transport. In tests `read` can be a stub; in production it wraps
|
||||
* `@larksuiteoapi/node-sdk`.
|
||||
*/
|
||||
export function feishuContextTool(
|
||||
read: (args: FeishuContextArgs, ctx: ToolContext, rt: unknown) => Promise<string>,
|
||||
rt: unknown,
|
||||
): ToolFactory {
|
||||
return (ctx) =>
|
||||
tool({
|
||||
description:
|
||||
"Read on-demand Feishu context (a trigger message, status card, reply, or thread) for the current project's bound chat. The chat id must match the project binding.",
|
||||
inputSchema: z.object({
|
||||
chat_id: z.string().describe("The Feishu chat id to read from."),
|
||||
anchor: z.enum(["trigger_message", "status_card", "reply", "thread"]).describe("Which kind of anchor to read."),
|
||||
id: z.string().describe("The anchor id (message id or run id)."),
|
||||
}),
|
||||
execute: async (args): Promise<string> => {
|
||||
if (args.chat_id !== ctx.boundChatId) {
|
||||
throw new UnauthorizedChatRead(args.chat_id, ctx.boundChatId);
|
||||
}
|
||||
return read(args, ctx, rt);
|
||||
},
|
||||
});
|
||||
}
|
||||
@@ -1,64 +0,0 @@
|
||||
/**
|
||||
* Session transcript — append-only JSONL file in the workspace.
|
||||
*
|
||||
* Each line is one AI SDK {@link ModelMessage}, JSON-encoded. The transcript lives at
|
||||
* `workspaceDir/.cph/sessions/<sessionId>.jsonl`, following the same "workspace
|
||||
* is a directory tree" principle as the engineering file itself (ADR-0007).
|
||||
*
|
||||
* This mirrors how Claude Code stores its transcript (a `.jsonl` file per
|
||||
* session). The agent can read its own history via `read_file` — no special
|
||||
* "load history" code path. ADR-0002's lock guarantees one run per project at a
|
||||
* time, so the transcript is never concurrently written.
|
||||
*
|
||||
* ADR-0003: this stores **agent session messages** (prompt + response + tool
|
||||
* calls produced by the Hub), NOT Feishu group chat history. The two are
|
||||
* distinct; storing session messages does not conflict with "the Hub avoids
|
||||
* becoming a full chat history store."
|
||||
*/
|
||||
import { readFile, mkdir, appendFile } from "node:fs/promises";
|
||||
import { join, dirname } from "node:path";
|
||||
import type { ModelMessage } from "ai";
|
||||
|
||||
/// Subdirectory within a workspace where session transcripts live.
|
||||
export const TRANSCRIPT_DIR = ".cph/sessions";
|
||||
|
||||
/** Path for a session's transcript file within a workspace. */
|
||||
export function transcriptPath(workspaceDir: string, sessionId: string): string {
|
||||
return join(workspaceDir, TRANSCRIPT_DIR, `${sessionId}.jsonl`);
|
||||
}
|
||||
|
||||
/**
|
||||
* Read prior messages from a transcript file. Returns an empty array if the
|
||||
* file doesn't exist yet (first run in this session). Corrupt lines are
|
||||
* skipped — a partially-written last line (crash mid-append) won't break the
|
||||
* next run.
|
||||
*/
|
||||
export async function readTranscript(path: string): Promise<ModelMessage[]> {
|
||||
let content: string;
|
||||
try {
|
||||
content = await readFile(path, "utf8");
|
||||
} catch {
|
||||
return [];
|
||||
}
|
||||
const messages: ModelMessage[] = [];
|
||||
for (const line of content.split("\n")) {
|
||||
const trimmed = line.trim();
|
||||
if (trimmed === "") continue;
|
||||
try {
|
||||
messages.push(JSON.parse(trimmed) as ModelMessage);
|
||||
} catch {
|
||||
// Skip corrupt line — likely a partial write from a crash.
|
||||
}
|
||||
}
|
||||
return messages;
|
||||
}
|
||||
|
||||
/**
|
||||
* Append messages to a transcript file. Creates the parent directory if needed.
|
||||
* Each message is written as one JSON line.
|
||||
*/
|
||||
export async function appendTranscript(path: string, messages: readonly ModelMessage[]): Promise<void> {
|
||||
await mkdir(dirname(path), { recursive: true });
|
||||
const lines = messages.map((m) => JSON.stringify(m)).join("\n") + "\n";
|
||||
await appendFile(path, lines, "utf8");
|
||||
}
|
||||
@@ -1,106 +0,0 @@
|
||||
/**
|
||||
* Workspace file tools - bounded read/write/list against the project's
|
||||
* curriculum engineering-file tree (ADR-0007 directory tree).
|
||||
*
|
||||
* All paths are **confined to `ctx.workspaceDir`**: the handler resolves the
|
||||
* requested relative path against the workspace root and rejects any path that
|
||||
* escapes it (via `..` or absolute paths). This is the agent's only file
|
||||
* surface; the Hub agent is narrower than a general coding agent.
|
||||
*/
|
||||
import { readFile, writeFile, readdir, mkdir } from "node:fs/promises";
|
||||
import { join, resolve, relative, isAbsolute } from "node:path";
|
||||
import { tool } from "ai";
|
||||
import { z } from "zod";
|
||||
import type { ToolContext, ToolDefinition } from "./tools.js";
|
||||
|
||||
/** Thrown when a requested path escapes the project workspace root. */
|
||||
export class PathEscape extends Error {
|
||||
constructor(readonly requested: string, readonly workspaceDir: string) {
|
||||
super(`path escapes workspace: ${requested} (root ${workspaceDir})`);
|
||||
this.name = "PathEscape";
|
||||
}
|
||||
}
|
||||
|
||||
/** Resolve a tool-supplied path against the workspace root, rejecting escapes. */
|
||||
function confine(requestedPath: string, workspaceDir: string): string {
|
||||
if (isAbsolute(requestedPath)) {
|
||||
// Allow absolute paths only if they're already inside the workspace.
|
||||
const rel = relative(workspaceDir, requestedPath);
|
||||
if (rel.startsWith("..") || rel === "") {
|
||||
throw new PathEscape(requestedPath, workspaceDir);
|
||||
}
|
||||
return requestedPath;
|
||||
}
|
||||
const resolved = resolve(workspaceDir, requestedPath);
|
||||
const rel = relative(workspaceDir, resolved);
|
||||
if (rel.startsWith("..")) {
|
||||
throw new PathEscape(requestedPath, workspaceDir);
|
||||
}
|
||||
return resolved;
|
||||
}
|
||||
|
||||
export function readFileTool(ctx: ToolContext): ToolDefinition {
|
||||
return tool({
|
||||
description: "Read a file from the project's curriculum engineering-file workspace. Path is relative to the workspace root.",
|
||||
inputSchema: z.object({
|
||||
path: z.string().describe("Relative path within the workspace."),
|
||||
}),
|
||||
execute: async (args): Promise<string> => {
|
||||
try {
|
||||
const full = confine(args.path, ctx.workspaceDir);
|
||||
return await readFile(full, "utf8");
|
||||
} catch (e) {
|
||||
return JSON.stringify({ error: e instanceof Error ? e.message : String(e) });
|
||||
}
|
||||
},
|
||||
});
|
||||
}
|
||||
|
||||
export function writeFileTool(ctx: ToolContext): ToolDefinition {
|
||||
return tool({
|
||||
description:
|
||||
"Write a file in the project's curriculum engineering-file workspace. Path is relative to the workspace root. Creates parent directories.",
|
||||
inputSchema: z.object({
|
||||
path: z.string().describe("Relative path within the workspace."),
|
||||
content: z.string().describe("The full file content to write."),
|
||||
}),
|
||||
execute: async (args): Promise<string> => {
|
||||
try {
|
||||
const full = confine(args.path, ctx.workspaceDir);
|
||||
await mkdir(join(full, ".."), { recursive: true });
|
||||
await writeFile(full, args.content, "utf8");
|
||||
return JSON.stringify({ ok: true, path: args.path, bytes: args.content.length });
|
||||
} catch (e) {
|
||||
return JSON.stringify({ error: e instanceof Error ? e.message : String(e) });
|
||||
}
|
||||
},
|
||||
});
|
||||
}
|
||||
|
||||
interface Entry {
|
||||
readonly name: string;
|
||||
readonly kind: "file" | "dir";
|
||||
}
|
||||
|
||||
export function listFilesTool(ctx: ToolContext): ToolDefinition {
|
||||
return tool({
|
||||
description: "List files and directories at a path within the workspace. Defaults to the workspace root.",
|
||||
inputSchema: z.object({
|
||||
path: z.string().describe("Relative path within the workspace; defaults to root.").optional(),
|
||||
}),
|
||||
execute: async (args): Promise<string> => {
|
||||
const sub = args.path ?? ".";
|
||||
try {
|
||||
const full = confine(sub, ctx.workspaceDir);
|
||||
const entries = await readdir(full, { withFileTypes: true });
|
||||
const result: Entry[] = entries.map((e) => ({
|
||||
name: e.name,
|
||||
kind: e.isDirectory() ? "dir" : "file",
|
||||
}));
|
||||
return JSON.stringify(result);
|
||||
} catch (e) {
|
||||
return JSON.stringify({ error: e instanceof Error ? e.message : String(e) });
|
||||
}
|
||||
},
|
||||
});
|
||||
}
|
||||
@@ -1,59 +0,0 @@
|
||||
/**
|
||||
* Audit write path — A-8. The `AuditEntry` table existed but had no writer;
|
||||
* callers (trigger path, permission denials, slash commands) had no way to
|
||||
* record what happened. This module is that single write seam.
|
||||
*
|
||||
* ADR reference: spec Audit. The skeleton pins only the `runId` relation;
|
||||
* event type / actor / timestamp / details are content-OPEN. This helper
|
||||
* exposes `action` (event type) + `actorUserId` (actor) + `metadata`
|
||||
* (details) + `projectId` (locates audit points that don't have a run, e.g.
|
||||
* permission denials) + `runId` (loose string ref, not a Prisma relation —
|
||||
* see schema). `createdAt` is `@default(now())` so we don't pass it.
|
||||
*
|
||||
* Best-effort by design: an audit failure must never break the caller's path
|
||||
* (a trigger failing because the audit log is down would be a spec breach —
|
||||
* audit is observability, not control). Errors are swallowed here. There's no
|
||||
* logger in this layer yet; a future logger can be threaded in without
|
||||
* changing the signature.
|
||||
*/
|
||||
import type { PrismaClient, Prisma } from "@prisma/client";
|
||||
|
||||
export interface AuditInput {
|
||||
readonly runId?: string | undefined;
|
||||
readonly projectId?: string | undefined;
|
||||
readonly actorUserId?: string | undefined;
|
||||
readonly action: string;
|
||||
readonly metadata: Record<string, unknown>;
|
||||
}
|
||||
|
||||
/**
|
||||
* Write one audit entry. Best-effort: any Prisma error is swallowed so the
|
||||
* caller's path (trigger, permission gate, slash command) is unaffected.
|
||||
*
|
||||
* Optional fields are only included when defined — under
|
||||
* `exactOptionalPropertyTypes`, assigning `undefined` to an optional key in a
|
||||
* Prisma `create` payload is a type error (and would also write an explicit
|
||||
* NULL rather than omit the column). Conditional assignment keeps the payload
|
||||
* honest. The data object is typed as `AuditEntryUncheckedCreateInput` (the
|
||||
* direct-FK variant) so it matches one branch of Prisma's `create` input
|
||||
* union exactly — the relation-connect branch has no `projectId`/`runId`
|
||||
* columns and would otherwise reject these fields.
|
||||
*/
|
||||
export async function writeAudit(
|
||||
prisma: PrismaClient,
|
||||
entry: AuditInput,
|
||||
): Promise<void> {
|
||||
const data: Prisma.AuditEntryUncheckedCreateInput = {
|
||||
action: entry.action,
|
||||
metadata: entry.metadata as Prisma.InputJsonValue,
|
||||
};
|
||||
if (entry.runId !== undefined) data.runId = entry.runId;
|
||||
if (entry.projectId !== undefined) data.projectId = entry.projectId;
|
||||
if (entry.actorUserId !== undefined) data.actorUserId = entry.actorUserId;
|
||||
|
||||
try {
|
||||
await prisma.auditEntry.create({ data });
|
||||
} catch {
|
||||
// Swallow: audit is best-effort and must not break the caller's path.
|
||||
}
|
||||
}
|
||||
@@ -1,21 +0,0 @@
|
||||
/**
|
||||
* Prisma client singleton.
|
||||
*
|
||||
* Prisma's client is a connection-pooled datasource; constructing it per-query
|
||||
* exhausts connections. This module exports one shared instance per process.
|
||||
* Hot-reload (tsx watch) can re-import this module — the global guard prevents
|
||||
* a second PrismaClient from being created.
|
||||
*/
|
||||
import { PrismaClient } from "@prisma/client";
|
||||
|
||||
const globalForPrisma = globalThis as unknown as { __hubPrisma?: PrismaClient };
|
||||
|
||||
export const prisma: PrismaClient =
|
||||
globalForPrisma.__hubPrisma ??
|
||||
new PrismaClient({
|
||||
log: process.env["HUB_PRISMA_LOG"] !== undefined ? ["query", "error", "warn"] : ["error", "warn"],
|
||||
});
|
||||
|
||||
if (process.env["NODE_ENV"] !== "production") {
|
||||
globalForPrisma.__hubPrisma = prisma;
|
||||
}
|
||||
@@ -1,177 +0,0 @@
|
||||
/**
|
||||
* Feishu lark client + long-connection event dispatcher.
|
||||
*
|
||||
* Uses lark's WebSocket long-connection mode (no public callback endpoint). The
|
||||
* `EventDispatcher` registers `im.message.receive_v1`; the SDK delivers the raw
|
||||
* event to our handler. This version of the SDK does not auto-normalize on the
|
||||
* ws path — `normalize()` is a separate helper — so we work with the raw event
|
||||
* shape directly (it carries chat_id, message_type, content, mentions).
|
||||
*
|
||||
* ADR-0001: the bot operates inside a project's bound group. It does not own
|
||||
* the lock (ADR-0002) and is not the session owner.
|
||||
*/
|
||||
import * as lark from "@larksuiteoapi/node-sdk";
|
||||
import type { FastifyBaseLogger } from "fastify";
|
||||
|
||||
export interface FeishuConfig {
|
||||
readonly appId: string;
|
||||
readonly appSecret: string;
|
||||
readonly botOpenId: string;
|
||||
}
|
||||
|
||||
export interface FeishuRuntime {
|
||||
readonly client: lark.Client;
|
||||
readonly logger: FastifyBaseLogger;
|
||||
}
|
||||
|
||||
/** Raw `im.message.receive_v1` event payload (subset we use). */
|
||||
export interface MessageReceiveEvent {
|
||||
readonly header?: {
|
||||
readonly event_id?: string;
|
||||
readonly event_type?: string;
|
||||
};
|
||||
readonly message: {
|
||||
readonly message_id: string;
|
||||
readonly chat_id: string;
|
||||
readonly chat_type: string;
|
||||
readonly message_type: string;
|
||||
readonly content: string;
|
||||
readonly mentions?: ReadonlyArray<{
|
||||
readonly key: string;
|
||||
readonly id: { readonly open_id?: string };
|
||||
readonly name: string;
|
||||
}>;
|
||||
};
|
||||
readonly sender: {
|
||||
readonly sender_id: { readonly open_id?: string };
|
||||
readonly sender_type: string;
|
||||
};
|
||||
}
|
||||
|
||||
/** Send a text message to a chat. */
|
||||
export async function sendText(rt: FeishuRuntime, chatId: string, text: string): Promise<void> {
|
||||
// SDK exposes im.v1 dynamically at runtime; the generated types are weak
|
||||
// there, so cast through the known shape.
|
||||
const client = rt.client as unknown as {
|
||||
im: { v1: { message: { create: (p: unknown) => Promise<unknown> } } };
|
||||
};
|
||||
await client.im.v1.message.create({
|
||||
params: { receive_id_type: "chat_id" },
|
||||
data: {
|
||||
receive_id: chatId,
|
||||
msg_type: "text",
|
||||
content: JSON.stringify({ text }),
|
||||
},
|
||||
});
|
||||
}
|
||||
|
||||
/** Send an interactive card to a chat. `card` is the lark card schema object. */
|
||||
export async function sendCard(
|
||||
rt: FeishuRuntime,
|
||||
chatId: string,
|
||||
card: unknown,
|
||||
): Promise<string | null> {
|
||||
const client = rt.client as unknown as {
|
||||
im: { v1: { message: { create: (p: unknown) => Promise<{ data?: { message_id?: string } }> } } };
|
||||
};
|
||||
const res = await client.im.v1.message.create({
|
||||
params: { receive_id_type: "chat_id" },
|
||||
data: {
|
||||
receive_id: chatId,
|
||||
msg_type: "interactive",
|
||||
content: JSON.stringify(card),
|
||||
},
|
||||
});
|
||||
return res.data?.message_id ?? null;
|
||||
}
|
||||
|
||||
/** Build a run-status card: status text + model selector + cancel button. */
|
||||
export function buildRunStatusCard(opts: {
|
||||
readonly status: string;
|
||||
readonly model: string;
|
||||
readonly models: readonly { readonly id: string; readonly label: string }[];
|
||||
readonly runId: string;
|
||||
}): unknown {
|
||||
return {
|
||||
config: { wide_screen_mode: true },
|
||||
header: {
|
||||
title: { tag: "plain_text", content: `@Claude · ${opts.status}` },
|
||||
template: opts.status === "处理完成" ? "green" : opts.status === "处理出错" ? "red" : "blue",
|
||||
},
|
||||
elements: [
|
||||
{ tag: "div", text: { tag: "lark_md", content: `**model:** ${opts.model}` } },
|
||||
{
|
||||
tag: "action",
|
||||
actions: [
|
||||
{
|
||||
tag: "select",
|
||||
placeholder: { tag: "plain_text", content: "切换 model" },
|
||||
options: opts.models.map((m) => ({ text: { tag: "plain_text", content: m.label }, value: m.id })),
|
||||
value: opts.model,
|
||||
},
|
||||
{
|
||||
tag: "button",
|
||||
text: { tag: "plain_text", content: "取消" },
|
||||
type: "danger",
|
||||
value: JSON.stringify({ action: "cancel", runId: opts.runId }),
|
||||
},
|
||||
],
|
||||
},
|
||||
],
|
||||
};
|
||||
}
|
||||
|
||||
/**
|
||||
* Start the lark WebSocket client and route `im.message.receive_v1` events to
|
||||
* `onMessage`. The ws connection lives in the background; this resolves the
|
||||
* runtime handle.
|
||||
*/
|
||||
/** Build a lark Client (HTTP API surface). Used before the ws starts, so tools
|
||||
* that need to call Feishu APIs can hold it from server boot. */
|
||||
export function createLarkClient(config: FeishuConfig): lark.Client {
|
||||
return new lark.Client({
|
||||
appId: config.appId,
|
||||
appSecret: config.appSecret,
|
||||
appType: lark.AppType.SelfBuild,
|
||||
});
|
||||
}
|
||||
|
||||
export interface FeishuListener {
|
||||
readonly runtime: FeishuRuntime;
|
||||
readonly stop: () => Promise<void>;
|
||||
}
|
||||
|
||||
/** Start the ws listener using an already-built client. Returns the runtime. */
|
||||
export function startFeishuListenerWithClient(
|
||||
config: FeishuConfig,
|
||||
client: lark.Client,
|
||||
logger: FastifyBaseLogger,
|
||||
onMessage: (event: MessageReceiveEvent, rt: FeishuRuntime) => Promise<void>,
|
||||
): FeishuRuntime {
|
||||
const wsClient = new lark.WSClient({
|
||||
appId: config.appId,
|
||||
appSecret: config.appSecret,
|
||||
domain: lark.Domain.Feishu,
|
||||
loggerLevel: lark.LoggerLevel.info,
|
||||
});
|
||||
const rt: FeishuRuntime = { client, logger };
|
||||
void wsClient.start({
|
||||
eventDispatcher: new lark.EventDispatcher({}).register({
|
||||
"im.message.receive_v1": async (data) => {
|
||||
try {
|
||||
await onMessage(data as MessageReceiveEvent, rt);
|
||||
} catch (e) {
|
||||
logger.error({ err: e }, "feishu message handler threw");
|
||||
}
|
||||
},
|
||||
}),
|
||||
});
|
||||
return rt;
|
||||
}
|
||||
export function startFeishuListener(
|
||||
config: FeishuConfig,
|
||||
logger: FastifyBaseLogger,
|
||||
onMessage: (event: MessageReceiveEvent, rt: FeishuRuntime) => Promise<void>,
|
||||
): FeishuRuntime {
|
||||
return startFeishuListenerWithClient(config, createLarkClient(config), logger, onMessage);
|
||||
}
|
||||
@@ -1,97 +0,0 @@
|
||||
/**
|
||||
* Feishu context reader — the real implementation behind `feishuContextTool`.
|
||||
*
|
||||
* ADR-0003: Hub stores only anchors, reads Feishu context on demand. The tool
|
||||
* (`feishu_read_context`) is already chat-authorized by `tools.ts` (chat must
|
||||
* match the project binding). Here we actually call lark's `im.v1.message`:
|
||||
*
|
||||
* - `trigger_message` / `reply`: `message.get` by message_id.
|
||||
* - `status_card`: the run's status card message — same `message.get` by id.
|
||||
* - `thread`: lark's thread replies. The SDK exposes `message.list` with a
|
||||
* `parent_message_id` filter; we map "thread" to that.
|
||||
*
|
||||
* The lark SDK's `im.v1.message` methods are dynamic at runtime (weak types);
|
||||
* we cast through a known request/response shape and return a compact JSON for
|
||||
* the model. All calls use the chat-authorized `client` from the runtime — no
|
||||
* separate credential path, so the ADR-0003 invariant holds end-to-end.
|
||||
*/
|
||||
import type { FeishuRuntime } from "./client.js";
|
||||
import type { FeishuContextArgs } from "../agent/tools.js";
|
||||
import type { ToolContext } from "../agent/tools.js";
|
||||
|
||||
/** Pragmatic shape of the lark message object we consume. */
|
||||
interface LarkMessage {
|
||||
message_id?: string;
|
||||
msg_type?: string;
|
||||
content?: string;
|
||||
create_time?: string;
|
||||
sender?: { id?: string; sender_type?: string };
|
||||
chat_id?: string;
|
||||
parent_message_id?: string;
|
||||
root_id?: string;
|
||||
}
|
||||
|
||||
interface ImV1Message {
|
||||
get: (p: { path: { message_id: string } }) => Promise<{ data?: { items?: LarkMessage[]; message?: LarkMessage } }>;
|
||||
list: (p: {
|
||||
params: { container_id_type: string; container_id: string; page_size?: number };
|
||||
}) => Promise<{ data?: { items?: LarkMessage[] } }>;
|
||||
}
|
||||
|
||||
function im(rt: FeishuRuntime): ImV1Message {
|
||||
return (rt.client as unknown as { im: { v1: { message: ImV1Message } } }).im.v1.message;
|
||||
}
|
||||
|
||||
/** Read on-demand Feishu context for the current run. Entry point for the tool. */
|
||||
export async function readFeishuContext(
|
||||
args: FeishuContextArgs,
|
||||
_ctx: ToolContext,
|
||||
rt: unknown,
|
||||
): Promise<string> {
|
||||
const runtime = rt as FeishuRuntime;
|
||||
const api = im(runtime);
|
||||
try {
|
||||
switch (args.anchor) {
|
||||
case "trigger_message":
|
||||
case "status_card":
|
||||
case "reply": {
|
||||
// All three are single-message reads by id.
|
||||
const res = await api.get({ path: { message_id: args.id } });
|
||||
const msg = res.data?.message ?? res.data?.items?.[0];
|
||||
if (msg === undefined) return JSON.stringify({ error: "message not found", id: args.id });
|
||||
return JSON.stringify(compact(msg));
|
||||
}
|
||||
case "thread": {
|
||||
// Thread = replies to a parent message. `container_id` is the parent's
|
||||
// message_id; container_id_type=message_id scopes the list to that thread.
|
||||
const res = await api.list({
|
||||
params: {
|
||||
container_id_type: "message_id",
|
||||
container_id: args.id,
|
||||
page_size: 50,
|
||||
},
|
||||
});
|
||||
const items = res.data?.items ?? [];
|
||||
return JSON.stringify(items.map(compact));
|
||||
}
|
||||
default:
|
||||
return JSON.stringify({ error: `unknown anchor type: ${args.anchor as string}` });
|
||||
}
|
||||
} catch (e) {
|
||||
return JSON.stringify({ error: e instanceof Error ? e.message : String(e) });
|
||||
}
|
||||
}
|
||||
|
||||
/** Project a lark message down to the fields the model actually needs. */
|
||||
function compact(m: LarkMessage): Record<string, unknown> {
|
||||
return {
|
||||
message_id: m.message_id,
|
||||
msg_type: m.msg_type,
|
||||
content: m.content,
|
||||
create_time: m.create_time,
|
||||
sender_id: m.sender?.id,
|
||||
parent_message_id: m.parent_message_id,
|
||||
root_id: m.root_id,
|
||||
};
|
||||
}
|
||||
|
||||
@@ -1,361 +0,0 @@
|
||||
/**
|
||||
* Feishu @bot trigger → AgentRun lifecycle.
|
||||
*
|
||||
* The core path (ADR-0001..0003, 0017):
|
||||
* 1. A message mentioning the bot arrives in a project group.
|
||||
* 2. Resolve the chat → project binding (ADR-0001). Unknown chat ⇒ ignored.
|
||||
* 3. Create an AgentRun + AgentSession (provider-bound, ADR-0017).
|
||||
* 4. Acquire the project lock for the run (ADR-0002). If locked, reply busy.
|
||||
* 5. Run the agent loop; the agent reads Feishu context on demand through the
|
||||
* ADR-0003-authorized tool (chat must match binding).
|
||||
* 6. On finish/fail/timeout: release the lock, post a status card.
|
||||
*
|
||||
* The agent model id comes from the ModelRegistry (ADR-0017 role-based
|
||||
* routing, role-as-data). The trigger does not pick a model directly.
|
||||
*/
|
||||
import type { PrismaClient } from "@prisma/client";
|
||||
import type { FastifyBaseLogger } from "fastify";
|
||||
import { sendText, sendCard, buildRunStatusCard, type FeishuRuntime, type MessageReceiveEvent } from "./client.js";
|
||||
import type { ToolRegistry } from "../agent/tools.js";
|
||||
import type { ModelRegistry } from "../agent/models.js";
|
||||
import { runAgent, type ModelFactory, type ProjectContext } from "../agent/runner.js";
|
||||
import { acquireLock, currentLockRunId, releaseLock } from "../lock.js";
|
||||
import { canTriggerAgent, canTriggerRole } from "../permission.js";
|
||||
import { transcriptPath } from "../agent/transcript.js";
|
||||
import { writeAudit } from "../audit.js";
|
||||
|
||||
interface TriggerDeps {
|
||||
readonly prisma: PrismaClient;
|
||||
readonly modelFactory: ModelFactory;
|
||||
readonly tools: ToolRegistry;
|
||||
readonly models: ModelRegistry;
|
||||
readonly logger: FastifyBaseLogger;
|
||||
}
|
||||
|
||||
/**
|
||||
* Build the message handler. Returns a function suitable for the lark
|
||||
* `im.message.receive_v1` event. The handler is async and long-running (the
|
||||
* agent run is the long leg); the lock guarantees one run per project at a time.
|
||||
*/
|
||||
export function makeTriggerHandler(deps: TriggerDeps) {
|
||||
return async (event: MessageReceiveEvent, rt: FeishuRuntime): Promise<void> => {
|
||||
const msg = event.message;
|
||||
const sender = event.sender;
|
||||
void sender; // sender→user mapping is OPEN (principal sub-typology)
|
||||
|
||||
// Dedup: the lark ws client redelivers at-least-once. A duplicate event
|
||||
// would spawn a second AgentRun — the lock would refuse it, but a FAILED
|
||||
// run row + a busy reply would leak. Record the event_id up front; if it
|
||||
// already exists, this is a redelivery → stop.
|
||||
const eventId = event.header?.event_id;
|
||||
if (eventId !== undefined && eventId !== "") {
|
||||
const existing = await deps.prisma.feishuEventReceipt.findUnique({
|
||||
where: { eventId },
|
||||
select: { id: true },
|
||||
});
|
||||
if (existing !== null) {
|
||||
deps.logger.debug({ eventId }, "feishu trigger: duplicate event, skipping");
|
||||
return;
|
||||
}
|
||||
await deps.prisma.feishuEventReceipt.create({
|
||||
data: {
|
||||
eventId,
|
||||
eventType: event.header?.event_type ?? "im.message.receive_v1",
|
||||
messageId: msg.message_id,
|
||||
},
|
||||
});
|
||||
}
|
||||
|
||||
// Only react to text messages in group chats.
|
||||
if (msg.message_type !== "text") return;
|
||||
const chatId = msg.chat_id;
|
||||
if (chatId === "") return;
|
||||
|
||||
// ADR-0001: resolve chat → project. Unknown chat ⇒ not a project group.
|
||||
const binding = await deps.prisma.projectGroupBinding.findUnique({
|
||||
where: { chatId },
|
||||
select: { projectId: true },
|
||||
});
|
||||
if (binding === null) {
|
||||
deps.logger.debug({ chatId }, "feishu trigger: chat not bound to any project");
|
||||
return;
|
||||
}
|
||||
const projectId = binding.projectId;
|
||||
// ADR-0004: triggerAgent requires edit on the project. principal=sender
|
||||
// open_id (sub-typology OPEN — pragmatic choice, see permission.ts).
|
||||
const senderOpenId = event.sender.sender_id.open_id ?? "";
|
||||
if (senderOpenId !== "") {
|
||||
const perm = await canTriggerAgent(deps.prisma, projectId, senderOpenId);
|
||||
if (!perm.allowed) {
|
||||
deps.logger.info({ projectId, senderOpenId, reason: perm.reason }, "feishu trigger: permission denied");
|
||||
await writeAudit(deps.prisma, { projectId, actorUserId: senderOpenId || undefined, action: "trigger.denied", metadata: { reason: perm.reason } });
|
||||
await sendText(rt, chatId, "无权限触发。");
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
||||
const prompt = extractPrompt(msg);
|
||||
if (prompt === null) return;
|
||||
|
||||
// Slash commands: session management, not agent runs. These bypass the
|
||||
// lock — they don't create a run, so they can't conflict with one.
|
||||
if (prompt.startsWith("/")) {
|
||||
const cmd = prompt.split(/\s+/)[0];
|
||||
switch (cmd) {
|
||||
case "/new": {
|
||||
await deps.prisma.agentSession.updateMany({
|
||||
where: { projectId, archivedAt: null },
|
||||
data: { archivedAt: new Date() },
|
||||
});
|
||||
await sendText(rt, chatId, "已开新会话,下次 @bot 将从头开始。");
|
||||
return;
|
||||
}
|
||||
case "/resume": {
|
||||
const latest = await deps.prisma.agentSession.findFirst({
|
||||
where: { projectId, archivedAt: { not: null } },
|
||||
orderBy: { archivedAt: "desc" },
|
||||
select: { id: true },
|
||||
});
|
||||
if (latest === null) {
|
||||
await sendText(rt, chatId, "没有可恢复的会话。");
|
||||
return;
|
||||
}
|
||||
await deps.prisma.agentSession.update({
|
||||
where: { id: latest.id },
|
||||
data: { archivedAt: null },
|
||||
});
|
||||
await sendText(rt, chatId, "已恢复上一个会话。");
|
||||
return;
|
||||
}
|
||||
case "/reset": {
|
||||
await deps.prisma.agentSession.updateMany({
|
||||
where: { projectId, archivedAt: null },
|
||||
data: { archivedAt: new Date() },
|
||||
});
|
||||
await sendText(rt, chatId, "已重置,下次 @bot 将从头开始。");
|
||||
return;
|
||||
}
|
||||
default:
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
// ADR-0002: if locked by another run, reply busy.
|
||||
const existing = await currentLockRunId(deps.prisma, projectId);
|
||||
if (existing !== null) {
|
||||
await sendText(rt, chatId, "项目正在处理中,请稍候。");
|
||||
return;
|
||||
}
|
||||
|
||||
const project = await deps.prisma.project.findUnique({
|
||||
where: { id: projectId },
|
||||
select: { workspaceDir: true },
|
||||
});
|
||||
if (project === null) {
|
||||
deps.logger.error({ projectId }, "feishu trigger: project missing");
|
||||
return;
|
||||
}
|
||||
|
||||
// ADR-0017: role-as-data. Parse a leading `/<role>` command; unknown
|
||||
// slashes are left as literal text (extractRole returns null). Falls back
|
||||
// to "draft" when no role is named — the registry degrades gracefully.
|
||||
const { roleId: parsedRole, prompt: cleanPrompt } = extractRole(prompt, deps.models);
|
||||
const roleId = parsedRole ?? "draft";
|
||||
// Per-role trigger gate (ADR-0017). Orthogonal to ADR-0004's
|
||||
// canTriggerAgent above: that checked "can trigger an agent at all";
|
||||
// this checks "can trigger *this* role". Unconfigured role ⇒ open.
|
||||
if (senderOpenId !== "") {
|
||||
const rolePerm = await canTriggerRole(deps.prisma, projectId, roleId, senderOpenId);
|
||||
if (!rolePerm.allowed) {
|
||||
deps.logger.info({ projectId, roleId, senderOpenId, reason: rolePerm.reason }, "feishu trigger: role permission denied");
|
||||
await writeAudit(deps.prisma, { projectId, actorUserId: senderOpenId || undefined, action: "trigger.role_denied", metadata: { roleId, reason: rolePerm.reason } });
|
||||
await sendText(rt, chatId, `无权限使用角色 ${roleId}。`);
|
||||
return;
|
||||
}
|
||||
}
|
||||
const role = deps.models.role(roleId);
|
||||
const model = deps.models.resolve(undefined, roleId);
|
||||
const providerId = "openrouter";
|
||||
// Per-role bundle (ADR-0017): systemPrompt seeds persona; tools whitelist
|
||||
// is enforced inside runAgent when it builds the SDK tools record. `tools:
|
||||
// undefined` means the full registered set (unrestricted role).
|
||||
const systemPrompt = role?.systemPrompt;
|
||||
|
||||
// ADR-0017: provider+model-bound session. Reuse if one exists for this
|
||||
// (project, provider, model) triple; otherwise create.
|
||||
const existingSession = await deps.prisma.agentSession.findFirst({
|
||||
where: { projectId, provider: providerId, model, archivedAt: null },
|
||||
select: { id: true },
|
||||
});
|
||||
const session =
|
||||
existingSession !== null
|
||||
? await deps.prisma.agentSession.update({
|
||||
where: { id: existingSession.id },
|
||||
data: { provider: providerId, model, updatedAt: new Date() },
|
||||
select: { id: true },
|
||||
})
|
||||
: await deps.prisma.agentSession.create({
|
||||
data: {
|
||||
projectId,
|
||||
provider: providerId,
|
||||
model,
|
||||
title: cleanPrompt.slice(0, 40) || null,
|
||||
metadata: {},
|
||||
},
|
||||
select: { id: true },
|
||||
});
|
||||
|
||||
const run = await deps.prisma.agentRun.create({
|
||||
data: {
|
||||
projectId,
|
||||
sessionId: session.id,
|
||||
requestedByUserId: null, // sender→user mapping is OPEN (principal sub-typology)
|
||||
entrypoint: "FEISHU",
|
||||
status: "ACTIVE",
|
||||
prompt: cleanPrompt,
|
||||
model,
|
||||
provider: providerId,
|
||||
metadata: { roleId },
|
||||
},
|
||||
select: { id: true },
|
||||
});
|
||||
await writeAudit(deps.prisma, { runId: run.id, projectId, action: "run.created", metadata: { roleId, model, prompt: cleanPrompt.slice(0, 200) } });
|
||||
|
||||
// ADR-0002: acquire the project lock for this run.
|
||||
try {
|
||||
await acquireLock(deps.prisma, projectId, run.id, null);
|
||||
} catch {
|
||||
await deps.prisma.agentRun.update({
|
||||
where: { id: run.id },
|
||||
data: { status: "FAILED", error: "lock race", finishedAt: new Date() },
|
||||
});
|
||||
await writeAudit(deps.prisma, { runId: run.id, projectId, action: "run.lock_race", metadata: {} });
|
||||
await sendText(rt, chatId, "项目正在处理中,请稍候。");
|
||||
return;
|
||||
}
|
||||
|
||||
await sendText(rt, chatId, `已开始处理(role: ${roleId}, model: ${model})。`);
|
||||
|
||||
const projectCtx: ProjectContext = {
|
||||
projectId,
|
||||
boundChatId: chatId, // ADR-0003: Feishu reads stay in this chat
|
||||
workspaceDir: project.workspaceDir,
|
||||
};
|
||||
|
||||
// Run the agent — fire-and-forget from the ws handler's perspective.
|
||||
// Per-run tools + systemPrompt come from the role bundle (ADR-0017).
|
||||
runAgent(deps.modelFactory, deps.tools, {
|
||||
prompt: cleanPrompt,
|
||||
model,
|
||||
project: projectCtx,
|
||||
systemPrompt,
|
||||
toolWhitelist: role?.tools,
|
||||
transcriptPath: transcriptPath(project.workspaceDir, session.id),
|
||||
})
|
||||
.then(async (result) => {
|
||||
await deps.prisma.agentRun.update({
|
||||
where: { id: run.id },
|
||||
data: {
|
||||
status:
|
||||
result.status === "completed"
|
||||
? "COMPLETED"
|
||||
: result.status === "length"
|
||||
? "TIMED_OUT"
|
||||
: "FAILED",
|
||||
inputTokens: result.usage.inputTokens,
|
||||
outputTokens: result.usage.outputTokens,
|
||||
error: result.error ?? null,
|
||||
finishedAt: new Date(),
|
||||
},
|
||||
});
|
||||
await writeAudit(deps.prisma, { runId: run.id, projectId, action: "run.finished", metadata: { status: result.status, inputTokens: result.usage.inputTokens, outputTokens: result.usage.outputTokens } });
|
||||
await sendCard(rt, chatId, buildRunStatusCard({
|
||||
status: statusReply(result.status),
|
||||
model,
|
||||
models: deps.models.listModels(),
|
||||
runId: run.id,
|
||||
}));
|
||||
})
|
||||
.catch(async (e) => {
|
||||
// The run may have been removed (admin force-delete, or test reset)
|
||||
// between creation and this callback. A P2025 from update is not
|
||||
// actionable here — log and still post the status card.
|
||||
try {
|
||||
await deps.prisma.agentRun.update({
|
||||
where: { id: run.id },
|
||||
data: { status: "FAILED", error: String(e), finishedAt: new Date() },
|
||||
});
|
||||
} catch (updateErr) {
|
||||
deps.logger.warn({ runId: run.id, err: String(updateErr) }, "trigger: could not mark run FAILED (already gone?)");
|
||||
}
|
||||
await writeAudit(deps.prisma, { runId: run.id, projectId, action: "run.failed", metadata: { error: String(e) } });
|
||||
await sendCard(rt, chatId, buildRunStatusCard({
|
||||
status: "处理出错",
|
||||
model,
|
||||
models: deps.models.listModels(),
|
||||
runId: run.id,
|
||||
}));
|
||||
})
|
||||
.finally(async () => {
|
||||
await releaseLock(deps.prisma, run.id);
|
||||
});
|
||||
};
|
||||
}
|
||||
|
||||
function statusReply(status: "completed" | "length" | "failed"): string {
|
||||
switch (status) {
|
||||
case "completed":
|
||||
return "处理完成。";
|
||||
case "length":
|
||||
return "处理达到步数上限,已停止。";
|
||||
case "failed":
|
||||
return "处理出错。";
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Extract the prompt text from a text message, stripping @mentions.
|
||||
* Returns null if the message is empty after stripping or doesn't mention the bot.
|
||||
* Lark text content is JSON: `{"text":"@_user_1 do something"}`.
|
||||
*/
|
||||
export function extractPrompt(msg: MessageReceiveEvent["message"]): string | null {
|
||||
// Check for bot mention — mentions[].id.open_id should include the bot.
|
||||
// The dispatcher already routes only message events; we further require
|
||||
// that the bot is among the mentions (if no mentions, it's not @bot).
|
||||
const mentions = msg.mentions;
|
||||
if (mentions === undefined || mentions.length === 0) return null;
|
||||
|
||||
try {
|
||||
const parsed = JSON.parse(msg.content) as { text?: string };
|
||||
const text = parsed.text;
|
||||
if (typeof text !== "string") return null;
|
||||
// Strip @mentions (@_user_1 etc.) and trim; remainder is the prompt.
|
||||
const stripped = text.replace(/@_\w+\s*/g, "").trim();
|
||||
return stripped === "" ? null : stripped;
|
||||
} catch {
|
||||
return null;
|
||||
}
|
||||
}
|
||||
/**
|
||||
* Parse a leading `/<role>` command from a prompt (e.g. `/draft 帮我写教案`).
|
||||
* Returns the role id and the remaining prompt with the command stripped.
|
||||
* Control commands already handled upstream (`/new`, `/resume`, `/reset`) are
|
||||
* ignored here — they never reach this function.
|
||||
*
|
||||
* Unknown `/foo` that isn't a registered role: returns `null` role and the
|
||||
* original prompt unchanged (the slash is treated as literal text). Role
|
||||
* resolution still happens via the registry's fallback.
|
||||
*/
|
||||
export function extractRole(
|
||||
prompt: string,
|
||||
registry: { role(id: string): unknown },
|
||||
): { roleId: string | null; prompt: string } {
|
||||
const m = /^\/(\S+)\s*/.exec(prompt);
|
||||
if (m === null || m[1] === undefined) return { roleId: null, prompt };
|
||||
const roleId = m[1];
|
||||
if (registry.role(roleId) === undefined) {
|
||||
// Unknown slash command — leave the prompt as-is (no silent role switch).
|
||||
return { roleId: null, prompt };
|
||||
}
|
||||
return { roleId, prompt: prompt.slice(m[0].length) };
|
||||
}
|
||||
@@ -1,79 +0,0 @@
|
||||
/**
|
||||
* ProjectAgentLock — ADR-0002 invariant enforcement at the DB layer.
|
||||
*
|
||||
* `projectId @id` gives at-most-one lock per project; `runId @unique` gives a
|
||||
* run holds at most one lock. Those are DB-level. The spec's `WellFormed`
|
||||
* invariant ("holder is a non-terminal run") is app-level: it must hold on
|
||||
* every read of the lock table. `assertLockHolderActive` enforces it on the
|
||||
* read path — if a lock exists but its run is terminal, that's a bug (the run
|
||||
* should have released it), surfaced as an error rather than silently trusted.
|
||||
*/
|
||||
import type { PrismaClient } from "@prisma/client";
|
||||
import type { AgentRunStatus } from "@prisma/client";
|
||||
|
||||
/// spec RunState.Terminal: completed/failed/timedOut/canceled.
|
||||
/// active/waitingForUser are NOT terminal — the lock must still be held.
|
||||
const TERMINAL_STATUSES: ReadonlySet<AgentRunStatus> = new Set([
|
||||
"COMPLETED",
|
||||
"FAILED",
|
||||
"TIMED_OUT",
|
||||
"CANCELED",
|
||||
]);
|
||||
|
||||
export function isTerminal(status: AgentRunStatus): boolean {
|
||||
return TERMINAL_STATUSES.has(status);
|
||||
}
|
||||
|
||||
/**
|
||||
* Acquire the project lock for a run. Throws if the project is already locked
|
||||
* by another run (ADR-0002 exclusivity). The unique runId constraint means a
|
||||
* run that already holds a lock elsewhere will also fail — that's correct, a
|
||||
* run scopes to one project.
|
||||
*/
|
||||
export async function acquireLock(
|
||||
prisma: PrismaClient,
|
||||
projectId: string,
|
||||
runId: string,
|
||||
holderUserId: string | null,
|
||||
): Promise<void> {
|
||||
await prisma.projectAgentLock.create({
|
||||
data: { projectId, runId, holderUserId },
|
||||
});
|
||||
}
|
||||
|
||||
/**
|
||||
* Release the lock owned by a run. Idempotent — a no-op if no lock exists.
|
||||
* Called on run completion/failure/timeout/cancellation (ADR-0002).
|
||||
*/
|
||||
export async function releaseLock(prisma: PrismaClient, runId: string): Promise<void> {
|
||||
await prisma.projectAgentLock.deleteMany({ where: { runId } });
|
||||
}
|
||||
|
||||
/**
|
||||
* The spec's `LockTable.WellFormed` on a single read: if `projectId` has a
|
||||
* lock owned by `runId`, that run must be non-terminal. Throws if a terminal
|
||||
* run still holds a lock — that's a release-path bug, not a recoverable state.
|
||||
*
|
||||
* Returns the lock's runId if a healthy lock exists, or null if unlocked.
|
||||
*/
|
||||
export async function currentLockRunId(
|
||||
prisma: PrismaClient,
|
||||
projectId: string,
|
||||
): Promise<string | null> {
|
||||
const lock = await prisma.projectAgentLock.findUnique({
|
||||
where: { projectId },
|
||||
select: { runId: true },
|
||||
});
|
||||
if (lock === null) return null;
|
||||
|
||||
const run = await prisma.agentRun.findUnique({
|
||||
where: { id: lock.runId },
|
||||
select: { status: true },
|
||||
});
|
||||
if (run !== null && isTerminal(run.status)) {
|
||||
throw new Error(
|
||||
`lock invariant violated: project ${projectId} locked by terminal run ${lock.runId} (status ${run.status}) — release path bug (ADR-0002 WellFormed)`,
|
||||
);
|
||||
}
|
||||
return lock.runId;
|
||||
}
|
||||
@@ -1,126 +0,0 @@
|
||||
/**
|
||||
* Permission gate — ADR-0004 in code, project-scope.
|
||||
*
|
||||
* `triggerAgent` requires the `edit` capability (ADR-0004). `edit` is granted
|
||||
* by a `PermissionGrant` with role `edit` or `manage` (manage ⊇ edit, spec
|
||||
* `Role.can_mono`). This module checks that for the run's requester against
|
||||
* the project resource.
|
||||
*
|
||||
* Scope decision (project-wise): the resource is `project`, not
|
||||
* `project_group` — the run and lock scope to the project (ADR-0002), so the
|
||||
* capability is checked against the project. per-artifact permission is `OPEN`
|
||||
* pending a Courseware-side artifact id (ADR-0004 + ADR-0007 mapping).
|
||||
*
|
||||
* principal→user mapping is `OPEN` (ADR-0004 principal sub-typology). Here we
|
||||
* use the sender's Feishu open_id as the principal string literal — a pragmatic
|
||||
* choice for the first cut, not a spec decision. When a real principal model
|
||||
* lands, this is the single seam to change.
|
||||
*
|
||||
* settings.agentTrigger composition is `OPEN` (ADR-0004 separates role-derived
|
||||
* capabilities from settings policy knobs but doesn't pin the composition
|
||||
* rule). This gate implements the role half only; settings composition is
|
||||
* deferred and clearly marked.
|
||||
*/
|
||||
import type { PrismaClient } from "@prisma/client";
|
||||
import type { PermissionRole } from "@prisma/client";
|
||||
|
||||
/// The roles that grant `edit` capability (edit itself + manage, by monotonicity).
|
||||
const EDIT_OR_HIGHER: ReadonlySet<PermissionRole> = new Set(["EDIT", "MANAGE"]);
|
||||
|
||||
export interface PermissionResult {
|
||||
readonly allowed: boolean;
|
||||
readonly reason: string;
|
||||
}
|
||||
|
||||
/**
|
||||
* Check whether `principal` may trigger an agent run on `projectId`.
|
||||
*
|
||||
* Returns `{allowed, reason}`. On allow, the caller proceeds; on deny, the
|
||||
* caller replies with the reason. Never throws — a DB error is a deny with the
|
||||
* error as reason, so the run is not started on a broken state.
|
||||
*/
|
||||
export async function canTriggerAgent(
|
||||
prisma: PrismaClient,
|
||||
projectId: string,
|
||||
principal: string,
|
||||
): Promise<PermissionResult> {
|
||||
try {
|
||||
// Look for an active (non-revoked) grant on the project resource for this
|
||||
// principal, with a role that grants edit or higher.
|
||||
const grant = await prisma.permissionGrant.findFirst({
|
||||
where: {
|
||||
resourceType: "PROJECT",
|
||||
resourceId: projectId,
|
||||
principal,
|
||||
role: { in: ["EDIT", "MANAGE"] },
|
||||
revokedAt: null,
|
||||
},
|
||||
select: { id: true, role: true },
|
||||
});
|
||||
if (grant !== null) {
|
||||
return { allowed: true, reason: `granted by role ${grant.role}` };
|
||||
}
|
||||
return {
|
||||
allowed: false,
|
||||
reason: `no active edit+ grant for ${principal} on project ${projectId}`,
|
||||
};
|
||||
} catch (e) {
|
||||
return { allowed: false, reason: `permission check failed: ${e instanceof Error ? e.message : String(e)}` };
|
||||
}
|
||||
}
|
||||
/**
|
||||
* Per-role trigger gate (ADR-0017: roles are product config). Orthogonal to
|
||||
* {@link canTriggerAgent}: that decides "can trigger an agent at all"
|
||||
* (ADR-0004 triggerAgent capability); this decides "can trigger *which* role".
|
||||
* Two gates in series — both must pass.
|
||||
*
|
||||
* Semantics: if **no** `RoleTriggerGrant` row exists for `(projectId, roleId)`
|
||||
* (regardless of principal), the role is unconfigured on this project →
|
||||
* **allow** (back-compat: a project that hasn't configured per-role grants
|
||||
* doesn't get locked down). Once any grant exists for that role on the
|
||||
* project, only principals with an active grant may trigger it. "Grants exist
|
||||
* but this principal has none" → deny (admin explicitly restricted the role).
|
||||
*
|
||||
* `roleId` matches `RoleEntry.id` (the slash-command name). `principal` is the
|
||||
* same opaque string ADR-0004 uses (sender open_id here; principal
|
||||
* sub-typology OPEN).
|
||||
*/
|
||||
export async function canTriggerRole(
|
||||
prisma: PrismaClient,
|
||||
projectId: string,
|
||||
roleId: string,
|
||||
principal: string,
|
||||
): Promise<PermissionResult> {
|
||||
try {
|
||||
// Any grant record (active OR revoked) for this (project, role)? If none,
|
||||
// the role is unconfigured → allow (back-compat: no per-role restriction).
|
||||
// A revoked grant still counts as "configured" — revoking one person must
|
||||
// not silently reopen the role to everyone.
|
||||
const anyGrant = await prisma.roleTriggerGrant.findFirst({
|
||||
where: { projectId, roleId },
|
||||
select: { id: true },
|
||||
});
|
||||
if (anyGrant === null) {
|
||||
return { allowed: true, reason: `role ${roleId} unconfigured on project (open)` };
|
||||
}
|
||||
// Grants exist — this principal must hold one.
|
||||
const grant = await prisma.roleTriggerGrant.findFirst({
|
||||
where: { projectId, roleId, principal, revokedAt: null },
|
||||
select: { id: true },
|
||||
});
|
||||
if (grant !== null) {
|
||||
return { allowed: true, reason: `granted role ${roleId}` };
|
||||
}
|
||||
return {
|
||||
allowed: false,
|
||||
reason: `no active ${roleId} grant for ${principal} on project ${projectId}`,
|
||||
};
|
||||
} catch (e) {
|
||||
return { allowed: false, reason: `role permission check failed: ${e instanceof Error ? e.message : String(e)}` };
|
||||
}
|
||||
}
|
||||
|
||||
/// Whether a role grants edit capability (edit or manage). Exported for tests.
|
||||
export function roleGrantsEdit(role: PermissionRole): boolean {
|
||||
return EDIT_OR_HIGHER.has(role);
|
||||
}
|
||||
@@ -1,107 +0,0 @@
|
||||
/**
|
||||
* Hub entry — Fastify server + Feishu WebSocket listener.
|
||||
*
|
||||
* Wires the full trigger path: lark ws receives `im.message.receive_v1` →
|
||||
* trigger handler resolves chat->project (ADR-0001), creates AgentRun + acquires
|
||||
* the project lock (ADR-0002), runs the AI SDK-backed agent runner
|
||||
* (ADR-0017), and releases the lock on finish. Feishu context reads inside the
|
||||
* loop are ADR-0003-authorized (chat must match binding).
|
||||
*
|
||||
* Env (see .env.example):
|
||||
* DATABASE_URL, OPENROUTER_API_KEY, FEISHU_APP_ID/SECRET/BOT_OPEN_ID, PORT
|
||||
*/
|
||||
import "dotenv/config";
|
||||
import Fastify from "fastify";
|
||||
import { prisma } from "./db.js";
|
||||
import { createModelFactory } from "./agent/provider.js";
|
||||
import { InMemoryModelRegistry } from "./agent/models.js";
|
||||
import { ToolRegistry, feishuContextTool } from "./agent/tools.js";
|
||||
import { readFileTool, writeFileTool, listFilesTool } from "./agent/workspace.js";
|
||||
import { cphCheckTool, cphBuildTool } from "./agent/cph.js";
|
||||
import { createLarkClient, startFeishuListenerWithClient, type FeishuRuntime } from "./feishu/client.js";
|
||||
import { readFeishuContext } from "./feishu/read.js";
|
||||
import { makeTriggerHandler } from "./feishu/trigger.js";
|
||||
|
||||
function requireEnv(name: string): string {
|
||||
const v = process.env[name];
|
||||
if (v === undefined || v === "") {
|
||||
console.error(`[hub] missing required env: ${name}`);
|
||||
process.exit(1);
|
||||
}
|
||||
return v;
|
||||
}
|
||||
|
||||
async function main(): Promise<void> {
|
||||
const databaseUrl = requireEnv("DATABASE_URL");
|
||||
void databaseUrl; // prisma reads DATABASE_URL from env directly
|
||||
requireEnv("OPENROUTER_API_KEY");
|
||||
const feishuAppId = requireEnv("FEISHU_APP_ID");
|
||||
const feishuAppSecret = requireEnv("FEISHU_APP_SECRET");
|
||||
const feishuBotOpenId = requireEnv("FEISHU_BOT_OPEN_ID");
|
||||
const port = Number(process.env["PORT"] ?? "8788");
|
||||
|
||||
const app = Fastify({ logger: true });
|
||||
|
||||
app.get("/api/healthz", async () => ({ ok: true, ts: Date.now() }));
|
||||
|
||||
// --- Agent seam wiring ---
|
||||
const modelFactory = createModelFactory();
|
||||
const models = new InMemoryModelRegistry(
|
||||
[
|
||||
{ id: "z-ai/glm-4.6", label: "GLM-4.6", toolCapable: true },
|
||||
{ id: "anthropic/claude-3.5-sonnet", label: "Claude 3.5 Sonnet", toolCapable: true },
|
||||
],
|
||||
[
|
||||
{
|
||||
id: "draft",
|
||||
label: "草稿",
|
||||
defaultModel: "z-ai/glm-4.6",
|
||||
systemPrompt: undefined,
|
||||
// Drafting needs full workspace + cph access.
|
||||
tools: ["read_file", "write_file", "list_files", "cph_check", "cph_build", "feishu_read_context"],
|
||||
},
|
||||
{
|
||||
id: "review",
|
||||
label: "审校",
|
||||
defaultModel: "anthropic/claude-3.5-sonnet",
|
||||
systemPrompt: undefined,
|
||||
// Review is read-only on artifacts; no write_file, no build.
|
||||
tools: ["read_file", "list_files", "cph_check", "feishu_read_context"],
|
||||
},
|
||||
],
|
||||
);
|
||||
|
||||
// Build the lark client first — tools that call Feishu APIs hold it from boot.
|
||||
const feishuConfig = { appId: feishuAppId, appSecret: feishuAppSecret, botOpenId: feishuBotOpenId };
|
||||
const larkClient = createLarkClient(feishuConfig);
|
||||
const feishuRt: FeishuRuntime = { client: larkClient, logger: app.log };
|
||||
|
||||
const tools = new ToolRegistry();
|
||||
// ADR-0003: the handler enforces chat==boundChat before any API call;
|
||||
// real read wraps @larksuiteoapi/node-sdk's im.v1.message get/list.
|
||||
tools.register("feishu_read_context", feishuContextTool(readFeishuContext, feishuRt));
|
||||
// Workspace file tools (ADR-0007 directory tree, path-confined).
|
||||
tools.register("read_file", readFileTool);
|
||||
tools.register("write_file", writeFileTool);
|
||||
tools.register("list_files", listFilesTool);
|
||||
// cph CLI tools (ADR-0016 version contract enforced by cph itself).
|
||||
tools.register("cph_check", cphCheckTool);
|
||||
tools.register("cph_build", cphBuildTool);
|
||||
|
||||
// --- Feishu listener (reuses the same lark client) ---
|
||||
const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: app.log });
|
||||
startFeishuListenerWithClient(feishuConfig, larkClient, app.log, trigger);
|
||||
|
||||
app.listen({ port, host: "0.0.0.0" }, (err, address) => {
|
||||
if (err !== null) {
|
||||
app.log.error({ err }, "listen failed");
|
||||
process.exit(1);
|
||||
}
|
||||
app.log.info({ address }, "hub listening");
|
||||
});
|
||||
}
|
||||
|
||||
main().catch((e) => {
|
||||
console.error("[hub] fatal:", e);
|
||||
process.exit(1);
|
||||
});
|
||||
@@ -1,64 +0,0 @@
|
||||
import { describe, it, expect, beforeEach, afterEach } from "vitest";
|
||||
import { cp, mkdtemp, rm } from "node:fs/promises";
|
||||
import { tmpdir } from "node:os";
|
||||
import { join } from "node:path";
|
||||
import { ToolRegistry, type ToolContext } from "../../src/agent/tools.js";
|
||||
import { cphCheckTool, cphBuildTool } from "../../src/agent/cph.js";
|
||||
|
||||
const EXAMPLES_DIR = join(process.cwd(), "..", "examples", "TH-141");
|
||||
|
||||
describe("cph subprocess tools (integration, real cph binary)", () => {
|
||||
let ws: string;
|
||||
let tools: ToolRegistry;
|
||||
|
||||
beforeEach(async () => {
|
||||
// Use a writable copy of the real TH-141 example as the workspace.
|
||||
ws = await mkdtemp(join(tmpdir(), "hub-cph-example-"));
|
||||
await cp(EXAMPLES_DIR, ws, { recursive: true });
|
||||
tools = new ToolRegistry();
|
||||
tools.register("cph_check", cphCheckTool);
|
||||
tools.register("cph_build", cphBuildTool);
|
||||
});
|
||||
|
||||
afterEach(async () => {
|
||||
await rm(ws, { recursive: true, force: true });
|
||||
});
|
||||
|
||||
it("cph_check runs on the TH-141 example and returns diagnostics", async () => {
|
||||
const ctx = { runId: "r", projectId: "p", boundChatId: "c", workspaceDir: ws };
|
||||
const out = await executeTool(tools, "cph_check", {}, ctx);
|
||||
const result = JSON.parse(out) as { exitCode: number; stdout: string; stderr: string };
|
||||
|
||||
// cph check exits 0 on a legal lesson (no error diagnostics, ADR-0010).
|
||||
// If the example has warnings, exit is still 0.
|
||||
expect(result.exitCode).toBe(0);
|
||||
}, 30000);
|
||||
|
||||
it("cph_build renders the student target PDF", async () => {
|
||||
const ctx = { runId: "r", projectId: "p", boundChatId: "c", workspaceDir: ws };
|
||||
const out = await executeTool(tools, "cph_build", { target: "student", output: "build/test-student.pdf" }, ctx);
|
||||
const result = JSON.parse(out) as { exitCode: number; stdout: string; stderr: string; output: string };
|
||||
|
||||
expect(result.exitCode).toBe(0);
|
||||
}, 30000);
|
||||
|
||||
it("cph_check on a temp dir with no engineering file returns non-zero", async () => {
|
||||
const empty = await mkdtemp(join(tmpdir(), "hub-cph-empty-"));
|
||||
try {
|
||||
const ctx = { runId: "r", projectId: "p", boundChatId: "c", workspaceDir: empty };
|
||||
const out = await executeTool(tools, "cph_check", {}, ctx);
|
||||
const result = JSON.parse(out) as { exitCode: number };
|
||||
expect(result.exitCode).not.toBe(0);
|
||||
} finally {
|
||||
await rm(empty, { recursive: true, force: true });
|
||||
}
|
||||
}, 15000);
|
||||
});
|
||||
|
||||
async function executeTool(tools: ToolRegistry, name: string, args: unknown, ctx: ToolContext): Promise<string> {
|
||||
const def = tools.build(ctx)[name];
|
||||
if (def?.execute === undefined) {
|
||||
throw new Error(`missing executable tool: ${name}`);
|
||||
}
|
||||
return def.execute(args, { toolCallId: "call", messages: [], context: undefined }) as Promise<string>;
|
||||
}
|
||||
@@ -1,207 +0,0 @@
|
||||
/**
|
||||
* Test helpers for integration tests.
|
||||
*
|
||||
* Each test gets a clean DB (tables truncated before the test), a mock
|
||||
* FeishuRuntime (sendText/sendCard are no-ops that record calls), and a mock
|
||||
* AI SDK model factory (doGenerate() returns canned responses - no network).
|
||||
*/
|
||||
import { PrismaClient } from "@prisma/client";
|
||||
import type { FastifyBaseLogger } from "fastify";
|
||||
import type {
|
||||
LanguageModelV4,
|
||||
LanguageModelV4CallOptions,
|
||||
LanguageModelV4Content,
|
||||
LanguageModelV4GenerateResult,
|
||||
LanguageModelV4StreamResult,
|
||||
} from "@ai-sdk/provider";
|
||||
import type { FeishuRuntime } from "../../src/feishu/client.js";
|
||||
import type { ModelFactory } from "../../src/agent/runner.js";
|
||||
|
||||
export const TEST_DATABASE_URL = "postgresql://paradigm:paradigm@127.0.0.1:5432/cph_hub_test";
|
||||
|
||||
export const prisma = new PrismaClient({
|
||||
datasources: { db: { url: TEST_DATABASE_URL } },
|
||||
});
|
||||
|
||||
/** Truncate all tables before each test for isolation. */
|
||||
export async function resetDb(): Promise<void> {
|
||||
const tables = [
|
||||
"FeishuEventReceipt",
|
||||
"AuditEntry",
|
||||
"PermissionSettings",
|
||||
"PermissionGrant",
|
||||
"RoleTriggerGrant",
|
||||
"ProjectAgentLock",
|
||||
"AgentRun",
|
||||
"AgentSession",
|
||||
"ProjectGroupBinding",
|
||||
"PlatformRoleAssignment",
|
||||
"User",
|
||||
"Project",
|
||||
];
|
||||
// Truncate with CASCADE to wipe dependent rows in one shot.
|
||||
await prisma.$executeRawUnsafe(`TRUNCATE TABLE ${tables.map((t) => `"${t}"`).join(", ")} RESTART IDENTITY CASCADE`);
|
||||
}
|
||||
|
||||
/** A logger that discards everything (tests don't need fastify's pino). */
|
||||
export const silentLogger: FastifyBaseLogger = {
|
||||
info() {}, warn() {}, error() {}, debug() {}, fatal() {},
|
||||
child() { return this; },
|
||||
level: "silent",
|
||||
} as unknown as FastifyBaseLogger;
|
||||
|
||||
/** Records sendText/sendCard calls so tests can assert on them. */
|
||||
export interface MockFeishuRuntime extends FeishuRuntime {
|
||||
readonly sentTexts: string[];
|
||||
readonly sentCards: unknown[];
|
||||
}
|
||||
|
||||
export function mockFeishuRuntime(): MockFeishuRuntime {
|
||||
const sentTexts: string[] = [];
|
||||
const sentCards: unknown[] = [];
|
||||
// Mock the client — sendText/sendCard are in client.ts, not on the runtime
|
||||
// object directly. We patch by providing a runtime whose client is a stub;
|
||||
// the actual send functions cast through shape, so a minimal stub works.
|
||||
const rt: MockFeishuRuntime = {
|
||||
client: {
|
||||
im: {
|
||||
v1: {
|
||||
message: {
|
||||
create: async (p: unknown) => {
|
||||
const payload = p as { data?: { msg_type?: string; content?: string } };
|
||||
if (payload.data?.msg_type === "interactive") {
|
||||
sentCards.push(payload.data.content ? JSON.parse(payload.data.content) : null);
|
||||
} else {
|
||||
try {
|
||||
const c = JSON.parse(payload.data?.content ?? "{}") as { text?: string };
|
||||
sentTexts.push(c.text ?? payload.data?.content ?? "");
|
||||
} catch {
|
||||
sentTexts.push(payload.data?.content ?? "");
|
||||
}
|
||||
}
|
||||
return { data: { message_id: "mock-msg-id" } };
|
||||
},
|
||||
},
|
||||
},
|
||||
},
|
||||
} as unknown as FeishuRuntime["client"],
|
||||
logger: silentLogger,
|
||||
sentTexts,
|
||||
sentCards,
|
||||
};
|
||||
return rt;
|
||||
}
|
||||
|
||||
export interface MockToolCall {
|
||||
readonly toolCallId: string;
|
||||
readonly toolName: string;
|
||||
readonly input: unknown;
|
||||
}
|
||||
|
||||
export interface MockModelResponse {
|
||||
readonly text?: string;
|
||||
readonly toolCalls?: readonly MockToolCall[];
|
||||
readonly finishReason?: "stop" | "length" | "content-filter" | "tool-calls" | "error" | "other";
|
||||
readonly inputTokens?: number;
|
||||
readonly outputTokens?: number;
|
||||
}
|
||||
|
||||
export class MockLanguageModel implements LanguageModelV4 {
|
||||
readonly specificationVersion = "v4";
|
||||
readonly provider = "mock";
|
||||
readonly supportedUrls: Record<string, RegExp[]> = {};
|
||||
readonly calls: LanguageModelV4CallOptions[] = [];
|
||||
|
||||
constructor(
|
||||
readonly modelId: string,
|
||||
private readonly responses: readonly MockModelResponse[] = [{ text: "mock response" }],
|
||||
) {}
|
||||
|
||||
async doGenerate(options: LanguageModelV4CallOptions): Promise<LanguageModelV4GenerateResult> {
|
||||
this.calls.push(options);
|
||||
const configured = this.responses[this.calls.length - 1];
|
||||
const last = this.responses[this.responses.length - 1];
|
||||
const response =
|
||||
configured ??
|
||||
((last?.toolCalls?.length ?? 0) > 0
|
||||
? { text: "mock response" }
|
||||
: last ?? { text: "mock response" });
|
||||
const content: LanguageModelV4Content[] = [];
|
||||
if (response.text !== undefined) {
|
||||
content.push({ type: "text", text: response.text });
|
||||
}
|
||||
for (const call of response.toolCalls ?? []) {
|
||||
content.push({
|
||||
type: "tool-call",
|
||||
toolCallId: call.toolCallId,
|
||||
toolName: call.toolName,
|
||||
input: JSON.stringify(call.input),
|
||||
});
|
||||
}
|
||||
const finishReason = response.finishReason ?? ((response.toolCalls?.length ?? 0) > 0 ? "tool-calls" : "stop");
|
||||
return {
|
||||
content,
|
||||
finishReason: { unified: finishReason, raw: finishReason },
|
||||
usage: {
|
||||
inputTokens: { total: response.inputTokens ?? 10, noCache: undefined, cacheRead: undefined, cacheWrite: undefined },
|
||||
outputTokens: { total: response.outputTokens ?? 5, text: undefined, reasoning: undefined },
|
||||
},
|
||||
response: { id: `mock-${this.calls.length}`, timestamp: new Date(), modelId: this.modelId },
|
||||
warnings: [],
|
||||
};
|
||||
}
|
||||
|
||||
async doStream(_options: LanguageModelV4CallOptions): Promise<LanguageModelV4StreamResult> {
|
||||
throw new Error("MockLanguageModel does not implement streaming");
|
||||
}
|
||||
}
|
||||
|
||||
export function createMockModelFactory(
|
||||
responses: readonly MockModelResponse[] = [{ text: "mock response" }],
|
||||
): { readonly modelFactory: ModelFactory; readonly models: ReadonlyMap<string, MockLanguageModel> } {
|
||||
const models = new Map<string, MockLanguageModel>();
|
||||
return {
|
||||
models,
|
||||
modelFactory: (modelId) => {
|
||||
const model = new MockLanguageModel(modelId, responses);
|
||||
models.set(modelId, model);
|
||||
return model;
|
||||
},
|
||||
};
|
||||
}
|
||||
|
||||
/** Create a project + binding + user + grant for a test. */
|
||||
export async function seedProject(
|
||||
projectId: string,
|
||||
chatId: string,
|
||||
options: { principal?: string; role?: "READ" | "EDIT" | "MANAGE" } = {},
|
||||
): Promise<void> {
|
||||
const principal = options.principal ?? "ou_test_user";
|
||||
const role = options.role ?? "EDIT";
|
||||
await prisma.project.create({
|
||||
data: {
|
||||
id: projectId,
|
||||
name: `Test ${projectId}`,
|
||||
workspaceDir: `/tmp/test-${projectId}`,
|
||||
},
|
||||
});
|
||||
await prisma.user.create({
|
||||
data: {
|
||||
id: "u_" + projectId,
|
||||
feishuOpenId: principal,
|
||||
displayName: "Test User",
|
||||
platformRoles: { create: { role: "TEACHER" } },
|
||||
permissionGrants: {
|
||||
create: {
|
||||
resourceType: "PROJECT",
|
||||
resourceId: projectId,
|
||||
principal,
|
||||
role,
|
||||
},
|
||||
},
|
||||
},
|
||||
});
|
||||
await prisma.projectGroupBinding.create({
|
||||
data: { projectId, chatId, createdByUserId: "u_" + projectId },
|
||||
});
|
||||
}
|
||||
@@ -1,85 +0,0 @@
|
||||
import { describe, it, expect, beforeEach, afterAll } from "vitest";
|
||||
import { prisma, resetDb } from "./helpers.js";
|
||||
import { acquireLock, releaseLock, currentLockRunId, isTerminal } from "../../src/lock.js";
|
||||
|
||||
describe("ProjectAgentLock WellFormed (integration, ADR-0002)", () => {
|
||||
beforeEach(async () => {
|
||||
await resetDb();
|
||||
});
|
||||
|
||||
it("acquireLock + currentLockRunId round-trip", async () => {
|
||||
const project = await prisma.project.create({
|
||||
data: { id: "p-lock-1", name: "Test", workspaceDir: "/tmp/x" },
|
||||
});
|
||||
const run = await prisma.agentRun.create({
|
||||
data: { projectId: project.id, entrypoint: "FEISHU", status: "ACTIVE", prompt: "x", model: "m", provider: "mock", metadata: {} },
|
||||
});
|
||||
|
||||
await acquireLock(prisma, project.id, run.id, null);
|
||||
const holder = await currentLockRunId(prisma, project.id);
|
||||
expect(holder).toBe(run.id);
|
||||
|
||||
await releaseLock(prisma, run.id);
|
||||
const after = await currentLockRunId(prisma, project.id);
|
||||
expect(after).toBeNull();
|
||||
});
|
||||
|
||||
it("acquireLock fails when project already locked (exclusivity)", async () => {
|
||||
const project = await prisma.project.create({
|
||||
data: { id: "p-lock-2", name: "Test", workspaceDir: "/tmp/x" },
|
||||
});
|
||||
const run1 = await prisma.agentRun.create({
|
||||
data: { projectId: project.id, entrypoint: "FEISHU", status: "ACTIVE", prompt: "x", model: "m", provider: "mock", metadata: {} },
|
||||
});
|
||||
const run2 = await prisma.agentRun.create({
|
||||
data: { projectId: project.id, entrypoint: "FEISHU", status: "ACTIVE", prompt: "y", model: "m", provider: "mock", metadata: {} },
|
||||
});
|
||||
|
||||
await acquireLock(prisma, project.id, run1.id, null);
|
||||
await expect(acquireLock(prisma, project.id, run2.id, null)).rejects.toThrow();
|
||||
});
|
||||
|
||||
it("currentLockRunId throws when a terminal run holds the lock (WellFormed)", async () => {
|
||||
const project = await prisma.project.create({
|
||||
data: { id: "p-lock-3", name: "Test", workspaceDir: "/tmp/x" },
|
||||
});
|
||||
// Create a run that is already COMPLETED (terminal), then manually insert a lock.
|
||||
const run = await prisma.agentRun.create({
|
||||
data: { projectId: project.id, entrypoint: "FEISHU", status: "COMPLETED", prompt: "x", model: "m", provider: "mock", metadata: {}, finishedAt: new Date() },
|
||||
});
|
||||
await prisma.projectAgentLock.create({
|
||||
data: { projectId: project.id, runId: run.id },
|
||||
});
|
||||
|
||||
// WellFormed invariant: reading a lock held by a terminal run must throw.
|
||||
await expect(currentLockRunId(prisma, project.id)).rejects.toThrow(/lock invariant violated/);
|
||||
});
|
||||
|
||||
it("releaseLock is idempotent", async () => {
|
||||
const project = await prisma.project.create({
|
||||
data: { id: "p-lock-4", name: "Test", workspaceDir: "/tmp/x" },
|
||||
});
|
||||
const run = await prisma.agentRun.create({
|
||||
data: { projectId: project.id, entrypoint: "FEISHU", status: "ACTIVE", prompt: "x", model: "m", provider: "mock", metadata: {} },
|
||||
});
|
||||
|
||||
await acquireLock(prisma, project.id, run.id, null);
|
||||
await releaseLock(prisma, run.id);
|
||||
// Second release is a no-op.
|
||||
await releaseLock(prisma, run.id);
|
||||
expect(await currentLockRunId(prisma, project.id)).toBeNull();
|
||||
});
|
||||
|
||||
it("isTerminal matches spec RunState.Terminal", () => {
|
||||
expect(isTerminal("ACTIVE")).toBe(false);
|
||||
expect(isTerminal("WAITING_FOR_USER")).toBe(false);
|
||||
expect(isTerminal("COMPLETED")).toBe(true);
|
||||
expect(isTerminal("FAILED")).toBe(true);
|
||||
expect(isTerminal("TIMED_OUT")).toBe(true);
|
||||
expect(isTerminal("CANCELED")).toBe(true);
|
||||
});
|
||||
});
|
||||
|
||||
afterAll(async () => {
|
||||
await prisma.$disconnect();
|
||||
});
|
||||
@@ -1,71 +0,0 @@
|
||||
import { describe, it, expect, beforeEach, afterAll } from "vitest";
|
||||
import { prisma, resetDb } from "./helpers.js";
|
||||
import { canTriggerRole } from "../../src/permission.js";
|
||||
|
||||
describe("canTriggerRole (integration, per-role gate)", () => {
|
||||
beforeEach(async () => {
|
||||
await resetDb();
|
||||
});
|
||||
|
||||
afterAll(async () => {
|
||||
await prisma.$disconnect();
|
||||
});
|
||||
|
||||
it("allows when role is unconfigured on the project (back-compat: open)", async () => {
|
||||
const project = await prisma.project.create({
|
||||
data: { id: "p-role-1", name: "T", workspaceDir: "/tmp/x" },
|
||||
});
|
||||
const r = await canTriggerRole(prisma, project.id, "draft", "ou_a");
|
||||
expect(r.allowed).toBe(true);
|
||||
});
|
||||
|
||||
it("allows when principal holds an active grant for the role", async () => {
|
||||
const project = await prisma.project.create({
|
||||
data: { id: "p-role-2", name: "T", workspaceDir: "/tmp/x" },
|
||||
});
|
||||
await prisma.roleTriggerGrant.create({
|
||||
data: { projectId: project.id, roleId: "review", principal: "ou_a" },
|
||||
});
|
||||
const r = await canTriggerRole(prisma, project.id, "review", "ou_a");
|
||||
expect(r.allowed).toBe(true);
|
||||
});
|
||||
|
||||
it("denies when grants exist for the role but principal has none", async () => {
|
||||
const project = await prisma.project.create({
|
||||
data: { id: "p-role-3", name: "T", workspaceDir: "/tmp/x" },
|
||||
});
|
||||
// Someone else has the role; ou_b does not.
|
||||
await prisma.roleTriggerGrant.create({
|
||||
data: { projectId: project.id, roleId: "review", principal: "ou_a" },
|
||||
});
|
||||
const r = await canTriggerRole(prisma, project.id, "review", "ou_b");
|
||||
expect(r.allowed).toBe(false);
|
||||
});
|
||||
|
||||
it("denies when the principal's grant was revoked", async () => {
|
||||
const project = await prisma.project.create({
|
||||
data: { id: "p-role-4", name: "T", workspaceDir: "/tmp/x" },
|
||||
});
|
||||
await prisma.roleTriggerGrant.create({
|
||||
data: { projectId: project.id, roleId: "review", principal: "ou_a", revokedAt: new Date() },
|
||||
});
|
||||
const r = await canTriggerRole(prisma, project.id, "review", "ou_a");
|
||||
expect(r.allowed).toBe(false);
|
||||
});
|
||||
|
||||
it("scopes grants per-project (grant on p1 does not allow on p2)", async () => {
|
||||
const p1 = await prisma.project.create({ data: { id: "p-role-5a", name: "T", workspaceDir: "/tmp/x" } });
|
||||
const p2 = await prisma.project.create({ data: { id: "p-role-5b", name: "T", workspaceDir: "/tmp/x" } });
|
||||
await prisma.roleTriggerGrant.create({
|
||||
data: { projectId: p1.id, roleId: "review", principal: "ou_a" },
|
||||
});
|
||||
// p2 has the role configured for someone else; ou_a has no grant there.
|
||||
await prisma.roleTriggerGrant.create({
|
||||
data: { projectId: p2.id, roleId: "review", principal: "ou_other" },
|
||||
});
|
||||
const onP1 = await canTriggerRole(prisma, p1.id, "review", "ou_a");
|
||||
expect(onP1.allowed).toBe(true);
|
||||
const onP2 = await canTriggerRole(prisma, p2.id, "review", "ou_a");
|
||||
expect(onP2.allowed).toBe(false);
|
||||
});
|
||||
});
|
||||
@@ -1,295 +0,0 @@
|
||||
import { describe, it, expect, beforeEach, afterAll, vi } from "vitest";
|
||||
import { prisma, resetDb, mockFeishuRuntime, createMockModelFactory, seedProject, silentLogger } from "./helpers.js";
|
||||
import { InMemoryModelRegistry } from "../../src/agent/models.js";
|
||||
import { ToolRegistry } from "../../src/agent/tools.js";
|
||||
import { makeTriggerHandler, extractPrompt } from "../../src/feishu/trigger.js";
|
||||
import type { MessageReceiveEvent } from "../../src/feishu/client.js";
|
||||
import type { ModelFactory } from "../../src/agent/runner.js";
|
||||
|
||||
const bot = { key: "@_user_1", id: { open_id: "ou_bot" }, name: "Bot" };
|
||||
|
||||
function makeEvent(chatId: string, text: string, senderOpenId = "ou_test_user", eventId?: string): MessageReceiveEvent {
|
||||
const header = eventId !== undefined ? { event_id: eventId, event_type: "im.message.receive_v1" } : undefined;
|
||||
return {
|
||||
header,
|
||||
message: {
|
||||
message_id: "m_" + Math.random().toString(36).slice(2),
|
||||
chat_id: chatId,
|
||||
chat_type: "group",
|
||||
message_type: "text",
|
||||
content: JSON.stringify({ text }),
|
||||
mentions: [bot],
|
||||
},
|
||||
sender: { sender_id: { open_id: senderOpenId }, sender_type: "user" },
|
||||
};
|
||||
}
|
||||
|
||||
describe("trigger full lifecycle (integration)", () => {
|
||||
let modelFactory: ModelFactory;
|
||||
let tools: ToolRegistry;
|
||||
let models: InMemoryModelRegistry;
|
||||
let rt: ReturnType<typeof mockFeishuRuntime>;
|
||||
|
||||
beforeEach(async () => {
|
||||
await resetDb();
|
||||
modelFactory = createMockModelFactory().modelFactory;
|
||||
tools = new ToolRegistry();
|
||||
models = new InMemoryModelRegistry(
|
||||
[{ id: "mock-model", label: "Mock", toolCapable: true }],
|
||||
[
|
||||
{ id: "draft", label: "草稿", defaultModel: "mock-model", systemPrompt: undefined, tools: undefined },
|
||||
{ id: "review", label: "审校", defaultModel: "mock-model", systemPrompt: undefined, tools: ["read_file"] },
|
||||
],
|
||||
);
|
||||
rt = mockFeishuRuntime();
|
||||
});
|
||||
|
||||
it("creates a run, acquires + releases the lock, sends status card", async () => {
|
||||
await seedProject("proj-1", "chat-1");
|
||||
const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
|
||||
|
||||
await trigger(makeEvent("chat-1", "@_user_1 写教案"), rt);
|
||||
|
||||
// Wait for the async run to complete (fire-and-forget in trigger).
|
||||
await vi.waitFor(async () => {
|
||||
const runs = await prisma.agentRun.findMany();
|
||||
expect(runs).toHaveLength(1);
|
||||
expect(runs[0]?.status).toBe("COMPLETED");
|
||||
});
|
||||
|
||||
// Lock released (no lock row remains).
|
||||
const locks = await prisma.projectAgentLock.findMany();
|
||||
expect(locks).toHaveLength(0);
|
||||
|
||||
// A status card was sent.
|
||||
expect(rt.sentCards.length).toBeGreaterThanOrEqual(1);
|
||||
expect(rt.sentTexts).toContain("已开始处理(role: draft, model: mock-model)。");
|
||||
});
|
||||
|
||||
it("rejects a sender without edit grant (ADR-0004)", async () => {
|
||||
await seedProject("proj-2", "chat-2", { role: "READ" });
|
||||
const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
|
||||
|
||||
await trigger(makeEvent("chat-2", "@_user_1 写教案"), rt);
|
||||
|
||||
expect(rt.sentTexts).toContain("无权限触发。");
|
||||
const runs = await prisma.agentRun.findMany();
|
||||
expect(runs).toHaveLength(0);
|
||||
});
|
||||
|
||||
it("replies busy when project is already locked (ADR-0002)", async () => {
|
||||
await seedProject("proj-3", "chat-3");
|
||||
// Manually create a lock by inserting a run + lock.
|
||||
const existingRun = await prisma.agentRun.create({
|
||||
data: { projectId: "proj-3", entrypoint: "FEISHU", status: "ACTIVE", prompt: "x", model: "m", provider: "mock", metadata: {} },
|
||||
});
|
||||
await prisma.projectAgentLock.create({
|
||||
data: { projectId: "proj-3", runId: existingRun.id },
|
||||
});
|
||||
|
||||
const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
|
||||
await trigger(makeEvent("chat-3", "@_user_1 写教案"), rt);
|
||||
|
||||
expect(rt.sentTexts).toContain("项目正在处理中,请稍候。");
|
||||
// No new run created.
|
||||
const runs = await prisma.agentRun.findMany();
|
||||
expect(runs).toHaveLength(1);
|
||||
});
|
||||
|
||||
it("ignores messages from unbound chats (ADR-0001)", async () => {
|
||||
await seedProject("proj-4", "chat-4");
|
||||
const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
|
||||
|
||||
await trigger(makeEvent("chat-UNKNOWN", "@_user_1 写教案"), rt);
|
||||
|
||||
expect(rt.sentTexts).toHaveLength(0);
|
||||
expect(rt.sentCards).toHaveLength(0);
|
||||
const runs = await prisma.agentRun.findMany();
|
||||
expect(runs).toHaveLength(0);
|
||||
});
|
||||
|
||||
it("ignores messages without @bot mention", async () => {
|
||||
await seedProject("proj-5", "chat-5");
|
||||
const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
|
||||
|
||||
const event: MessageReceiveEvent = {
|
||||
message: {
|
||||
message_id: "m_nobot",
|
||||
chat_id: "chat-5",
|
||||
chat_type: "group",
|
||||
message_type: "text",
|
||||
content: JSON.stringify({ text: "hello no bot" }),
|
||||
mentions: undefined,
|
||||
},
|
||||
sender: { sender_id: { open_id: "ou_test_user" }, sender_type: "user" },
|
||||
};
|
||||
await trigger(event, rt);
|
||||
|
||||
expect(rt.sentTexts).toHaveLength(0);
|
||||
const runs = await prisma.agentRun.findMany();
|
||||
expect(runs).toHaveLength(0);
|
||||
});
|
||||
|
||||
it("/new archives current session (no run created)", async () => {
|
||||
await seedProject("proj-6", "chat-6");
|
||||
const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
|
||||
|
||||
// First @bot creates a session + run.
|
||||
await trigger(makeEvent("chat-6", "@_user_1 写教案"), rt);
|
||||
await vi.waitFor(async () => {
|
||||
const runs = await prisma.agentRun.findMany();
|
||||
expect(runs).toHaveLength(1);
|
||||
expect(runs[0]?.status).toBe("COMPLETED");
|
||||
});
|
||||
|
||||
// /new archives the session.
|
||||
await trigger(makeEvent("chat-6", "@_user_1 /new"), rt);
|
||||
expect(rt.sentTexts).toContain("已开新会话,下次 @bot 将从头开始。");
|
||||
|
||||
const sessions = await prisma.agentSession.findMany();
|
||||
expect(sessions).toHaveLength(1);
|
||||
expect(sessions[0]?.archivedAt).not.toBeNull();
|
||||
// No new run created for /new.
|
||||
expect(await prisma.agentRun.findMany()).toHaveLength(1);
|
||||
});
|
||||
|
||||
it("/resume un-archives the most recent session", async () => {
|
||||
await seedProject("proj-7", "chat-7");
|
||||
const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
|
||||
|
||||
// Create + archive a session via /new.
|
||||
await trigger(makeEvent("chat-7", "@_user_1 写教案"), rt);
|
||||
await vi.waitFor(async () => {
|
||||
expect(await prisma.agentRun.findMany()).toHaveLength(1);
|
||||
});
|
||||
await trigger(makeEvent("chat-7", "@_user_1 /new"), rt);
|
||||
|
||||
// /resume un-archives.
|
||||
await trigger(makeEvent("chat-7", "@_user_1 /resume"), rt);
|
||||
expect(rt.sentTexts).toContain("已恢复上一个会话。");
|
||||
|
||||
const sessions = await prisma.agentSession.findMany();
|
||||
expect(sessions).toHaveLength(1);
|
||||
expect(sessions[0]?.archivedAt).toBeNull();
|
||||
});
|
||||
|
||||
it("/reset archives current session", async () => {
|
||||
await seedProject("proj-8", "chat-8");
|
||||
const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
|
||||
|
||||
await trigger(makeEvent("chat-8", "@_user_1 写教案"), rt);
|
||||
await vi.waitFor(async () => {
|
||||
const runs = await prisma.agentRun.findMany();
|
||||
expect(runs).toHaveLength(1);
|
||||
expect(runs[0]?.status).toBe("COMPLETED");
|
||||
});
|
||||
|
||||
await trigger(makeEvent("chat-8", "@_user_1 /reset"), rt);
|
||||
expect(rt.sentTexts).toContain("已重置,下次 @bot 将从头开始。");
|
||||
|
||||
const sessions = await prisma.agentSession.findMany();
|
||||
expect(sessions).toHaveLength(1);
|
||||
expect(sessions[0]?.archivedAt).not.toBeNull();
|
||||
});
|
||||
|
||||
it("unknown slash command falls through to agent", async () => {
|
||||
await seedProject("proj-9", "chat-9");
|
||||
const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
|
||||
|
||||
await trigger(makeEvent("chat-9", "@_user_1 /unknown"), rt);
|
||||
// Should create a run (falls through as a normal prompt).
|
||||
await vi.waitFor(async () => {
|
||||
const runs = await prisma.agentRun.findMany();
|
||||
expect(runs).toHaveLength(1);
|
||||
expect(runs[0]?.prompt).toBe("/unknown");
|
||||
});
|
||||
});
|
||||
|
||||
it("denies /review when sender has no role grant (per-role gate)", async () => {
|
||||
await seedProject("proj-10", "chat-10");
|
||||
// Someone else holds review; ou_test_user does not.
|
||||
await prisma.roleTriggerGrant.create({
|
||||
data: { projectId: "proj-10", roleId: "review", principal: "ou_other" },
|
||||
});
|
||||
const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
|
||||
|
||||
await trigger(makeEvent("chat-10", "@_user_1 /review 看看这节"), rt);
|
||||
|
||||
expect(rt.sentTexts).toContain("无权限使用角色 review。");
|
||||
const runs = await prisma.agentRun.findMany();
|
||||
expect(runs).toHaveLength(0);
|
||||
});
|
||||
|
||||
it("allows /review when sender holds the role grant", async () => {
|
||||
await seedProject("proj-11", "chat-11");
|
||||
await prisma.roleTriggerGrant.create({
|
||||
data: { projectId: "proj-11", roleId: "review", principal: "ou_test_user" },
|
||||
});
|
||||
const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
|
||||
|
||||
await trigger(makeEvent("chat-11", "@_user_1 /review 看看这节"), rt);
|
||||
|
||||
await vi.waitFor(async () => {
|
||||
const runs = await prisma.agentRun.findMany();
|
||||
expect(runs).toHaveLength(1);
|
||||
expect(runs[0]?.status).toBe("COMPLETED");
|
||||
expect(runs[0]?.metadata).toMatchObject({ roleId: "review" });
|
||||
});
|
||||
});
|
||||
|
||||
it("extractRole: /draft sets roleId=draft, strips command from prompt", async () => {
|
||||
await seedProject("proj-12", "chat-12");
|
||||
const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
|
||||
|
||||
await trigger(makeEvent("chat-12", "@_user_1 /draft 写第三单元"), rt);
|
||||
|
||||
await vi.waitFor(async () => {
|
||||
const runs = await prisma.agentRun.findMany();
|
||||
expect(runs).toHaveLength(1);
|
||||
expect(runs[0]?.prompt).toBe("写第三单元");
|
||||
expect(runs[0]?.metadata).toMatchObject({ roleId: "draft" });
|
||||
});
|
||||
});
|
||||
|
||||
it("dedups a redelivered event by event_id (no second run)", async () => {
|
||||
await seedProject("proj-13", "chat-13");
|
||||
const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
|
||||
|
||||
// First delivery: processes normally.
|
||||
await trigger(makeEvent("chat-13", "@_user_1 写教案", "ou_test_user", "evt-dedup-1"), rt);
|
||||
await vi.waitFor(async () => {
|
||||
const runs = await prisma.agentRun.findMany();
|
||||
expect(runs).toHaveLength(1);
|
||||
expect(runs[0]?.status).toBe("COMPLETED");
|
||||
});
|
||||
|
||||
// Redelivery of the same event_id: must not create a second run.
|
||||
await trigger(makeEvent("chat-13", "@_user_1 写教案", "ou_test_user", "evt-dedup-1"), rt);
|
||||
const runs2 = await prisma.agentRun.findMany();
|
||||
expect(runs2).toHaveLength(1);
|
||||
|
||||
// Only one event receipt row.
|
||||
const receipts = await prisma.feishuEventReceipt.findMany();
|
||||
expect(receipts).toHaveLength(1);
|
||||
expect(receipts[0]?.eventId).toBe("evt-dedup-1");
|
||||
});
|
||||
|
||||
it("writes audit entries across the run lifecycle", async () => {
|
||||
await seedProject("proj-14", "chat-14");
|
||||
const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
|
||||
|
||||
await trigger(makeEvent("chat-14", "@_user_1 写教案"), rt);
|
||||
await vi.waitFor(async () => {
|
||||
const audit = await prisma.auditEntry.findMany();
|
||||
expect(audit.length).toBeGreaterThanOrEqual(2);
|
||||
});
|
||||
|
||||
const audit = await prisma.auditEntry.findMany({ orderBy: { createdAt: "asc" } });
|
||||
expect(audit.some((a) => a.action === "run.created")).toBe(true);
|
||||
expect(audit.some((a) => a.action === "run.finished")).toBe(true);
|
||||
});
|
||||
});
|
||||
|
||||
afterAll(async () => {
|
||||
await prisma.$disconnect();
|
||||
});
|
||||
@@ -1,73 +0,0 @@
|
||||
import { describe, expect, it, vi } from "vitest";
|
||||
import type { PrismaClient } from "@prisma/client";
|
||||
import { writeAudit } from "../../src/audit.js";
|
||||
|
||||
/// Minimal mock: only the surface `writeAudit` touches. Cast through unknown
|
||||
/// so we don't have to implement the rest of the PrismaClient surface — this
|
||||
/// is a unit test, not a DB test.
|
||||
interface AuditEntryMock {
|
||||
create: ReturnType<typeof vi.fn>;
|
||||
}
|
||||
function mockPrisma(): PrismaClient & { auditEntry: AuditEntryMock } {
|
||||
return { auditEntry: { create: vi.fn() } } as unknown as PrismaClient & {
|
||||
auditEntry: AuditEntryMock;
|
||||
};
|
||||
}
|
||||
|
||||
describe("writeAudit (A-8 audit write path)", () => {
|
||||
it("creates a row with all fields set", async () => {
|
||||
const prisma = mockPrisma();
|
||||
prisma.auditEntry.create.mockResolvedValue({ id: "aud-1" });
|
||||
|
||||
await writeAudit(prisma, {
|
||||
runId: "run-1",
|
||||
projectId: "proj-1",
|
||||
actorUserId: "user-1",
|
||||
action: "run.triggered",
|
||||
metadata: { source: "feishu" },
|
||||
});
|
||||
|
||||
expect(prisma.auditEntry.create).toHaveBeenCalledTimes(1);
|
||||
expect(prisma.auditEntry.create).toHaveBeenCalledWith({
|
||||
data: {
|
||||
runId: "run-1",
|
||||
projectId: "proj-1",
|
||||
actorUserId: "user-1",
|
||||
action: "run.triggered",
|
||||
metadata: { source: "feishu" },
|
||||
},
|
||||
});
|
||||
});
|
||||
|
||||
it("creates a row with only required fields (action + metadata)", async () => {
|
||||
const prisma = mockPrisma();
|
||||
prisma.auditEntry.create.mockResolvedValue({ id: "aud-2" });
|
||||
|
||||
await writeAudit(prisma, {
|
||||
action: "permission.denied",
|
||||
metadata: { reason: "no-edit-role" },
|
||||
});
|
||||
|
||||
expect(prisma.auditEntry.create).toHaveBeenCalledTimes(1);
|
||||
expect(prisma.auditEntry.create).toHaveBeenCalledWith({
|
||||
data: {
|
||||
action: "permission.denied",
|
||||
metadata: { reason: "no-edit-role" },
|
||||
},
|
||||
});
|
||||
});
|
||||
|
||||
it("swallows a prisma error (best-effort, must not throw)", async () => {
|
||||
const prisma = mockPrisma();
|
||||
prisma.auditEntry.create.mockRejectedValue(new Error("db down"));
|
||||
|
||||
// Must not throw — audit is observability, not control.
|
||||
await expect(
|
||||
writeAudit(prisma, {
|
||||
action: "run.triggered",
|
||||
metadata: {},
|
||||
}),
|
||||
).resolves.toBeUndefined();
|
||||
expect(prisma.auditEntry.create).toHaveBeenCalledTimes(1);
|
||||
});
|
||||
});
|
||||
@@ -1,16 +0,0 @@
|
||||
import { describe, it, expect } from "vitest";
|
||||
import { roleGrantsEdit } from "../../src/permission.js";
|
||||
|
||||
describe("roleGrantsEdit (ADR-0004 monotonicity)", () => {
|
||||
it("READ does not grant edit", () => {
|
||||
expect(roleGrantsEdit("READ")).toBe(false);
|
||||
});
|
||||
|
||||
it("EDIT grants edit", () => {
|
||||
expect(roleGrantsEdit("EDIT")).toBe(true);
|
||||
});
|
||||
|
||||
it("MANAGE grants edit (manage ⊇ edit, spec can_mono)", () => {
|
||||
expect(roleGrantsEdit("MANAGE")).toBe(true);
|
||||
});
|
||||
});
|
||||
@@ -1,75 +0,0 @@
|
||||
import { describe, it, expect } from "vitest";
|
||||
import { extractPrompt } from "../../src/feishu/trigger.js";
|
||||
import type { MessageReceiveEvent } from "../../src/feishu/client.js";
|
||||
|
||||
const bot = { key: "@_user_1", id: { open_id: "ou_bot" }, name: "Bot" };
|
||||
|
||||
function msg(text: string, mentions: typeof bot[] | undefined = [bot]): MessageReceiveEvent["message"] {
|
||||
return {
|
||||
message_id: "m",
|
||||
chat_id: "c",
|
||||
chat_type: "group",
|
||||
message_type: "text",
|
||||
content: JSON.stringify({ text }),
|
||||
mentions,
|
||||
};
|
||||
}
|
||||
|
||||
describe("extractPrompt (@bot mention parsing)", () => {
|
||||
it("extracts the prompt after @bot", () => {
|
||||
expect(extractPrompt(msg("@_user_1 帮我写教案"))).toBe("帮我写教案");
|
||||
});
|
||||
|
||||
it("strips multiple mentions", () => {
|
||||
const other = { key: "@_user_2", id: { open_id: "ou_other" }, name: "Other" };
|
||||
expect(extractPrompt(msg("@_user_1 @_user_2 检查例题2", [bot, other]))).toBe("检查例题2");
|
||||
});
|
||||
|
||||
it("returns null when only @bot with no prompt", () => {
|
||||
expect(extractPrompt(msg("@_user_1"))).toBeNull();
|
||||
});
|
||||
|
||||
it("returns null when @bot followed by whitespace only", () => {
|
||||
expect(extractPrompt(msg("@_user_1 "))).toBeNull();
|
||||
});
|
||||
it("returns null when no mentions", () => {
|
||||
const m: MessageReceiveEvent["message"] = {
|
||||
message_id: "m", chat_id: "c", chat_type: "group",
|
||||
message_type: "text",
|
||||
content: JSON.stringify({ text: "hello" }),
|
||||
mentions: undefined,
|
||||
};
|
||||
expect(extractPrompt(m)).toBeNull();
|
||||
});
|
||||
|
||||
it("returns null for non-text message_type (content still parseable)", () => {
|
||||
const m = msg("{}", [bot]);
|
||||
// message_type check is the caller's job; extractPrompt only parses content.
|
||||
// But with empty text it returns null.
|
||||
expect(extractPrompt({ ...m, content: JSON.stringify({ text: "" }) })).toBeNull();
|
||||
});
|
||||
|
||||
it("returns null when content is not valid JSON", () => {
|
||||
const m: MessageReceiveEvent["message"] = {
|
||||
message_id: "m",
|
||||
chat_id: "c",
|
||||
chat_type: "group",
|
||||
message_type: "text",
|
||||
content: "not json",
|
||||
mentions: [bot],
|
||||
};
|
||||
expect(extractPrompt(m)).toBeNull();
|
||||
});
|
||||
|
||||
it("returns null when JSON has no text field", () => {
|
||||
const m: MessageReceiveEvent["message"] = {
|
||||
message_id: "m",
|
||||
chat_id: "c",
|
||||
chat_type: "group",
|
||||
message_type: "text",
|
||||
content: JSON.stringify({ foo: "bar" }),
|
||||
mentions: [bot],
|
||||
};
|
||||
expect(extractPrompt(m)).toBeNull();
|
||||
});
|
||||
});
|
||||
@@ -1,39 +0,0 @@
|
||||
import { describe, expect, it } from "vitest";
|
||||
import { mkdtemp, rm, writeFile } from "node:fs/promises";
|
||||
import { tmpdir } from "node:os";
|
||||
import { join } from "node:path";
|
||||
import { runAgent } from "../../src/agent/runner.js";
|
||||
import { ToolRegistry } from "../../src/agent/tools.js";
|
||||
import { readFileTool } from "../../src/agent/workspace.js";
|
||||
import { createMockModelFactory } from "../integration/helpers.js";
|
||||
|
||||
describe("runAgent with AI SDK tool loop", () => {
|
||||
it("executes SDK tools and returns the final assistant response", async () => {
|
||||
const ws = await mkdtemp(join(tmpdir(), "hub-runner-"));
|
||||
try {
|
||||
await writeFile(join(ws, "lesson.txt"), "hello lesson", "utf8");
|
||||
const tools = new ToolRegistry();
|
||||
tools.register("read_file", readFileTool);
|
||||
const { modelFactory, models } = createMockModelFactory([
|
||||
{
|
||||
toolCalls: [{ toolCallId: "call-1", toolName: "read_file", input: { path: "lesson.txt" } }],
|
||||
},
|
||||
{ text: "done", finishReason: "stop" },
|
||||
]);
|
||||
|
||||
const result = await runAgent(modelFactory, tools, {
|
||||
prompt: "read lesson.txt",
|
||||
model: "mock-model",
|
||||
project: { projectId: "p", boundChatId: "c", workspaceDir: ws },
|
||||
systemPrompt: "system",
|
||||
maxIterations: 5,
|
||||
});
|
||||
|
||||
expect(result.status).toBe("completed");
|
||||
expect(result.messages.at(-1)).toMatchObject({ role: "assistant" });
|
||||
expect(models.get("mock-model")?.calls).toHaveLength(2);
|
||||
} finally {
|
||||
await rm(ws, { recursive: true, force: true });
|
||||
}
|
||||
});
|
||||
});
|
||||
@@ -1,60 +0,0 @@
|
||||
import { describe, it, expect, beforeEach, afterEach } from "vitest";
|
||||
import { mkdtemp, rm, readFile, writeFile } from "node:fs/promises";
|
||||
import { tmpdir } from "node:os";
|
||||
import { join } from "node:path";
|
||||
import { readTranscript, appendTranscript, transcriptPath, TRANSCRIPT_DIR } from "../../src/agent/transcript.js";
|
||||
import type { ModelMessage } from "ai";
|
||||
|
||||
const sample: ModelMessage = { role: "user", content: "hello" };
|
||||
const reply: ModelMessage = { role: "assistant", content: "hi" };
|
||||
|
||||
describe("transcript JSONL", () => {
|
||||
let dir: string;
|
||||
let path: string;
|
||||
|
||||
beforeEach(async () => {
|
||||
dir = await mkdtemp(join(tmpdir(), "hub-transcript-"));
|
||||
path = join(dir, "session.jsonl");
|
||||
});
|
||||
afterEach(async () => {
|
||||
await rm(dir, { recursive: true, force: true });
|
||||
});
|
||||
|
||||
it("readTranscript returns empty array for nonexistent file", async () => {
|
||||
expect(await readTranscript(path)).toEqual([]);
|
||||
});
|
||||
|
||||
it("appendTranscript creates parent dirs and writes JSONL", async () => {
|
||||
await appendTranscript(path, [sample]);
|
||||
const content = await readFile(path, "utf8");
|
||||
expect(content.trim()).toBe(JSON.stringify(sample));
|
||||
});
|
||||
|
||||
it("readTranscript reads back appended messages", async () => {
|
||||
await appendTranscript(path, [sample, reply]);
|
||||
const messages = await readTranscript(path);
|
||||
expect(messages).toHaveLength(2);
|
||||
expect(messages[0]).toEqual(sample);
|
||||
expect(messages[1]).toEqual(reply);
|
||||
});
|
||||
|
||||
it("multiple appends accumulate", async () => {
|
||||
await appendTranscript(path, [sample]);
|
||||
await appendTranscript(path, [reply]);
|
||||
const messages = await readTranscript(path);
|
||||
expect(messages).toHaveLength(2);
|
||||
});
|
||||
|
||||
it("skips corrupt lines (partial write recovery)", async () => {
|
||||
await appendTranscript(path, [sample]);
|
||||
// Append a corrupt line (simulating a crash mid-write).
|
||||
await writeFile(path, '{"broken json\n', { flag: "a" });
|
||||
const messages = await readTranscript(path);
|
||||
expect(messages).toHaveLength(1); // only the valid line
|
||||
});
|
||||
|
||||
it("transcriptPath builds the expected path", () => {
|
||||
const p = transcriptPath("/ws", "sess-1");
|
||||
expect(p).toBe(join("/ws", TRANSCRIPT_DIR, "sess-1.jsonl"));
|
||||
});
|
||||
});
|
||||
@@ -1,88 +0,0 @@
|
||||
import { describe, it, expect, beforeEach } from "vitest";
|
||||
import { mkdtemp, writeFile, mkdir } from "node:fs/promises";
|
||||
import { tmpdir } from "node:os";
|
||||
import { join } from "node:path";
|
||||
import { ToolRegistry, type ToolContext } from "../../src/agent/tools.js";
|
||||
import { readFileTool, writeFileTool, listFilesTool, PathEscape } from "../../src/agent/workspace.js";
|
||||
|
||||
describe("workspace path confinement", () => {
|
||||
let ws: string;
|
||||
let tools: ToolRegistry;
|
||||
|
||||
beforeEach(async () => {
|
||||
ws = await mkdtemp(join(tmpdir(), "hub-unit-"));
|
||||
tools = new ToolRegistry();
|
||||
tools.register("read_file", readFileTool);
|
||||
tools.register("write_file", writeFileTool);
|
||||
tools.register("list_files", listFilesTool);
|
||||
await mkdir(join(ws, "sub"));
|
||||
await writeFile(join(ws, "a.txt"), "hello");
|
||||
await writeFile(join(ws, "sub", "b.txt"), "world");
|
||||
});
|
||||
|
||||
const ctx = () => ({ runId: "r", projectId: "p", boundChatId: "c", workspaceDir: ws });
|
||||
|
||||
it("reads a file inside the workspace", async () => {
|
||||
expect(await executeTool(tools, "read_file", { path: "a.txt" }, ctx())).toBe("hello");
|
||||
});
|
||||
|
||||
it("reads nested files", async () => {
|
||||
expect(await executeTool(tools, "read_file", { path: "sub/b.txt" }, ctx())).toBe("world");
|
||||
});
|
||||
|
||||
it("rejects .. escapes as error JSON, not a throw", async () => {
|
||||
const out = await executeTool(tools, "read_file", { path: "../../etc/passwd" }, ctx());
|
||||
expect((JSON.parse(out) as { error: string }).error).toContain("escapes workspace");
|
||||
});
|
||||
|
||||
it("rejects absolute paths outside the workspace", async () => {
|
||||
const out = await executeTool(tools, "read_file", { path: "/etc/passwd" }, ctx());
|
||||
expect((JSON.parse(out) as { error: string }).error).toContain("escapes workspace");
|
||||
});
|
||||
|
||||
it("writes a file and reads it back", async () => {
|
||||
await executeTool(tools, "write_file", { path: "sub/c.txt", content: "new" }, ctx());
|
||||
expect(await executeTool(tools, "read_file", { path: "sub/c.txt" }, ctx())).toBe("new");
|
||||
});
|
||||
|
||||
it("creates parent dirs on write", async () => {
|
||||
await executeTool(tools, "write_file", { path: "deep/nested/d.txt", content: "x" }, ctx());
|
||||
expect(await executeTool(tools, "read_file", { path: "deep/nested/d.txt" }, ctx())).toBe("x");
|
||||
});
|
||||
|
||||
it("lists the workspace root", async () => {
|
||||
const out = await executeTool(tools, "list_files", {}, ctx());
|
||||
const entries = JSON.parse(out) as Array<{ name: string; kind: string }>;
|
||||
expect(entries).toContainEqual({ name: "a.txt", kind: "file" });
|
||||
expect(entries).toContainEqual({ name: "sub", kind: "dir" });
|
||||
});
|
||||
|
||||
it("lists a subdirectory", async () => {
|
||||
const out = await executeTool(tools, "list_files", { path: "sub" }, ctx());
|
||||
const entries = JSON.parse(out) as Array<{ name: string; kind: string }>;
|
||||
expect(entries).toContainEqual({ name: "b.txt", kind: "file" });
|
||||
});
|
||||
|
||||
it("PathEscape is an Error subclass", () => {
|
||||
expect(new PathEscape("../x", "/ws")).toBeInstanceOf(Error);
|
||||
expect(new PathEscape("../x", "/ws").name).toBe("PathEscape");
|
||||
});
|
||||
|
||||
it("read of nonexistent file returns error JSON", async () => {
|
||||
const out = await executeTool(tools, "read_file", { path: "nope.txt" }, ctx());
|
||||
expect((JSON.parse(out) as { error: string }).error).toBeTruthy();
|
||||
});
|
||||
|
||||
it("write with .. escape returns error JSON", async () => {
|
||||
const out = await executeTool(tools, "write_file", { path: "../escape.txt", content: "x" }, ctx());
|
||||
expect((JSON.parse(out) as { error: string }).error).toContain("escapes workspace");
|
||||
});
|
||||
});
|
||||
|
||||
async function executeTool(tools: ToolRegistry, name: string, args: unknown, ctx: ToolContext): Promise<string> {
|
||||
const def = tools.build(ctx)[name];
|
||||
if (def?.execute === undefined) {
|
||||
throw new Error(`missing executable tool: ${name}`);
|
||||
}
|
||||
return def.execute(args, { toolCallId: "call", messages: [], context: undefined }) as Promise<string>;
|
||||
}
|
||||
@@ -1,22 +0,0 @@
|
||||
{
|
||||
"compilerOptions": {
|
||||
"target": "ES2022",
|
||||
"lib": ["ES2023"],
|
||||
"module": "NodeNext",
|
||||
"moduleResolution": "NodeNext",
|
||||
"rootDir": "src",
|
||||
"outDir": "dist",
|
||||
"strict": true,
|
||||
"noUncheckedIndexedAccess": true,
|
||||
"exactOptionalPropertyTypes": true,
|
||||
"noImplicitOverride": true,
|
||||
"noFallthroughCasesInSwitch": true,
|
||||
"verbatimModuleSyntax": true,
|
||||
"skipLibCheck": true,
|
||||
"esModuleInterop": true,
|
||||
"forceConsistentCasingInFileNames": true,
|
||||
"declaration": false,
|
||||
"sourceMap": true
|
||||
},
|
||||
"include": ["src/**/*.ts"]
|
||||
}
|
||||
@@ -1,12 +0,0 @@
|
||||
import { defineConfig } from "vitest/config";
|
||||
|
||||
export default defineConfig({
|
||||
test: {
|
||||
include: ["test/**/*.test.ts"],
|
||||
// Integration tests share one DB; run files sequentially to avoid
|
||||
// concurrent truncate/insert races. Unit tests are fast either way.
|
||||
pool: "forks",
|
||||
fileParallelism: false,
|
||||
env: { NODE_ENV: "test" },
|
||||
},
|
||||
});
|
||||
+54
-35
@@ -1,55 +1,74 @@
|
||||
# spec —— Lean 语义母本
|
||||
# spec —— 语义契约
|
||||
|
||||
这是本 monorepo 的**契约**:产品各部件语义的上游参照,用 Lean 编写。它的定位与约束见仓库根 `README.md` 的"宪法"5 条——本文件只讲**怎么往这份契约里写东西**。
|
||||
## 这个项目在解决什么
|
||||
|
||||
## 现状
|
||||
教研产出现在是一摞一次性的文档:写完就躺着,改一次要同步很多地方,没法校验、
|
||||
没法复用、没法追溯。这个项目想把教研产出变成可校验、可复用、能派生多种成品
|
||||
(讲义、教案、课件、归档)的工程化文件。
|
||||
|
||||
刚初始化的 Lean 工程(`lake init`),目前只有占位内容(`Spec/Basic.lean`)。实质领域内容(System 平台层、Courseware 产品层)将逐个概念加入,每个都遵循下面的规范。
|
||||
但光有工程文件还不够。它要变成一个能卖钱的产品,还得:
|
||||
|
||||
## 构建
|
||||
- 工程文件这种形式,正好适合现在大热的 LLM assistant 来改,从而提效;
|
||||
- 但 LLM 判不了一节课合不合法(它不能真去跑 typst 编译器、不能可靠地断言数据合不合
|
||||
schema),所以产品里还有一个 rule-based checker:它真跑工具、给确定性的诊断,补上
|
||||
LLM 判不了的这块。LLM 提效 + checker 兜底,两者一起才是完整的产品闭环。
|
||||
- 加上一些提升体验的小功能:飞书/企业微信集成、自动化提醒之类;
|
||||
- 如果要做 SaaS,还要有基本的管理概念:权限、LLM API 的配置和用量、费用等。
|
||||
|
||||
```sh
|
||||
cd spec
|
||||
lake build
|
||||
```
|
||||
工程文件是起点,不是终点。
|
||||
|
||||
工具链锁定在 `lean-toolchain`(`leanprover/lean4:v4.31.0`)。无外部依赖——Mathlib / Batteries 等留待第一个真正需要它的定理出现时再引入(依赖碰到再加)。
|
||||
## spec 是什么
|
||||
|
||||
## 写作规范
|
||||
spec/ 是产品语义的契约,用 Lean 写。它定义产品各部件"是什么意思"。
|
||||
|
||||
### 双半契约:prose + type
|
||||
- 它是开发者和 coding assistant 共同的语义依据:两边对某个东西的理解,以这里为准。
|
||||
- 它不进产品运行时。运行时真正做校验的那个东西用什么技术实现,还没定;但它的语义,
|
||||
先在这里固定下来。
|
||||
- 它精确、自洽,机器能校验它内部结构没有漏洞。它不保证实现一定符合它——
|
||||
实现和它是否一致,没有自动检查,要靠人工或 coding assistant 不定期(或每次改动后)核对。
|
||||
|
||||
每个 top-level 声明**必须**带 `/-- … -/` doc 注释,用自然语言陈述其语义意图。两半缺一不可:
|
||||
## 人机怎么一起干活
|
||||
|
||||
- **prose 半**给人读——说清"这在领域里是什么、为什么"。
|
||||
- **type 半**给机器读、给 type checker 把关——保证结构无洞。
|
||||
- 凭语义,不凭经验。这个领域新,coding assistant 在这里没有可靠的既有经验,
|
||||
所以语义以 spec 的注释为准,不要凭训练先验臆测。
|
||||
- 契约没写的,就是不存在的。遇到没定的点,提出来让开发者定,不要替它选答案。
|
||||
- 改了实现或 spec 之后,两边是否还对得上,要核对一下;这一致性没有自动闸门。
|
||||
|
||||
agent 不得用预训练先验脑补本领域(领域很新,无先验);prose 是 agent 理解语义的唯一权威来源。
|
||||
## 怎么往 spec 里写
|
||||
|
||||
### 标签分类法
|
||||
### 一条东西要不要进 spec
|
||||
|
||||
在 doc 注释里用以下标签标注每条语义的状态:
|
||||
不写它,开发者和 coding assistant 会不会各自做出不同假设?会,就进;不会
|
||||
(显然的事、纯基础设施、普通 CRUD 字段),就不进。
|
||||
|
||||
- **`PINNED`** —— 已解决的分歧点,契约在此处权威,双方据此对齐。
|
||||
- **`OPEN`** —— 故意未规定。双方均**不得假设**其解;实现遇到时必须 surface 出来讨论,而不是擅自决定。
|
||||
- **`ADR-NNNN`** —— 链接到根 `docs/adr/` 下的对应决策记录(如 `ADR-0002`),交代该语义的决策出处。
|
||||
### 进了之后,钉到多细
|
||||
|
||||
### 分歧点测试(写之前先过一遍)
|
||||
- 现在想清楚的,用 Lean 固定(声明、类型、关系)。
|
||||
- 没想清楚的,两三句话 prose 占位,标 `OPEN`。等讨论或业务反馈后再细化,
|
||||
细化结果可以再用 Lean 固定。
|
||||
- 不在 Lean 里验证实现真的做了这些事。spec 只讲"要做什么、判什么";实现有没有真做,
|
||||
不形式化证明。
|
||||
- 形式化定理:不用写;写了不是坏事,但现在很少有能写的定理。定理本身得是产品语义,
|
||||
不是"实现该满足的性质"。
|
||||
|
||||
新增任何概念前,先问:**"不写明,开发者与 agent 会不会各自做出不同假设?"**
|
||||
### 写的时候
|
||||
|
||||
- 会 → 它是分歧点,入契约。
|
||||
- 不会(显然的东西 / 纯 plumbing / 普通 CRUD 字段)→ 不入。
|
||||
|
||||
详见根 README 宪法第 5 条。
|
||||
|
||||
### 不用 `sorry`
|
||||
|
||||
无法陈述清楚的东西,用 `OPEN` 在 prose 里标注,而**不是**用 `sorry` 留一个假装成立的定理。`sorry` 会让 `lake build` 仍然变绿,却在契约里埋一个谎——这与"契约自包含、无洞"直接冲突。
|
||||
- 每个顶层声明要带 doc 注释,用 `/-- ... -/` 写自然语言,说清这在领域里是什么、为什么。
|
||||
注释是语义的依据,Lean 类型保证结构,两者缺一不可。
|
||||
- 在注释里标这条语义的状态:
|
||||
- `PINNED`:已定,契约在此处权威。
|
||||
- `OPEN`:故意没定。不要假设它的解,遇到要提出来讨论。
|
||||
- `ADR-NNNN`:指向 `docs/adr/` 下的决策记录。
|
||||
- 不用 `sorry`。没想清楚的,用 `OPEN` 标在注释里,不要用 `sorry` 假装成立——
|
||||
那会让构建通过,却在契约里埋一个谎。
|
||||
- 不复述文件系统上能直接看到的东西(目录结构、文件名)。文件系统应当自描述,文档讲 context。
|
||||
- 不写变更史(进 git/ADR)。不搬 ADR 内部黑话,要表达就直说。
|
||||
不为设计选择辩护("刻意用 X 而非 Y"),只说是什么。
|
||||
- "为什么"的背景考据(如某工具的内部机制)不进 spec,指向 ADR;但产品行为和设计模式要钉。
|
||||
|
||||
### 命名
|
||||
|
||||
- **模块 / 命名空间**:PascalCase,对应分层,如 `Spec.System.Run`、`Spec.Courseware.Validity`。
|
||||
- **类型**:PascalCase。
|
||||
- **谓词 / `Prop`**:用意图清晰的命名,如 `Legal…`、`ValidTransition`、`Can…`。
|
||||
- **文件粒度**:原则上"一个带独立不变式的概念一个文件"。
|
||||
- 模块/命名空间:PascalCase,按分层,如 `Spec.System.Run`。
|
||||
- 类型:PascalCase。
|
||||
- 谓词(`Prop`):用意图清楚的词,如 `Legal…`、`ValidTransition`、`Can…`。
|
||||
- 文件粒度:一个带独立不变式的概念一个文件。
|
||||
|
||||
@@ -6,16 +6,5 @@ import Spec.Courseware.Open
|
||||
/-!
|
||||
# Courseware —— 产品层契约(课程工程文件)
|
||||
|
||||
护城河:课程"工程文件"的语义母本与合法性规则。决策出处 ADR-0005..0016。按四组组织:
|
||||
|
||||
- **`Model`** —— 工程文件的内容模型:基元 `Primitives`、富内容 `RichContent`、原子
|
||||
单位 `Element`、单节课 `Lesson`(element 的有序序列)。
|
||||
- **`Export`** —— export target = artifact + 有序 typed steps:产物 ADT `Artifact`
|
||||
(`singleFile` / `fileTree`),build 规格 `TargetSpec`(artifact + steps + 覆盖声明
|
||||
`covers`)与 `RenderConfig`。
|
||||
- **`Check`** —— checker 语义:`Severity` + 6 类诊断 + **合法 lesson = 无 error 级
|
||||
诊断**(模型外设施诊断以抽象谓词 + `Oracle` 表示);检查管线的 5 阶段、序、compile
|
||||
门控。
|
||||
- **`Open`** —— 留白骨架(核心关系 OPEN,已 surface 不臆造):题库 `QuestionBank`、
|
||||
课程编排 `Course`。
|
||||
课程"工程文件"的语义母本与合法性规则。决策出处 ADR-0005..0016。
|
||||
-/
|
||||
|
||||
@@ -2,7 +2,7 @@ import Spec.Courseware.Check.Diagnostic
|
||||
import Spec.Courseware.Check.Pipeline
|
||||
|
||||
/-!
|
||||
# Courseware.Check —— checker 语义
|
||||
# Courseware.Check —— 产品 checker 语义
|
||||
|
||||
诊断分类与合法 lesson(`Diagnostic`)、检查管线的阶段与序(`Pipeline`)。决策出处
|
||||
ADR-0010。
|
||||
|
||||
@@ -2,30 +2,39 @@ import Spec.Courseware.Model.Lesson
|
||||
import Spec.Courseware.Export.Render
|
||||
|
||||
/-!
|
||||
# Diagnostic —— checker 诊断:分类、严重级别、合法 lesson
|
||||
# Diagnostic —— 产品 checker 的诊断
|
||||
|
||||
产品里"站在 Lean 位置"的 rule-based checker,语义在此沉淀(ADR-0010,经 ADR-0012
|
||||
修订)。它对 lesson 提诊断,每条有**分类**(`DiagKind`)与**严重级别**(`Severity`)。
|
||||
本模块:钉级别类型(二分);钉 7 类诊断各自的含义与级别,并把"**合法 lesson = 无
|
||||
error 级诊断**"建成判定(ADR-0005 deferred 的"完整合法判定"的回填);对**模型外设施**
|
||||
型诊断(typst 编过否、数据合 schema 否)用**抽象谓词 + `Oracle` 实现边界**表示——契约
|
||||
说"存在这条诊断、什么意思、什么级别",真值由实现提供,不在 Lean 内计算(不内嵌 typst
|
||||
编译器)。引用解析(`@ref`、相对 import)不另设诊断:它们都是 typst 编译期失败,归
|
||||
`typstCompile`(ADR-0012)。版本契约诊断 `cphVersionMismatch`(ADR-0016)是第 7 类。
|
||||
这个 codebase 是要拿去卖的产品。LLM 辅助操作提效是它的核心卖点之一——但 LLM 判不了
|
||||
一节课合不合法:它不能真的去跑 typst 编译器、不能可靠地断言一段数据合不合 schema、
|
||||
也不能可靠地检查文件齐不齐。所以产品里有一个 rule-based checker 来做这件事:它真跑
|
||||
工具、给确定性的诊断,补上 LLM 判不了的这块。这个 checker 的语义在这里(ADR-0010,
|
||||
经 ADR-0012、ADR-0016 修订)。它对 lesson 提诊断,每条有一个分类(`DiagKind`)和一
|
||||
个严重级别(`Severity`)。
|
||||
|
||||
注意区分两个"检查":这里的 checker 是**产品功能**——用户把教研工程文件喂给 `cph`,
|
||||
检查这个工程文件合不合法。它和"开发时 spec 与实现是否一致"是两回事,后者没有自动
|
||||
闸门,靠核对。
|
||||
|
||||
本模块钉三件事:严重级别二分;7 类诊断各自的含义和级别;"合法 lesson = 无 error 级
|
||||
诊断"这条判定。其中有些诊断是 LLM 判不了、得 checker 真跑工具才能判的(typst 编不编
|
||||
得过、数据合不合 schema、content 文件齐不齐)——这些用抽象谓词加 `Oracle` 表示:契约
|
||||
说"存在这条诊断、什么意思、什么级别",真值由 checker 给(契约不在 Lean 里内嵌 typst
|
||||
编译器去算)。引用解析(`@ref`、相对 import)不单列:它们都是 typst 编译期失败,归
|
||||
`typstCompile`(ADR-0012)。版本契约 `cphVersionMismatch`(ADR-0016)是第 7 类。
|
||||
-/
|
||||
|
||||
namespace Spec.Courseware
|
||||
|
||||
/-- 诊断严重级别(`PINNED` 二分, ADR-0005)。`error` 阻断(产物不合法),`warning` 不
|
||||
阻断(产物仍可导出,只是有损)。更细级别(info/hint)未决策,故只二分。 -/
|
||||
/-- 诊断严重级别(ADR-0005)。`error` 阻断(产物不合法),`warning` 不阻断(产物仍可导出,
|
||||
只是有损)。更细级别(info/hint)未决策,故只二分。 -/
|
||||
inductive Severity where
|
||||
| warning
|
||||
| error
|
||||
|
||||
/-- 诊断**分类**(`PINNED` 7 类, ADR-0010,经 ADR-0012 修订为 6 类,经 ADR-0016 增至 7
|
||||
类)。按"谁来判定"分三层:**结构型**(模型自身可判):`partPathMissing`/`unknownKind`/
|
||||
`cphVersionMismatch`;**schema/外部设施型**(靠实现 oracle):
|
||||
`missingContentFile`/`schemaViolation`/`typstCompile`;**语义型**:`renderIgnored`。 -/
|
||||
/-- 诊断分类(ADR-0010,经 ADR-0012 折并为 6 类、ADR-0016 增至 7 类)。按 checker 怎么判分三层:
|
||||
结构型(checker 自己按结构判):`partPathMissing`/`unknownKind`/`cphVersionMismatch`;
|
||||
schema/外部工具型(得真跑工具):`missingContentFile`/`schemaViolation`/`typstCompile`;
|
||||
语义型:`renderIgnored`。 -/
|
||||
inductive DiagKind where
|
||||
/-- manifest 的 part 指向不存在的文件夹(或经 `..` 逃出根)。结构型。 -/
|
||||
| partPathMissing
|
||||
@@ -36,21 +45,19 @@ inductive DiagKind where
|
||||
/-- 实例数据不合其 kind 的 JSON Schema;亦作 manifest/element.toml 畸形的兜底。 -/
|
||||
| schemaViolation
|
||||
/-- 拼装出的 typst 源编译失败:语法错、未解析的交叉引用 `@ref`、越界或缺失的相对
|
||||
`import`/`include`(后两者即旧 `danglingReference` 的两种情形——typst 在编译期
|
||||
检出,故归此类,ADR-0012)。外部设施型。 -/
|
||||
`import`/`include`。后两者 typst 在编译期检出,故归此类(ADR-0012)。外部工具型。 -/
|
||||
| typstCompile
|
||||
/-- 某被用到的 kind 在某声明的 target 下无渲染规则,该 element 被忽略。语义型。 -/
|
||||
| renderIgnored
|
||||
/-- 工程文件的 `.cph-version` 与 CLI(cph)版本不相容(ADR-0016)。**结构型**(加载期
|
||||
判)。工程文件根的 `.cph-version` 声明它所面向的 cph 版本;CLI 加载时按**兼容性判
|
||||
定**比对自身版本(实现侧 `CARGO_PKG_VERSION`),不相容即产此类。**当前判定为版本
|
||||
完全相等才相容**(MVP;后续可放宽为 semver 区间,判定逻辑可逐步修改而不动本分类)。
|
||||
`error` 级——版本不相容的工程文件不应被该 CLI 处理。 -/
|
||||
/-- 工程文件的 `.cph-version` 与 CLI(cph)版本不相容(ADR-0016)。结构型(加载期判)。
|
||||
工程文件根的 `.cph-version` 声明它所面向的 cph 版本;CLI 加载时比对自身版本,不相容
|
||||
即产此类。当前判定为版本完全相等才相容(MVP;后续可放宽为 semver 区间,判定逻辑可
|
||||
逐步改而不动本分类)。`error` 级——版本不相容的工程文件不应被该 CLI 处理。 -/
|
||||
| cphVersionMismatch
|
||||
|
||||
/-- 每类诊断的**严重级别**(`PINNED`, ADR-0010)。六类 `error`(阻断);**唯
|
||||
`renderIgnored` 为 `warning`**——ADR-0005 种子规则"缺渲染 ⇒ warning,不阻断导出"。
|
||||
钉成全函数使"哪类阻断"成为可引用、可对齐的事实(实现侧 `DiagCode` 级别据此对齐)。 -/
|
||||
/-- 每类诊断的严重级别(ADR-0010)。六类 `error`(阻断);唯 `renderIgnored` 为 `warning`
|
||||
——ADR-0005 种子规则"缺渲染 ⇒ warning,不阻断导出"。钉成全函数使"哪类阻断"成为可
|
||||
引用、可对齐的事实。 -/
|
||||
def DiagKind.severity : DiagKind → Severity
|
||||
| .partPathMissing => .error
|
||||
| .unknownKind => .error
|
||||
@@ -60,46 +67,51 @@ def DiagKind.severity : DiagKind → Severity
|
||||
| .renderIgnored => .warning
|
||||
| .cphVersionMismatch => .error
|
||||
|
||||
/-- 缺渲染诊断的级别 = **warning**(`PINNED`, ADR-0005/0010,**非 error**)。具名常量,
|
||||
使"它是 warning"可被实现侧 grep 对齐(实现里同名常量 `RENDER_IGNORED_SEVERITY` 引用
|
||||
本定义)。等价于 `DiagKind.renderIgnored.severity`。 -/
|
||||
/-- 缺渲染诊断的级别 = warning(ADR-0005/0010,非 error)。具名常量,使"它是 warning"
|
||||
可被实现 grep 对齐(实现里同名常量 `RENDER_IGNORED_SEVERITY` 引用本定义)。
|
||||
等价于 `DiagKind.renderIgnored.severity`。 -/
|
||||
def renderIgnoredSeverity : Severity := DiagKind.renderIgnored.severity
|
||||
|
||||
variable (P : Primitives)
|
||||
|
||||
/-- **缺渲染诊断**:lesson 在 target `t` 下存在无法渲染的 element(`PINNED`,
|
||||
ADR-0005/0009)。成立 ⟺ 存在某 element,其 kind 在 `t` 下 `covers` 为假。语义型诊断,
|
||||
级别 warning。 -/
|
||||
/-- 缺渲染诊断:lesson 在 target `t` 下存在无法渲染的 element(ADR-0005/0009)。成立 ⟺
|
||||
存在某 element,其 kind 在 `t` 下 `covers` 为假。语义型诊断,级别 warning。 -/
|
||||
def renderIgnored (l : Lesson P) (c : RenderConfig P) (t : P.TargetId) : Prop :=
|
||||
∃ e ∈ l, ¬ c.covers e.kind t
|
||||
|
||||
/-!
|
||||
## 模型外设施型诊断:抽象谓词 + 实现边界(ADR-0010)
|
||||
## 要真跑工具才能判的诊断:抽象谓词 + Oracle
|
||||
|
||||
`typstCompile`/`schemaViolation`(的 schema-合规面)断言的是模型自身无法判定的事实——
|
||||
要跑 typst 编译器、schema 校验器。契约把它们建成**抽象谓词**,真值由实现提供的 oracle
|
||||
给出。下面用 `Oracle` 收口这些判定:它不是要在 Lean 里实现 checker,而是把"这些事实
|
||||
来自模型外"显式化、类型化。
|
||||
诊断分两类(按 checker 怎么判):有些 checker 自己按工程文件结构就能判(part 路径
|
||||
在不在、kind 知不知道、某 kind 在某 target 下有没有被覆盖);有些 checker 自己也判
|
||||
不了,得真跑外部工具——typst 编不编得过(要跑 typst 编译器)、数据合不合 schema(要
|
||||
跑 schema 校验器)、content 文件齐不齐(要看磁盘)。后者就是 `Oracle` 收口的。
|
||||
|
||||
`Oracle` 把这些"得 checker 委托外部工具才能判"的事实建成抽象谓词,真值由 checker 给。
|
||||
它不是要在 Lean 里实现 checker,而是把"这几件事 checker 自己算不了、得委托出去"显式
|
||||
表达、类型化。它只收 Legal 需要的、得委托外部工具的事实;checker 自己能判的(如
|
||||
`renderIgnored`)不进 Oracle。
|
||||
|
||||
(这两类 checker 都判得了;但 LLM 两类都判不了——这正是产品里要有个 rule-based
|
||||
checker 的理由,见本模块顶部。)
|
||||
-/
|
||||
|
||||
/-- **实现侧判定 oracle**(`PINNED` 实现边界, ADR-0010)。每个字段是一个谓词,真值由
|
||||
实现(checker)提供。结构型诊断(part 路径、未知 kind)不入此 oracle——那些模型自身可判。 -/
|
||||
/-- checker 委托外部工具才能判的那些事实(ADR-0010)。每个字段是一个谓词,真值由
|
||||
checker 提供。checker 自己按结构就能判的诊断(part 路径、未知 kind)不入此 oracle。 -/
|
||||
structure Oracle (l : Lesson P) (c : RenderConfig P) where
|
||||
/-- target `t` 下拼装源可编译(否 ⇒ `typstCompile`)。**含引用解析**:源能编译即蕴含
|
||||
其 `@ref`、相对 import 全部解析(ADR-0012 已把引用诊断并入 `typstCompile`)。 -/
|
||||
/-- target `t` 下拼装源可编译(否 ⇒ `typstCompile`)。含引用解析:源能编译即蕴含其
|
||||
`@ref`、相对 import 全部解析(ADR-0012)。 -/
|
||||
compiles : P.TargetId → Prop
|
||||
/-- 每个 element 数据合 schema(否 ⇒ `schemaViolation`)。 -/
|
||||
dataConforms : Prop
|
||||
/-- schema 要求的 content 文件齐备(否 ⇒ `missingContentFile`)。 -/
|
||||
contentFilesPresent : Prop
|
||||
|
||||
/-- **合法 lesson**(`PINNED`, ADR-0010;回填 ADR-0005 deferred 的"完整合法判定")。
|
||||
|
||||
合法 ⟺ 检查管线产出**零条 error 级诊断**。展开为:模型外设施判定(经 `Oracle`)全为真,
|
||||
**且**每个声明的 target 都编译通过。结构型诊断由 `cph-model` 在加载期判定;能走到这步
|
||||
谈合法性意味着已加载成功,故此处聚焦 schema/外部设施层。引用解析不单列——已被
|
||||
`compiles` 蕴含(ADR-0012)。`renderIgnored` 是 warning,**不**进合取——ADR-0005 种子
|
||||
规则的体现。`targets` 用全称式表达以不绑定 `TargetId` 的可枚举性。 -/
|
||||
/-- 合法 lesson(ADR-0010)。合法 ⟺ 检查管线产出零条 error 级诊断。展开为:得委托外部
|
||||
工具的判定(经 `Oracle`)全为真,且每个声明的 target 都编译通过。checker 自己按结构
|
||||
能判的诊断(part 路径、未知 kind)在加载期已判;能走到这步谈合法性意味着那些已过,
|
||||
故此处聚焦 schema/外部工具层。`renderIgnored` 是 warning,不进合取(ADR-0005 种子
|
||||
规则)。`targets` 用全称式表达以不绑定 `TargetId` 的可枚举性。 -/
|
||||
def Legal (l : Lesson P) (c : RenderConfig P) (o : Oracle P l c) : Prop :=
|
||||
o.dataConforms ∧ o.contentFilesPresent ∧
|
||||
(∀ t : P.TargetId, (c.spec t).isSome → o.compiles t)
|
||||
|
||||
@@ -1,26 +1,24 @@
|
||||
import Spec.Courseware.Check.Diagnostic
|
||||
|
||||
/-!
|
||||
# Pipeline —— checker 检查管线的阶段与序(ADR-0010)
|
||||
# Pipeline —— 检查管线的阶段与序
|
||||
|
||||
checker 的 `check` 按**固定顺序**跑五个阶段,逐阶段收集诊断;`compile` 阶段有**门控**。
|
||||
顺序与门控是契约——它决定用户看到哪些诊断(藏在缺文件背后的语法错,在文件补齐前不
|
||||
显示,这是有意的)。每阶段的**算法**不进 Lean(宪法第 5 条深度上限):只钉**阶段、序、
|
||||
门控**。阶段对应上游模块:`load`←`cph-model`;`structural`←part 路径/未知 kind;
|
||||
`schema`←`cph-schema`;`compile`←`cph-typst`(模型外设施);`coverage`←`renderIgnored`。
|
||||
checker 的 `check` 按固定顺序跑五个阶段,逐阶段收集诊断;`compile` 阶段有门控。顺序和
|
||||
门控是契约——它决定用户看到哪些诊断(藏在缺文件背后的语法错,在文件补齐前不显示,这是
|
||||
有意的)。每阶段的算法不进 Lean(宪法第 5 条深度上限):只钉阶段、序、门控。
|
||||
-/
|
||||
|
||||
namespace Spec.Courseware
|
||||
|
||||
/-- 检查管线的**阶段**(`PINNED` 5 阶段, ADR-0010)。
|
||||
/-- 检查管线的阶段(ADR-0010)。
|
||||
|
||||
- `load` —— 解析 manifest + 各 element.toml。**含 `.cph-version` 兼容性判定**
|
||||
(ADR-0016:工程根 `.cph-version` 与 CLI 版本不相容 ⇒ `cphVersionMismatch` error)。
|
||||
硬失败(无法解析 lesson)则**停**整条管线。
|
||||
- `load` —— 解析 manifest + 各 element.toml。含 `.cph-version` 兼容性判定(ADR-0016:
|
||||
工程根 `.cph-version` 与 CLI 版本不相容 ⇒ `cphVersionMismatch` error)。硬失败(无法
|
||||
解析 lesson)则停整条管线。
|
||||
- `structural` —— part 路径存在、无 `..`、kind 已知且一致。此处判缺的 part 后续跳过。
|
||||
- `schema` —— 每个"存在且 kind 已知"的 part 按其 kind schema 校验。
|
||||
- `compile` —— 模型外设施阶段(typst 编译)。**门控:仅当前序零 error 才跑**。
|
||||
- `coverage` —— 语义型 warning(`renderIgnored`);**不**受门控,总跑。 -/
|
||||
- `compile` —— 跑外部工具的阶段(typst 编译)。门控:仅当前序零 error 才跑。
|
||||
- `coverage` —— 语义型 warning(`renderIgnored`);不受门控,总跑。 -/
|
||||
inductive Phase where
|
||||
| load
|
||||
| structural
|
||||
@@ -29,8 +27,8 @@ inductive Phase where
|
||||
| coverage
|
||||
deriving DecidableEq
|
||||
|
||||
/-- 管线阶段的**执行序**(`PINNED`, ADR-0010)。`order p` 越小越先跑。序是契约:
|
||||
`compile`(3)排在 `structural`(1)/`schema`(2)之后,正因前者门控于后者无 error。 -/
|
||||
/-- 管线阶段的执行序(ADR-0010)。`order p` 越小越先跑。序是契约:`compile`(3)排在
|
||||
`structural`(1)/`schema`(2)之后,正因前者门控于后者无 error。 -/
|
||||
def Phase.order : Phase → Nat
|
||||
| .load => 0
|
||||
| .structural => 1
|
||||
@@ -38,15 +36,14 @@ def Phase.order : Phase → Nat
|
||||
| .compile => 3
|
||||
| .coverage => 4
|
||||
|
||||
/-- 某阶段是否**受"前序零 error"门控**(`PINNED`, ADR-0010)。唯 `compile` 受门控:藏在
|
||||
结构/schema 错背后的编译错,在前者修好前不显示——有意降噪。 -/
|
||||
/-- 某阶段是否受"前序零 error"门控(ADR-0010)。唯 `compile` 受门控:藏在结构/schema 错
|
||||
背后的编译错,在前者修好前不显示——有意降噪。 -/
|
||||
def Phase.gated : Phase → Bool
|
||||
| .compile => true
|
||||
| _ => false
|
||||
|
||||
/-- 管线在 `load` 硬失败时**停**(`PINNED`, ADR-0010)。`load` 拿不到可解析 lesson 时,
|
||||
无 lesson 可喂下游,整条管线终止——唯一会截断后续所有阶段的情形(区别于 `compile`
|
||||
门控只跳过自己)。 -/
|
||||
/-- 管线在 `load` 硬失败时停(ADR-0010)。`load` 拿不到可解析 lesson 时,无 lesson 可喂
|
||||
下游,整条管线终止——唯一会截断后续所有阶段的情形(区别于 `compile` 门控只跳过自己)。 -/
|
||||
def Phase.haltsPipelineOnFailure : Phase → Bool
|
||||
| .load => true
|
||||
| _ => false
|
||||
|
||||
@@ -4,5 +4,5 @@ import Spec.Courseware.Export.Render
|
||||
/-!
|
||||
# Courseware.Export —— export target = artifact + 有序 typed steps
|
||||
|
||||
产物 ADT(`Artifact`)、build 规格与渲染覆盖(`Render`)。决策出处 ADR-0009 / 0011。
|
||||
产物 ADT、build 规格与渲染覆盖。决策出处 ADR-0009 / 0011。
|
||||
-/
|
||||
|
||||
@@ -1,23 +1,22 @@
|
||||
/-!
|
||||
# Artifact —— export target 的产物(ADR-0009 / 0011)
|
||||
# Artifact —— export target 的产物
|
||||
|
||||
ADR-0009:一个 export target 是**一次 build**,产出一个**有类型的产物**。ADR-0011
|
||||
钉死:产物是**带字段的 ADT**——"产物到底指什么"(单文件落在哪 / 一棵树产出哪些文件)
|
||||
是不好猜的领域语义,必须写进字段 + doc,而非抹成两个空构造子。路径/glob 用 `String`
|
||||
承载并由 doc 赋义(它们就是文本),不复刻文件系统类型。
|
||||
一个 export target 是一次 build,产出一个有类型的产物(ADR-0009、ADR-0011)。产物是
|
||||
带字段的 ADT:"产物到底指什么"(单文件落在哪 / 一棵树产出哪些文件)是不好猜的领域
|
||||
语义,要写进字段 + doc,而不是抹成两个空构造子。路径、glob 用 `String` 承载并由 doc
|
||||
赋义(它们就是文本),不复刻文件系统类型。
|
||||
-/
|
||||
|
||||
namespace Spec.Courseware
|
||||
|
||||
/-- export 产物(`PINNED` 带字段 ADT, ADR-0011)。产物形状决定 `cph build` 吐文件还是
|
||||
目录、reduce 怎么折叠(`singleFile` 把有序片段拼成一份再编译——交叉引用 `@ref`、例题
|
||||
计数器能工作的前提;`fileTree` 每 part 落一文件)。后端/格式仍 OPEN(ADR-0009)。 -/
|
||||
/-- export 产物(ADR-0011)。产物形状决定 `cph build` 吐文件还是目录、reduce 怎么折叠
|
||||
(`singleFile` 把有序片段拼成一份再编译——交叉引用 `@ref`、例题计数器能工作的
|
||||
前提;`fileTree` 每 part 落一文件)。后端、格式仍 OPEN(ADR-0009)。 -/
|
||||
inductive Artifact where
|
||||
/-- 单文件产物,落在 `filepath`(相对工程根)。讲义/教案 PDF 即此。 -/
|
||||
| singleFile (filepath : String)
|
||||
/-- 多文件产物:`root` 目录下匹配 `outputs` **glob** 的文件集(第三方平台 archive
|
||||
即此)。用 glob 而非显式清单:轻,又让消费方/checker 知道该产出哪些文件、可校验
|
||||
完整性。 -/
|
||||
/-- 多文件产物:`root` 目录下匹配 `outputs` glob 的文件集(第三方平台归档即此)。
|
||||
用 glob 而非显式清单:轻,又让消费方/checker 知道该产出哪些文件、可校验完整性。 -/
|
||||
| fileTree (root : String) (outputs : String)
|
||||
|
||||
end Spec.Courseware
|
||||
|
||||
@@ -2,88 +2,89 @@ import Spec.Courseware.Model.Primitives
|
||||
import Spec.Courseware.Export.Artifact
|
||||
|
||||
/-!
|
||||
# Render —— export target = artifact + 有序 typed steps(ADR-0009 / 0011)
|
||||
# Render —— export target = artifact + 有序 typed steps
|
||||
|
||||
ADR-0009:export target 是一次 build,产出一个有类型的 `Artifact`。ADR-0011 钉死 build
|
||||
的**形状**:一个 target 是 `artifact` + 一串**有序 typed step**。
|
||||
一个 export target 是一次 build,产出一个有类型的 `Artifact`(ADR-0009)。build 的形状
|
||||
是:一个 target = `artifact` + 一串有序的 typed step(ADR-0011)。
|
||||
|
||||
- `typstCompile template` —— 把**模板文件**(如 `exports/student.typ`)编译成产物。它是
|
||||
*typed* 而非裸 shell,正因框架要把 **manifest 注入**模板(经 `--input manifest=…`),
|
||||
裸字符串表达不了这个 wiring。presentation(编号、样式)住模板里,不在 manifest。
|
||||
- `shell run` —— 逃生口,给难以声明的步骤(ADR-0005 的 (b) 类 medium-only)。
|
||||
- `assembleMarkdown field` —— 按 parts 顺序把每个 element 的 `field`(markdown content 叶子,
|
||||
ADR-0015)拼成**单文件 markdown** 产物。typed 而非 `cat`,因为按 manifest `[[parts]]` 顺序读取 +
|
||||
跳过缺失项 + 写到单文件产物路径这件事,框架 own 比裸 shell 稳。
|
||||
- `typstCompile template` —— 把模板文件(如 `exports/student.typ`)编译成产物。它是
|
||||
typed 而非裸 shell,因为框架要把 manifest 注入模板(经 `--input manifest=…`),裸
|
||||
字符串表达不了这个 wiring。presentation(编号、样式)住模板里,不在 manifest。
|
||||
- `shell run` —— 逃生口,给难以声明的步骤。
|
||||
- `assembleMarkdown field` —— 按 parts 顺序把每个 element 的 `field`(markdown content
|
||||
叶子,ADR-0015)拼成单文件 markdown 产物。typed 而非裸 `cat`:按 manifest `[[parts]]`
|
||||
顺序读取 + 跳过缺失项 + 写到单文件产物路径,框架自己来比裸 shell 稳。
|
||||
|
||||
**渲染覆盖**:ADR-0011 废止了 per-target `RenderRule` 载荷——渲染的"how"已移进模板。
|
||||
契约只保留覆盖声明 `covers`(该 target 渲染哪些 kind),供种子诊断用。
|
||||
渲染覆盖:契约只保留覆盖声明 `covers`(该 target 渲染哪些 kind),供种子诊断用;渲染的
|
||||
"how"住模板里(ADR-0011)。
|
||||
|
||||
**shell step 的执行语义(ADR-0013)。** `shell` 不再只是占位:它**会被执行**,语义是把
|
||||
`run` 交给平台 shell、以**工程根为工作目录**运行,产物由被调外部工具自己写出(框架不装配
|
||||
内容)。三条边界是真分歧点,故钉契约:
|
||||
1. **opt-in by construction** —— 任意命令执行只在用户**显式** build 一个 shell target 时发生,
|
||||
绝不在 `check` 里跑。`check` 只校验结构(lesson 是否合法),不执行外部工具、不验其产物。
|
||||
2. **失败归属** —— shell step 退出非零是一次 **build-过程失败**,不是 lesson 的合法性缺陷;
|
||||
因此它**不**进 `Diagnostic` 的 6 类(那 6 类是 lesson 自身的诊断,见 `Check/Diagnostic.lean`),
|
||||
而由 build 执行层报告。诊断分类保持 6 类不变(ADR-0013 显式拒绝新增 `ShellStep` 诊断码)。
|
||||
3. **非-typst target 不过 typst 编译** —— 一个只含 `shell` step 的 target(教具包即此)由
|
||||
shell step 的执行语义(ADR-0013):`shell` 会被执行,语义是把 `run` 交给平台 shell、以
|
||||
工程根为工作目录运行,产物由被调外部工具自己写出(框架不装配内容)。三条边界:
|
||||
|
||||
1. opt-in:命令执行只在用户显式 build 一个 shell target 时发生,绝不在 `check` 里跑。
|
||||
`check` 只校验结构,不执行外部工具、不验其产物。
|
||||
2. 失败归属:shell step 退出非零是一次 build 过程失败,不是 lesson 的合法性缺陷;因此
|
||||
它不进 `Diagnostic` 的 7 类(那 7 类是 lesson 自身的诊断,见 `Check/Diagnostic.lean`),
|
||||
而由 build 执行层报告。诊断分类保持 7 类不变。
|
||||
3. 非-typst target 不过 typst 编译:一个只含 `shell` step 的 target(教具包即此)由
|
||||
执行器跑命令,而非走 typst 引擎;`check` 的 compile 阶段跳过它。
|
||||
|
||||
**assembleMarkdown step 的执行语义(ADR-0015)。** 与 `shell` 同属"非-typst target":框架 own
|
||||
读取每个 element 的 `<field>.md`、按 `[[parts]]` 顺序拼接、写到单文件产物路径(产物是 markdown,
|
||||
不经 typst 引擎)。同 shell 的三条边界:① 只在显式 `build --target` 跑,`check` 不跑;② 装配失败
|
||||
(如写盘失败、引用图缺失)是 build-过程错误,不入 6 类诊断;③ 非-typst target,`check` 的 compile
|
||||
阶段跳过它。**单文件产物**(现):装配器注入课程级标题为文档 h1(课程元数据,非 element 内容),
|
||||
每份 `slides.md`/`transcript.md` 贡献其 `##` part 与 `###` 小节(presentation 在内容里, ADR-0011),
|
||||
按 `[[parts]]` 顺序拼接(分隔符空行)。**自包含**:装配器扫描产物里的 `` 图引用,把引用到的
|
||||
本地图从工程根按原相对路径复制进产物所在 build 根,使该 build 目录可独立交付;引用图在工程根缺失属
|
||||
build-过程错误(不入 6 类)。外部 URL(`http(s)://`/`data:`)不复制。结构化 FileTree 产物延后
|
||||
(待 parts 树形重组, ADR-0015 OPEN)。
|
||||
assembleMarkdown step 的执行语义(ADR-0015):与 `shell` 同属"非-typst target"。框架
|
||||
自己读每个 element 的 `<field>.md`、按 `[[parts]]` 顺序拼接、写到单文件产物路径(产物
|
||||
是 markdown,不经 typst 引擎)。同 shell 的三条边界:① 只在显式 `build --target` 跑,
|
||||
`check` 不跑;② 装配失败(如写盘失败、引用图缺失)是 build 过程错误,不入 7 类诊断;
|
||||
③ 非-typst target,`check` 的 compile 阶段跳过它。
|
||||
|
||||
单文件产物(现):装配器注入课程级标题为文档 h1(课程元数据,非 element 内容),每份
|
||||
`slides.md`/`transcript.md` 贡献其 `##` part 与 `###` 小节(presentation 在内容里,
|
||||
ADR-0011),按 `[[parts]]` 顺序拼接(分隔符空行)。自包含:装配器扫描产物里的 ``
|
||||
图引用,把引用到的本地图从工程根按原相对路径复制进产物所在 build 根,使该 build 目录
|
||||
可独立交付;引用图在工程根缺失属 build 过程错误(不入 7 类)。外部 URL(`http(s)://`、
|
||||
`data:`)不复制。结构化 FileTree 产物延后(待 parts 树形重组,ADR-0015 OPEN)。
|
||||
-/
|
||||
|
||||
namespace Spec.Courseware
|
||||
|
||||
variable (P : Primitives)
|
||||
|
||||
/-- 一个 build **step**(`PINNED` typed, ADR-0011;可扩展)。MVP 仅一个 `typstCompile`;
|
||||
`steps` 是 list 因为 FileTree / 第三方 build 会需多步。刻意不把模板内部、shell 命令的
|
||||
解析结构写进来(实现细节, ADR-0011 OPEN)。 -/
|
||||
/-- 一个 build step(ADR-0011;可扩展)。MVP 仅一个 `typstCompile`;`steps` 是 list 因为
|
||||
FileTree、第三方 build 会需多步。不把模板内部、shell 命令的解析结构写进来(实现细节,
|
||||
ADR-0011 OPEN)。 -/
|
||||
inductive Step where
|
||||
/-- 编译模板文件 `template`(相对工程根)成产物;框架注入 manifest。typed 的理由:
|
||||
注入这件事裸 shell 写不出。 -/
|
||||
| typstCompile (template : String)
|
||||
/-- shell 逃生口:执行命令 `run`(ADR-0005 (b) 类落这)。**已实现**(ADR-0013):以工程根
|
||||
为 cwd 执行,opt-in(只在显式 build 该 target 时跑,`check` 不跑),失败属 build-过程错误
|
||||
而非 lesson 诊断。教具包(如 KenKen 交互 HTML 由外部 `kendoku` 生成)即走此 step。 -/
|
||||
/-- shell 逃生口:执行命令 `run`(ADR-0013)。以工程根为 cwd 执行,opt-in(只在显式
|
||||
build 该 target 时跑,`check` 不跑),失败属 build 过程错误而非 lesson 诊断。
|
||||
教具包(如 KenKen 交互 HTML 由外部 `kendoku` 生成)即走此 step。 -/
|
||||
| shell (run : String)
|
||||
/-- 装配 markdown:按 `[[parts]]` 顺序读取每个 element 的 `field`(markdown content 叶子,
|
||||
ADR-0015),注入课程 h1 后拼接成**单文件 markdown** 产物,并收集 `` 引用的本地图进
|
||||
build 根使产物自包含。typed 而非 `cat`:按序读取+跳过缺失+注入标题+写盘+收集图由框架 own。
|
||||
**已实现**(ADR-0015):非-typst target(`check` 不跑,失败属 build-过程错误不入 6 类诊断)。
|
||||
slides 大纲面 / 逐字稿口播面即走此 step(直接 markdown+KaTeX 撰写,绕开 typst→md 公式转换,
|
||||
ADR-0014 R2)。 -/
|
||||
ADR-0015),注入课程 h1 后拼接成单文件 markdown 产物,并收集 `` 引用的本地图
|
||||
进 build 根使产物自包含。typed 而非 `cat`:按序读取+跳过缺失+注入标题+写盘+收集图由
|
||||
框架自己来。非-typst target(`check` 不跑,失败属 build 过程错误不入 7 类诊断)。
|
||||
slides 大纲、逐字稿口播即走此 step(直接 markdown+KaTeX 撰写,绕开 typst→md 公式转换,
|
||||
ADR-0014)。 -/
|
||||
| assembleMarkdown (field : String)
|
||||
|
||||
/-- 一个 export target 的 build 规格(`PINNED` artifact + 有序 steps, ADR-0011)。 -/
|
||||
/-- 一个 export target 的 build 规格(ADR-0011:artifact + 有序 steps)。 -/
|
||||
structure TargetSpec where
|
||||
/-- 产物(带字段,ADR-0011)。决定 build 折叠成单文件还是文件树。 -/
|
||||
artifact : Artifact
|
||||
/-- **有序** build steps。按序执行;MVP 仅一个 `typstCompile`。 -/
|
||||
/-- 有序 build steps。按序执行;MVP 仅一个 `typstCompile`。 -/
|
||||
steps : List Step
|
||||
/-- **覆盖声明**:`covers k` 表示此 target 渲染 kind `k`。ADR-0011 把旧
|
||||
`renders : KindId → Option RenderRule` 降级后的产物——契约只声明"渲染哪些 kind"
|
||||
(种子诊断 `renderIgnored` 用),"how"由 `steps` 的模板实现。 -/
|
||||
/-- 覆盖声明:`covers k` 表示此 target 渲染 kind `k`。契约只声明"渲染哪些 kind"
|
||||
(种子诊断 `renderIgnored` 用),"how"由 `steps` 的模板实现(ADR-0011)。 -/
|
||||
covers : P.KindId → Prop
|
||||
|
||||
/-- 渲染配置(`PINNED` target-中心, ADR-0009/0011)。`spec t = none` 表示 target `t`
|
||||
未声明(不导出);`some s` 给出其 build 规格。 -/
|
||||
/-- 渲染配置(ADR-0009/0011)。`spec t = none` 表示 target `t` 未声明(不导出);
|
||||
`some s` 给出其 build 规格。 -/
|
||||
structure RenderConfig where
|
||||
/-- target ↦ 该 target 的 build 规格(未声明则 `none`)。 -/
|
||||
spec : P.TargetId → Option (TargetSpec P)
|
||||
|
||||
/-- kind `k` 在 target `t` 下**被渲染**(`PINNED`, ADR-0009/0011;承接 ADR-0005)。成立
|
||||
⟺ `t` 已声明(`spec t = some s`)**且** `s.covers k`。为假即"此 kind 在此 target 下不
|
||||
被渲染"——checker 据此报 warning(见 `Diagnostic.renderIgnored`)。`P` 隐式以便点记法。 -/
|
||||
/-- kind `k` 在 target `t` 下被渲染(ADR-0009/0011)。成立 ⟺ `t` 已声明
|
||||
(`spec t = some s`)且 `s.covers k`。为假即"此 kind 在此 target 下不被渲染"——
|
||||
checker 据此报 warning(见 `Diagnostic.renderIgnored`)。 -/
|
||||
def RenderConfig.covers {P : Primitives} (c : RenderConfig P)
|
||||
(k : P.KindId) (t : P.TargetId) : Prop :=
|
||||
match c.spec t with
|
||||
|
||||
@@ -7,7 +7,5 @@ import Spec.Courseware.Model.Info
|
||||
/-!
|
||||
# Courseware.Model —— 工程文件的内容模型
|
||||
|
||||
留白基元(`Primitives`)、富内容锚点(`RichContent`)、原子单位(`Element`)、单节课
|
||||
(`Lesson`)、课时元信息(`Info`:canonical author 为列表 vs `RawInfo` 撰写态)。
|
||||
决策出处 ADR-0005 / 0006 / 0008。
|
||||
基元、富内容、element、lesson、课时元信息。决策出处 ADR-0005 / 0006 / 0008。
|
||||
-/
|
||||
|
||||
@@ -1,24 +1,23 @@
|
||||
import Spec.Courseware.Model.Primitives
|
||||
|
||||
/-!
|
||||
# Element —— 课程内容的原子单位
|
||||
# Element —— 课程内容的最小单位
|
||||
|
||||
ADR-0005:element 实例 = 一个 kind 标签 + 符合该 kind schema 的数据。本模块把它编码成
|
||||
依赖结构,使"数据必须匹配其 kind"成为类型层面的事实而非运行时校验。
|
||||
一个 element = 一个 kind 标签 + 符合该 kind schema 的数据(ADR-0005)。
|
||||
用依赖结构编码,使"数据必须匹配 kind"成为类型层面的事实,不是运行时校验。
|
||||
-/
|
||||
|
||||
namespace Spec.Courseware
|
||||
|
||||
variable (P : Primitives)
|
||||
|
||||
/-- element 实例(`PINNED`, ADR-0005)。`data : P.ElementData kind` 由 `kind` 决定——
|
||||
无法构造数据与 kind 不符的 element,schema 合规由类型系统保证。ADR-0005 的 (a) 类
|
||||
字段(逐字稿、重点圈划)落在具体 kind 的 `ElementData` 内,不出现在此通用结构上;
|
||||
交互教具等"重型 kind"在此与例题、定理同构,仅 `kind` 不同,重实现在模型之外。 -/
|
||||
/-- 一个 element 实例(ADR-0005)。data 的类型由 kind 决定,所以没法造出数据和 kind
|
||||
不符的 element——schema 合规由类型保证。逐字稿、重点圈划这类跟具体 kind 强相关
|
||||
的字段,落在该 kind 的 ElementData 里,不放在这个通用结构上。 -/
|
||||
structure Element where
|
||||
/-- 该 element 的 kind。 -/
|
||||
/-- 这个 element 的 kind。 -/
|
||||
kind : P.KindId
|
||||
/-- 符合 `kind` schema 的数据(类型随 `kind` 而变)。 -/
|
||||
/-- 符合 kind schema 的数据,类型随 kind 变。 -/
|
||||
data : P.ElementData kind
|
||||
|
||||
end Spec.Courseware
|
||||
|
||||
@@ -1,56 +1,54 @@
|
||||
/-!
|
||||
# Info —— 课时元信息:canonical 模型 vs 撰写态(authoring surface)
|
||||
# Info —— 课时元信息:canonical 模型 vs 撰写态
|
||||
|
||||
`[info]`(标题、作者)大多是 passthrough 元数据(ADR-0008),本不入契约。但**作者的
|
||||
基数**是一个真分歧点:一节课可由多人(教研组)署名,故 canonical 模型里 author 是一个
|
||||
**有序列表**,不是单值或可选单值。
|
||||
`[info]`(标题、作者)大多是 passthrough 元数据(ADR-0008),本不入契约。但作者的
|
||||
基数是一个真分歧点:一节课可由多人(教研组)署名,故 canonical 模型里 author 是一个
|
||||
有序列表,不是单值或可选单值。
|
||||
|
||||
另有一条值得钉的模式:on-disk 的**撰写态**(用户实际填写的形态)是**语法糖**——单作者可写
|
||||
`author = "…"`,多作者写 `author = ["…", "…"]`——但这个"字符串或数组"的二态**只活在加载
|
||||
边界**:`RawInfo` 经归一化折叠成 canonical `Info`,其后不再出现。canonical 接收端始终是
|
||||
`List String`,raw 形式不泄漏进模型其余部分。这正是 `Info`(canonical)与 `RawInfo`
|
||||
(撰写态)两个结构存在的理由。
|
||||
另有一条值得钉的模式:on-disk 的撰写态(用户实际填写的形态)是语法糖——单作者可写
|
||||
`author = "…"`,多作者写 `author = ["…", "…"]`——但这个"字符串或数组"的二态只活在
|
||||
加载边界:`RawInfo` 经归一化折叠成 canonical `Info`,其后不再出现。canonical 接收端
|
||||
始终是 `List String`,raw 形式不泄漏进模型其余部分。这正是 `Info`(canonical)与
|
||||
`RawInfo`(撰写态)两个结构存在的理由。
|
||||
-/
|
||||
|
||||
namespace Spec.Courseware
|
||||
|
||||
/-- 作者的**撰写态形式**(`PINNED` 仅填写便利, ADR-0008)。on-disk 单作者可写裸
|
||||
字符串、多作者写数组——填写便利,非语义分歧。此 union **只活在加载边界**,经
|
||||
`RawAuthor.normalize` 折叠后不再出现。 -/
|
||||
/-- 作者的撰写态形式(ADR-0008)。on-disk 单作者可写裸字符串、多作者写数组——填写便利,
|
||||
非语义分歧。此 union 只活在加载边界,经 `RawAuthor.normalize` 折叠后不再出现。 -/
|
||||
inductive RawAuthor where
|
||||
/-- 单作者裸字符串 `author = "…"`。 -/
|
||||
| one (name : String)
|
||||
/-- 多作者数组 `author = ["…", "…"]`。 -/
|
||||
| many (names : List String)
|
||||
|
||||
/-- raw 作者归一化为**有序作者列表**(`PINNED`, ADR-0008)。单作者 ⇒ 单元素列表;数组
|
||||
⇒ 原样。这条钉死"canonical 接收端始终是 `List String`"。 -/
|
||||
/-- raw 作者归一化为有序作者列表(ADR-0008)。单作者 ⇒ 单元素列表;数组 ⇒ 原样。
|
||||
这条钉"canonical 接收端始终是 `List String`"。 -/
|
||||
def RawAuthor.normalize : RawAuthor → List String
|
||||
| .one n => [n]
|
||||
| .many ns => ns
|
||||
|
||||
/-- 课时元信息的 **canonical 模型**(`PINNED` author 为列表, ADR-0008)。`authors` 是
|
||||
**有序列表**:多人署名第一类,空列表 = 未署名。`title` 等其余字段是 passthrough 元数据,
|
||||
不在此承诺更多。这是系统其余部分唯一所见的形态——author 在此**已**是列表,不再是
|
||||
"字符串或数组"。 -/
|
||||
/-- 课时元信息的 canonical 模型(ADR-0008)。`authors` 是有序列表:多人署名第一类,
|
||||
空列表 = 未署名。`title` 等其余字段是 passthrough 元数据,不在此承诺更多。这是系统
|
||||
其余部分唯一所见的形态——author 在此已是列表,不再是"字符串或数组"。 -/
|
||||
structure Info where
|
||||
/-- 标题(passthrough 元数据)。 -/
|
||||
title : String
|
||||
/-- 作者**有序列表**(空 = 未署名)。canonical 始终是列表。 -/
|
||||
/-- 作者有序列表(空 = 未署名)。canonical 始终是列表。 -/
|
||||
authors : List String
|
||||
|
||||
/-- 撰写态的 `[info]`(`PINNED` 仅填写便利, ADR-0008)。`author` 用 `RawAuthor`
|
||||
(字符串或数组),`author` 缺省即未署名。此结构刻画"为便于填写而存在的 raw 形态",
|
||||
**不**是模型其余部分流通的形式——它经 `RawInfo.toInfo` 归一化为 canonical `Info`。 -/
|
||||
/-- 撰写态的 `[info]`(ADR-0008)。`author` 用 `RawAuthor`(字符串或数组),缺省即未署名。
|
||||
此结构刻画"为便于填写而存在的 raw 形态",不是模型其余部分流通的形式——它经
|
||||
`RawInfo.toInfo` 归一化为 canonical `Info`。 -/
|
||||
structure RawInfo where
|
||||
/-- 标题。 -/
|
||||
title : String
|
||||
/-- 作者 raw 形式(可选;缺省即未署名)。 -/
|
||||
author : Option RawAuthor
|
||||
|
||||
/-- raw `[info]` 归一化为 canonical `Info`(`PINNED` 加载边界归一化, ADR-0008)。缺省
|
||||
author ⇒ 空列表,否则按 `RawAuthor.normalize`。raw 的"字符串或数组"二态在此被消解,
|
||||
**不**泄漏进 `Info`——canonical 接收端恒为 `List String`。 -/
|
||||
/-- raw `[info]` 归一化为 canonical `Info`(ADR-0008)。缺省 author ⇒ 空列表,否则按
|
||||
`RawAuthor.normalize`。raw 的"字符串或数组"二态在此被消解,不泄漏进 `Info`——
|
||||
canonical 接收端恒为 `List String`。 -/
|
||||
def RawInfo.toInfo (r : RawInfo) : Info :=
|
||||
{ title := r.title
|
||||
authors := (r.author.map RawAuthor.normalize).getD [] }
|
||||
|
||||
@@ -3,14 +3,14 @@ import Spec.Courseware.Model.Element
|
||||
/-!
|
||||
# Lesson —— 单节课工程文件
|
||||
|
||||
ADR-0005:一个工程文件 = 一节课,是 element 实例的**有序序列**。课程/单元不是工程
|
||||
文件,而是 lesson 的编排(见 `Spec.Courseware.Course`,OPEN)。
|
||||
一个工程文件 = 一节课,是 element 实例的有序序列(ADR-0005)。课程、单元不是工程文件,
|
||||
而是 lesson 的编排(见 `Spec.Courseware.Course`,OPEN)。
|
||||
-/
|
||||
|
||||
namespace Spec.Courseware
|
||||
|
||||
/-- 一节课(`PINNED`, ADR-0005)。用 `List` 因为 **element 次序承载教学语义**(先讲
|
||||
定义再举例 ≠ 反过来);**不建模时长**——ADR-0005 决定 lesson 是内容编排而非时间轴。 -/
|
||||
/-- 一节课(ADR-0005)。用 `List` 因为 element 的次序承载教学语义(先讲定义再举例, ≠ 反过来)。
|
||||
不建模时长——lesson 是内容编排,不是时间轴(ADR-0005)。 -/
|
||||
abbrev Lesson (P : Primitives) := List (Element P)
|
||||
|
||||
end Spec.Courseware
|
||||
|
||||
@@ -1,34 +1,26 @@
|
||||
/-!
|
||||
# Primitives —— Courseware 契约的留白基元
|
||||
# 基元
|
||||
|
||||
课程工程文件模型(ADR-0005)依赖一组基元:element kind 怎么标识、某 kind 的数据
|
||||
schema 是什么、export target 怎么标识。收口成载体 `Primitives`,让模型在其上参数化
|
||||
——契约谈得了 element / lesson / 渲染**之间的关系**,而把每个基元的**内部表示**留给
|
||||
实现。注意:某基元语义已 PINNED(如 schema 形态由 ADR-0006 钉死)与其表示进 Lean
|
||||
是两回事——JSON Schema / typst 的内部结构属实现细节,不入 Lean,故基元在此仍以抽象
|
||||
类型承载。富内容的 prose 母本见 `Courseware.RichContent`。
|
||||
课程模型要谈"element、lesson、target 之间的关系",但每个基元本身(element kind
|
||||
怎么标识、kind 的数据 schema 长什么样、target 怎么标识)的内部表示是实现的事。
|
||||
这里把它们收成一组抽象基元,让模型在它们之上参数化。
|
||||
|
||||
契约只钉基元之间的关系;基元内部用什么表示,留给实现。
|
||||
-/
|
||||
|
||||
namespace Spec.Courseware
|
||||
|
||||
/-- Courseware 契约基元载体(关系 `PINNED`, ADR-0005;各基元表示留给实现, ADR-0006)。 -/
|
||||
/-- 课程模型的一组抽象基元:关系已定,内部表示留给实现(ADR-0005、ADR-0006)。 -/
|
||||
structure Primitives where
|
||||
/-- element kind 标识(`PINNED` **开放宇宙**, ADR-0005;表示 `OPEN`)。刻意用抽象
|
||||
类型而非 `inductive`:ADR-0005 决定 kind 是开放可扩展宇宙(stdlib + 第三方),
|
||||
封闭枚举会违背它——此处开放是**已决策的**(区别于 `RunState` 的"尚未封闭")。 -/
|
||||
/-- element kind 的标识。kind 是开放宇宙:stdlib 加第三方都可加,不是封闭枚举
|
||||
(ADR-0005)。表示方式留给实现。 -/
|
||||
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;契约只锚定"数据符合
|
||||
kind schema"这条关系,故此处仍是抽象类型。 -/
|
||||
/-- 某 kind 的合法数据类型,以 kind 为索引:`ElementData k` 就是"符合 k 的 schema
|
||||
的数据"。schema 用声明式 JSON Schema,带 content 叶子(ADR-0006);JSON Schema
|
||||
的内部结构是实现细节,不进契约,契约只钉"数据要符合 kind 的 schema"这条关系。 -/
|
||||
ElementData : KindId → Type
|
||||
/-- export target 标识(`PINNED` 角色, ADR-0005;表示 `OPEN`)。一个 target 是一次
|
||||
build,产出对 lesson 的一种投影(讲义/教案/PPT/平台 archive…),见 `Render`。 -/
|
||||
/-- export target 的标识。一个 target 是一次 build,产出对 lesson 的一种投影
|
||||
(讲义、教案、PPT、平台归档等),见 Render。 -/
|
||||
TargetId : Type
|
||||
|
||||
-- 注:原 `RenderRule : Type` 已随 ADR-0011 移除。渲染的"how"不再是契约层 per-target
|
||||
-- 载荷,而由 `Render.TargetSpec.steps` 里 `typstCompile` step 引用的**模板文件**承载;
|
||||
-- 契约只保留覆盖声明 `TargetSpec.covers`(该 target 渲染哪些 kind),供种子诊断用。
|
||||
|
||||
end Spec.Courseware
|
||||
|
||||
@@ -1,44 +1,41 @@
|
||||
/-!
|
||||
# RichContent —— 富内容(ADR-0006 的 prose 母本)
|
||||
# 富内容
|
||||
|
||||
ADR-0006:element schema 的"叶子"可以是 `content` 类型,其值是一段**源文本**,
|
||||
按其 **format** 决定语义(ADR-0015)。两种 format:
|
||||
- **typst** —— 一段 typst 源,语义取该源作为 module 求值后的 body content(讲义/教案面)。
|
||||
- **markdown** —— 一段**原样**的 markdown + KaTeX 源,**不经 typst 求值**(slides 大纲面 / 逐字稿口播面;
|
||||
ADR-0015)。直接以 markdown 撰写**绕开** typst→markdown 的公式转换难题(ADR-0014 R2):公式一开始就是
|
||||
KaTeX 源(`$…$`),没有"把 typst 公式转成 md"这一步。
|
||||
element schema 的叶子可以是 content 类型:一段源文本,按 format 决定语义
|
||||
(ADR-0006、ADR-0015)。
|
||||
|
||||
关键约束(均 ADR-0006,源自 typst 源码事实):**typst** format 的富内容**不可无主**——typst 的源必须有
|
||||
`FileId`,否则 span 脱锚、相对 import 报"cannot access file system from here"。故每段 typst 富内容是 World 里
|
||||
的一等文件,坐落在一个**虚拟路径**上;相对 import 限本工程路径结构内 + `@package`(不跨工程)。markdown format
|
||||
的富内容不参与 typst 求值,但同样由一个虚拟路径定位(供 markdown 装配 step 按序读取,见 `Export/Render`)。
|
||||
两种 format:
|
||||
|
||||
本模块只立 prose 锚点 + 最小抽象签名:typst 的 `Content`/`Module` 内部结构、JSON Schema 形状、format 的
|
||||
具体判别属实现细节,不进 Lean,只承诺"富内容由一个虚拟路径定位"+"叶子带 format"这两条关系。
|
||||
- typst:一段 typst 源,求值后得到讲义/教案用的内容。
|
||||
- markdown:一段 markdown + KaTeX 源,原样保留,不经 typst 求值(slides 大纲、
|
||||
逐字稿口播)。直接用 markdown 写,公式一开始就是 KaTeX(`$…$`),绕开了
|
||||
typst→markdown 的公式转换这个难题(ADR-0014)。
|
||||
|
||||
约束:typst 内容必须挂在一个虚拟路径上(原因见 ADR-0006 的考据)。markdown 内容
|
||||
不经 typst 求值,但同样用虚拟路径定位,供 markdown 装配按序读取。
|
||||
|
||||
本模块只钉两条关系:富内容由一个虚拟路径定位、叶子带 format。typst 的 Content/Module
|
||||
内部结构、JSON Schema 形状、format 怎么判别,都是实现细节,不进契约。
|
||||
-/
|
||||
|
||||
namespace Spec.Courseware
|
||||
|
||||
/-- 富内容在工程文件路径结构中的**虚拟路径**(`OPEN` 表示, ADR-0006)。把一段富内容
|
||||
定位为 World 里的一等文件(span 可解析、相对 import 可锚定)。落盘后即真实相对路径
|
||||
(ADR-0007),不在本层承诺,故 opaque。 -/
|
||||
/-- 富内容在工程文件里的虚拟路径(ADR-0006)。落盘后是真实相对路径(ADR-0007),
|
||||
这层不承诺,所以 opaque。 -/
|
||||
opaque VPath : Type
|
||||
|
||||
/-- 富内容的 **format**(`PINNED`, ADR-0015)。`content` 叶子带 format:typst 叶子被 typst 求值;
|
||||
markdown 叶子原样保留(markdown+KaTeX 源,不经求值)。 -/
|
||||
/-- 富内容的 format(ADR-0015)。 -/
|
||||
inductive ContentFormat where
|
||||
/-- typst 源:求值为 typst `Content`(讲义/教案面)。 -/
|
||||
/-- typst 源:求值后得到讲义/教案用的内容。 -/
|
||||
| typst
|
||||
/-- markdown + KaTeX 源:原样保留,不经 typst 求值(slides 大纲面 / 逐字稿口播面;ADR-0015)。 -/
|
||||
/-- markdown + KaTeX 源:原样保留,不经 typst 求值(slides、逐字稿)。 -/
|
||||
| markdown
|
||||
|
||||
/-- 对一段富内容的**引用**:它坐落在某个虚拟路径上(`PINNED` 关系, ADR-0006),并带一个
|
||||
**format**(`PINNED`, ADR-0015)。刻意**不**建模源文本、不建模求值出的 `Content`(那是实现侧的事);
|
||||
只钉"富内容经由一个 `VPath` 定位 + 带 format",作为 `Primitives.ElementData` 里 `content` 叶子的语义锚点。 -/
|
||||
/-- 对一段富内容的引用:它挂在一个虚拟路径上(ADR-0006),带一个 format(ADR-0015)。
|
||||
不建模源文本,也不建模求值出的内容——那是实现的事;这里只钉"富内容由虚拟路径定位
|
||||
+ 带 format",作为 ElementData 里 content 叶子的语义锚点。 -/
|
||||
structure RichContentRef where
|
||||
/-- 该富内容所在的虚拟路径(ADR-0006;落盘后为真实相对路径, ADR-0007)。 -/
|
||||
vpath : VPath
|
||||
/-- 该富内容的 format(ADR-0015)。 -/
|
||||
format : ContentFormat
|
||||
|
||||
end Spec.Courseware
|
||||
|
||||
@@ -2,8 +2,8 @@ import Spec.Courseware.Open.QuestionBank
|
||||
import Spec.Courseware.Open.Course
|
||||
|
||||
/-!
|
||||
# Courseware.Open —— 留白骨架(核心关系 OPEN)
|
||||
# Courseware.Open —— 留白骨架
|
||||
|
||||
题库与 element 的关系(`QuestionBank`)、课程编排规则(`Course`)。两者均为已 surface
|
||||
但未决策的分歧点,按宪法第 2 条不臆造,待专门 ADR 落定。
|
||||
题库与 element 的关系(`QuestionBank`)、课程编排规则(`Course`)。两者都是已提出但
|
||||
未决策的分歧点,不臆造,待专门 ADR 落定。
|
||||
-/
|
||||
|
||||
@@ -1,10 +1,10 @@
|
||||
/-!
|
||||
# Course —— 课程编排(骨架,规则 OPEN)
|
||||
# Course —— 课程编排(OPEN)
|
||||
|
||||
ADR-0005:工程文件的粒度是**单节课**;course / 单元**不是**工程文件,而是 lesson 的
|
||||
**编排**。但"编排"的具体规则未决策:有序列表还是带层级(单元 → 课)的树?lesson 被
|
||||
引用还是被包含?跨 lesson 有无约束(目标覆盖、前后置)?这些都是 `OPEN`。
|
||||
工程文件的粒度是单节课(ADR-0005);course / 单元不是工程文件,而是 lesson 的编排。
|
||||
但"编排"的具体规则没定:有序列表,还是带层级(单元 → 课)的树?lesson 被引用还是被
|
||||
包含?跨 lesson 有无约束(目标覆盖、前后置)?这些都 OPEN。
|
||||
|
||||
按宪法第 2 条本模块**不臆造**编排结构——不建 `Course := List Lesson`(那会偷偷承诺
|
||||
"扁平有序、无层级")。只在此 surface:课程编排待专门 ADR。本文件当前不引入任何承诺性声明。
|
||||
不臆造编排结构——不建 `Course := List Lesson`(那会偷偷承诺"扁平有序、无层级")。课程
|
||||
编排待专门 ADR。本文件不引入任何承诺性声明。
|
||||
-/
|
||||
|
||||
@@ -1,10 +1,10 @@
|
||||
/-!
|
||||
# QuestionBank —— 题库(骨架,核心关系 OPEN)
|
||||
# QuestionBank —— 题库(OPEN)
|
||||
|
||||
题库是与工程文件并列的资产(类比 DAW 的 sample library):有自身结构的实体,又是最
|
||||
典型的可复用单元,lesson 会引用它。但**题库与 element 的关系尚未决策**,且用户明确
|
||||
指出"纯引用可能不够"——element 内联题目数据 / lesson 持指向题库条目的引用 / 两者并存?
|
||||
题库是与工程文件并列的资产:有自身结构的实体,又是最典型的可复用单元,lesson 会引用它。
|
||||
但题库与 element 的关系没定,用户也指出"纯引用可能不够"——element 内联题目数据?lesson
|
||||
持指向题库条目的引用?两者并存?
|
||||
|
||||
这是一个 `OPEN` 分歧点。按宪法第 2 条本模块**不替它选解**——不建 `QuestionRef` 也不建
|
||||
内联结构,只在此 surface。待专门 ADR 落定后再填。本文件当前不引入任何承诺性声明。
|
||||
这是 OPEN 分歧点。不替它选解——不建 `QuestionRef` 也不建内联结构,只在此提出。待专门
|
||||
ADR 落定后再填。本文件不引入任何承诺性声明。
|
||||
-/
|
||||
|
||||
+9
-17
@@ -1,31 +1,23 @@
|
||||
/-!
|
||||
# Prelude —— System 层共享标识符
|
||||
|
||||
平台层反复引用一组标识符(项目、run、session、principal、chat)。其内部表示从未被决策
|
||||
(UUID / 复合键、principal 子类型学),也非分歧点,故收口成 opaque 载体
|
||||
`Identifiers`,System 各模块在其上参数化——契约谈得了"锁 owner 是哪个 run"这类
|
||||
**关系**,却不对标识符表示作承诺。
|
||||
平台层反复引用一组标识符(项目、run、session、principal)。它们的内部表示从未被决策
|
||||
(UUID / 复合键、principal 的子类型学),也不是分歧点,所以收成 opaque 载体
|
||||
`Identifiers`,System 各模块在它之上参数化——契约谈得了"锁 owner 是哪个 run"这类关系,
|
||||
不对标识符表示作承诺。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
/-- System 层标识符载体(关系结构 `PINNED`;各字段表示 `OPEN`)。 -/
|
||||
/-- System 层标识符载体:关系已定,各字段表示 OPEN。 -/
|
||||
structure Identifiers where
|
||||
/-- 课程项目标识(`OPEN` 表示;聚合根,likec4 `Project`)。 -/
|
||||
/-- 课程项目标识(聚合根;表示 OPEN)。 -/
|
||||
ProjectId : Type
|
||||
/-- 一次 agent 任务的标识(`OPEN` 表示;锁的 owner、审计主体,`AgentRun`。provider 无关,
|
||||
ADR-0017;`@Claude` 仅为触发品牌,不承诺 provider)。 -/
|
||||
/-- 一次 Claude 任务的标识(锁的 owner、审计主体;表示 OPEN)。 -/
|
||||
RunId : Type
|
||||
/-- 长生命周期 agent 会话标识(`OPEN` 表示;**provider/model 绑定, ADR-0017**——一次
|
||||
session 不跨 provider/model;切 model 即新 session,跨 session 连续性由 ADR-0003 项目
|
||||
记忆/锚点重建,不由 session 自带。同 provider/model 内可跨多 run 复用, ADR-0002)。 -/
|
||||
/-- 长生命周期 Claude 会话标识(跨多 run 复用,ADR-0002;表示 OPEN)。 -/
|
||||
SessionId : Type
|
||||
/-- 权限主体标识(`OPEN` 表示及其子类型学;ADR-0004 的 user/chat/department/…
|
||||
子类型学未定且非本层分歧点,纯 plumbing,故只留 opaque 键)。 -/
|
||||
/-- 权限主体标识(表示 OPEN)。 -/
|
||||
Principal : Type
|
||||
/-- 飞书项目群 chat 标识(`OPEN` 表示;ADR-0001 协作空间、ADR-0003 锚点引用、
|
||||
ADR-0004 `feishu_chat` principal 三处共用同一实体。独立成载体而非 `Principal` 子
|
||||
类型——principal 子类型学 OPEN 见上,本层不预设"chat 是 principal 的哪种子型")。 -/
|
||||
ChatId : Type
|
||||
|
||||
end Spec.System
|
||||
|
||||
+10
-15
@@ -1,26 +1,21 @@
|
||||
import Spec.System.ProjectGroup
|
||||
import Spec.System.Run
|
||||
import Spec.System.Lock
|
||||
import Spec.System.Memory
|
||||
import Spec.System.Permission
|
||||
import Spec.System.PermissionGrant
|
||||
import Spec.System.Audit
|
||||
|
||||
/-!
|
||||
# System —— Hub 平台层契约
|
||||
|
||||
协作与执行的平台:项目、飞书群、AgentRun、锁、权限、审计、按需上下文。likec4
|
||||
(`docs/architecture/likec4/`)已画出这一层的**结构**;本层只补 likec4 画不出的
|
||||
**语义分歧点**:
|
||||
这一层是产品里的协作与执行平台:项目、飞书群、AgentRun、锁、权限、审计。决策出处
|
||||
ADR-0001..0004。
|
||||
|
||||
- `ProjectGroup` —— project↔飞书群 1:1 长生命周期绑定(ADR-0001);群是协作空间,不持锁。
|
||||
- `Run` —— AgentRun 状态与终止判定(状态集合完整性 OPEN)。
|
||||
现状:Hub 还没建、没有业务反馈,所以这一层多为 OPEN 占位,只钉少数已定且有语义分量的
|
||||
东西(锁 owner = run、持锁者必为非终止 run、角色三级)。其余等 Hub 真建起来、业务反馈
|
||||
来了再细化。做 SaaS 要的权限、LLM API 配置和用量、费用等管理概念,将来也落在这层。
|
||||
|
||||
- `Run` —— AgentRun 的终止判定(状态集合 OPEN)。
|
||||
- `Lock` —— 锁 owner = run(ADR-0002),及"持锁者必为非终止 run"的核心不变式。
|
||||
- `Memory` —— 按需上下文:锚点类别(ADR-0003)+ MCP 工具按 run/project 上下文授权的不变式。
|
||||
- `Permission` —— read⊂edit⊂manage 角色格、能力推导、单调性;force-release 在格外。
|
||||
- `PermissionGrant` —— grant(resource×principal×role)与 settings(六 policy 旋钮)结构
|
||||
(ADR-0004);role-capability 与 settings-policy 的组合规则 OPEN。
|
||||
- `Audit` —— 有意从简(内容多为 plumbing,OPEN)。
|
||||
- `Permission` —— read ⊂ edit ⊂ manage 角色三级;force-release 在格外。
|
||||
- 审计以 run 为主体记录其生命周期事件;审计记录里装什么未定(OPEN)。
|
||||
|
||||
标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004。
|
||||
标识符见 `Spec.Prelude`。
|
||||
-/
|
||||
|
||||
@@ -1,22 +0,0 @@
|
||||
import Spec.Prelude
|
||||
|
||||
/-!
|
||||
# Audit —— 审计日志(有意从简)
|
||||
|
||||
likec4 把 `AuditLog` 列为实体(`AgentRun -> AuditLog 'records lifecycle events'`),
|
||||
但**审计记录里装什么**(事件 schema、保留策略、可查询维度)在任何 ADR / 散文里都
|
||||
未决策,且大多是 plumbing——按分歧点测试不入契约。故本模块刻意几乎为空:只固定
|
||||
"审计以 run 为主体记录其生命周期事件"这一条已决策关系,其余 `OPEN`(留白本身是
|
||||
契约的一部分:承诺此处尚无答案、勿填)。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
/-- 审计条目的最小骨架(关系 `PINNED` / 内容 `OPEN`, likec4)。只承诺"一条审计记录
|
||||
关联到某个 run";事件类型、时间、actor、详情等字段 `OPEN`,待真实分歧点出现时由
|
||||
对应 ADR 落定。 -/
|
||||
structure AuditEntry (I : Identifiers) where
|
||||
/-- 该审计条目所属的 run(`PINNED` 关系, likec4)。 -/
|
||||
run : I.RunId
|
||||
|
||||
end Spec.System
|
||||
+12
-17
@@ -4,34 +4,29 @@ import Spec.System.Run
|
||||
/-!
|
||||
# Lock —— 项目锁与排他不变式
|
||||
|
||||
ADR-0002 的核心:防止并发 Claude 同改一个项目,锁的 **owner 是当前 `AgentRun`**
|
||||
(不是 teacher / chat / session)。本模块把这条决策编码进类型,并钉死那条
|
||||
likec4 画不出的语义不变式——**持锁者必为非终止 run**。
|
||||
ADR-0002 的核心:防止并发 Claude 同改一个项目,锁的 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 持有。 -/
|
||||
/-- 项目级锁(ADR-0002)。`owner : RunId`(非 SessionId/Principal)从类型上编码
|
||||
"lock owner = run":锁不可能被 session / teacher 持有。 -/
|
||||
structure ProjectAgentLock where
|
||||
/-- 作用域:项目级(`PINNED`, ADR-0002 `scope = project_id`)。 -/
|
||||
/-- 作用域:项目级(ADR-0002)。 -/
|
||||
scope : I.ProjectId
|
||||
/-- 持有者:一个 run(`PINNED`, ADR-0002 `owner = run_id`)。 -/
|
||||
/-- 持有者:一个 run(ADR-0002)。 -/
|
||||
owner : I.RunId
|
||||
|
||||
/-- 锁表:每项目当前持锁 run(`PINNED` 排他性, ADR-0002)。`ProjectId → Option RunId`
|
||||
的结构**本身**即排他——不可能为同一项目登记两个并发 owner。 -/
|
||||
/-- 锁表:每项目当前持锁 run(ADR-0002 排他性)。`ProjectId → Option RunId` 的结构本身
|
||||
即排他——不可能为同一项目登记两个并发 owner。 -/
|
||||
def LockTable := I.ProjectId → Option I.RunId
|
||||
|
||||
/-- 锁表良构:**持锁者必为非终止 run**(`PINNED` 平台核心不变式, ADR-0002)。
|
||||
|
||||
"锁在 run 终止时释放"的逻辑等价物:若 `p` 的锁被 `r` 持有,则 `r` 不在终止态。这条
|
||||
把 Lock 与 Run 耦合起来——likec4 能画"run owns lock while running",画不出"终止即
|
||||
必须释放"这个约束;它正是契约相对结构图的增量。 -/
|
||||
def LockTable.WellFormed
|
||||
(lt : LockTable I) (statusOf : I.RunId → RunState) : Prop :=
|
||||
∀ p r, lt p = some r → ¬ (statusOf r).Terminal
|
||||
/-- 锁表良构:持锁者必为非终止 run(ADR-0002 核心不变式)。"锁在 run 终止时释放"
|
||||
的等价物:若 `p` 的锁被 `r` 持有,则 `r` 不在终止态。 -/
|
||||
def LockTable.WellFormed (lt : LockTable I) : Prop :=
|
||||
∀ p r, lt p = some r → ¬ Terminal I r
|
||||
|
||||
end Spec.System
|
||||
|
||||
@@ -1,51 +0,0 @@
|
||||
import Spec.Prelude
|
||||
|
||||
/-!
|
||||
# Memory —— 按需上下文:锚点与项目记忆(ADR-0003)
|
||||
|
||||
ADR-0003:Hub **只存锚点与项目记忆**,不存全量飞书消息历史;Claude 需要更多上下文时经
|
||||
飞书 API 按需读取。本模块刻画所存锚点的**类别**(ADR 列定,枚举完整性 OPEN——ADR 是
|
||||
"例如"式列举,新增类别不违反契约),并钉死一条 likec4 画不出的安全不变式:**MCP 工具
|
||||
按 run/project 上下文授权,Claude 不得传任意 chat id**(ADR-0003 Consequences 末条)。
|
||||
|
||||
"chat id 与 project 绑定"这一锚点类别由 `ProjectGroup.GroupBinding`(ADR-0001)权威承载,
|
||||
本模块不重复声明,只覆盖其余飞书侧指针(触发消息、状态卡片、回复、线程)。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
variable (I : Identifiers)
|
||||
variable (MessageId CardId : Type)
|
||||
|
||||
/-- 上下文锚点(`PINNED` 类别, ADR-0003 列定;**枚举完整性 `OPEN`**——ADR 是"例如"式
|
||||
列举,实现若需新类别须 surface,不得默认本枚举已穷尽)。承载 Hub 保留的飞书侧最小指针,
|
||||
而非消息正文。 -/
|
||||
inductive Anchor where
|
||||
/-- 触发某次 run 的消息(`PINNED` 类别, ADR-0003 "trigger message id")。 -/
|
||||
| triggerMessage : MessageId → Anchor
|
||||
/-- 某 run 的状态卡片(`PINNED` 类别, ADR-0003 "run id and status card id")。 -/
|
||||
| statusCard : I.RunId → CardId → Anchor
|
||||
/-- 回复锚点(`PINNED` 类别, ADR-0003 "reply anchors")。 -/
|
||||
| reply : MessageId → Anchor
|
||||
/-- 线程锚点(`PINNED` 类别, ADR-0003 "thread anchors")。 -/
|
||||
| thread : MessageId → Anchor
|
||||
|
||||
/-- MCP 读上下文请求:由某 run 发起、指向某 chat(`PINNED` 关系, ADR-0003 "Claude calls
|
||||
MCP tools to read … through Feishu APIs")。 -/
|
||||
structure McpReadRequest where
|
||||
/-- 发起请求的 run(授权上下文主体, ADR-0003)。 -/
|
||||
run : I.RunId
|
||||
/-- 请求读取的 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 越权读取。 -/
|
||||
def McpReadRequest.Authorized
|
||||
(req : McpReadRequest I)
|
||||
(runProject : I.RunId → Option I.ProjectId)
|
||||
(boundChat : I.ProjectId → Option I.ChatId) : Prop :=
|
||||
∃ p, runProject req.run = some p ∧ boundChat p = some req.chat
|
||||
|
||||
end Spec.System
|
||||
@@ -1,66 +1,23 @@
|
||||
import Spec.Prelude
|
||||
|
||||
/-!
|
||||
# Permission —— 角色、能力与授权
|
||||
# Permission —— 协作者角色
|
||||
|
||||
ADR-0004:权限走"飞书云文档式"——grant(`resource + principal + role`)与 settings
|
||||
分离;role 取自封闭的 `read / edit / manage`,且 **read ⊂ edit ⊂ manage** 累积赋能;
|
||||
强制释放锁是 **admin-only**,在 role 体系之外。本模块把这套结构与"高 role 含低
|
||||
role 全部能力"的单调性钉死。
|
||||
ADR-0004:权限走"飞书云文档式"——grant(resource + principal + role)与 settings 分离;
|
||||
role 取自封闭的 read / edit / manage,且 read ⊂ edit ⊂ manage 累积赋能;强制释放锁是
|
||||
admin-only,在 role 体系之外。
|
||||
|
||||
本模块钉角色三级与累积关系。具体哪些操作归哪级,见 ADR-0004,待业务反馈细化——所以这里
|
||||
不钉操作枚举,也不钉"哪个能力要求哪个 role"的映射。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
/-- 协作者角色(`PINNED` 封闭, ADR-0004 逐字 "roles are read, edit, or manage")。 -/
|
||||
/-- 协作者角色(ADR-0004:read / edit / manage)。read ⊂ edit ⊂ manage,高 role 含低 role
|
||||
全部能力。强制释放锁不在这套体系里,是 admin-only override,由平台另行判定。 -/
|
||||
inductive Role where
|
||||
| read
|
||||
| edit
|
||||
| manage
|
||||
|
||||
/-- 角色赋能层级(`PINNED` 序, ADR-0004 read⊂edit⊂manage 数值化)。仅服务于
|
||||
`Role.le` 与能力推导,不对外承诺"层级就是 `Nat`"。 -/
|
||||
def Role.level : Role → Nat
|
||||
| .read => 0
|
||||
| .edit => 1
|
||||
| .manage => 2
|
||||
|
||||
/-- 角色偏序:`r₁ ≤ r₂` 即 `r₁` 赋能不强于 `r₂`(`PINNED`, ADR-0004)。 -/
|
||||
def Role.le (r₁ r₂ : Role) : Prop := r₁.level ≤ r₂.level
|
||||
|
||||
/-- 受 role 调控的操作能力(各项 `PINNED` 取自 ADR-0004;**枚举完整性 `OPEN`**——
|
||||
这是 ADR 当前点名的能力,不保证穷尽,新增产品操作时可能扩)。注意 force-release
|
||||
**不在此列**——它是 admin-only override,见 `RequiresAdmin`。 -/
|
||||
inductive Capability where
|
||||
| view
|
||||
| discussComment
|
||||
| editArtifact
|
||||
| triggerAgent
|
||||
| answerChoiceCard
|
||||
| manageCollaborators
|
||||
| projectSettings
|
||||
| groupBinding
|
||||
| normalCancel
|
||||
|
||||
/-- 某能力所**要求的最低角色**(`PINNED`, ADR-0004 各 role 能力展开)。授权判定
|
||||
`Role.can` 据此定义,"谁能做什么"只有这一处真相。 -/
|
||||
def Capability.requiredRole : Capability → Role
|
||||
| .view => .read
|
||||
| .discussComment | .editArtifact | .triggerAgent | .answerChoiceCard => .edit
|
||||
| .manageCollaborators | .projectSettings | .groupBinding | .normalCancel => .manage
|
||||
|
||||
/-- 角色 `r` **具备**能力 `c`(`PINNED`, ADR-0004)。定义为"`c` 的最低角色 ≤ `r`",
|
||||
这一处同时编码了 read⊂edit⊂manage 的累积性。 -/
|
||||
def Role.can (r : Role) (c : Capability) : Prop := c.requiredRole |>.le r
|
||||
|
||||
/-- **单调性**:`r₁ ≤ r₂` 且 `r₁` 能做 `c` ⇒ `r₂` 也能(`PINNED` 定理, ADR-0004 累积
|
||||
赋能的形式化保证)。证明即偏序传递性,得益于 `can` 按"最低角色阈值"定义。 -/
|
||||
theorem Role.can_mono {r₁ r₂ : Role} {c : Capability}
|
||||
(h : r₁.le r₂) (hc : r₁.can c) : r₂.can c :=
|
||||
Nat.le_trans hc h
|
||||
|
||||
/-- **强制释放锁**要求 admin,**在 role 体系之外**(`PINNED`, ADR-0004 admin-only
|
||||
override)。即便 `manage` 也不经 `Role.can` 获得它,故它不是 `Capability` 而是独立
|
||||
谓词;`isAdmin` 由平台另行判定(本层不建 admin 模型)。 -/
|
||||
def RequiresAdmin (isAdmin : Prop) : Prop := isAdmin
|
||||
|
||||
end Spec.System
|
||||
|
||||
@@ -1,69 +0,0 @@
|
||||
import Spec.Prelude
|
||||
import Spec.System.Permission
|
||||
|
||||
/-!
|
||||
# PermissionGrant —— 授权与设置(ADR-0004)
|
||||
|
||||
ADR-0004 的"飞书云文档式"权限:**grant**(`resource × principal × role`)与 **settings**
|
||||
(各 policy 旋钮)分离;role 决定"谁能"(能力,见 `Permission`),settings 决定"此资源
|
||||
是否开某类操作"(策略)。本模块把 grant/settings 的结构钉死——`Permission` 已落 role 能
|
||||
力格,本模块补"授权如何挂到资源/主体上"。
|
||||
|
||||
principal 子类型学(user/chat/department/…)与各 policy 值域均为 `OPEN`(ADR 未定,非本
|
||||
层分歧点)。**role-capability 与 settings-policy 如何组合成最终授权决策**亦 `OPEN`——
|
||||
ADR-0004 把二者列为分离的闸,但未明文规定组合规则(AND?settings 能否超出 role?),实现
|
||||
须 surface,不得默认。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
variable (I : Identifiers)
|
||||
variable (ArtifactId Policy : Type)
|
||||
|
||||
/-- 受权限调控的资源(`PINNED` 三类, ADR-0004 `resource_type: project | artifact |
|
||||
project_group`);每类携带其 id,故 resource_id 由 resource_type 决定(结构无洞)。 -/
|
||||
inductive Resource where
|
||||
/-- 课程项目(`PINNED` 类别, ADR-0004)。 -/
|
||||
| project : I.ProjectId → Resource
|
||||
/-- 教研产物(`PINNED` 类别, ADR-0004;id 表示 `OPEN`,语义向 Courseware 半边对齐)。 -/
|
||||
| artifact : ArtifactId → Resource
|
||||
/-- 飞书项目群(`PINNED` 类别, ADR-0004 `project_group`;chat 标识见
|
||||
`Identifiers.ChatId`,绑定见 `ProjectGroup`)。 -/
|
||||
| projectGroup : I.ChatId → Resource
|
||||
|
||||
/-- 授权项(`PINNED` 结构, ADR-0004 `PermissionGrant`):把一个 role 授予一个 principal 对
|
||||
某个 resource。role 取自 `Permission.Role`(read/edit/manage 累积格)。principal 表示
|
||||
`OPEN`(子类型学未定,见 `Identifiers.Principal`)。 -/
|
||||
structure PermissionGrant where
|
||||
/-- 被授权的资源(`PINNED`, ADR-0004 `resource_id`)。 -/
|
||||
resource : Resource I ArtifactId
|
||||
/-- 被授权的主体(`PINNED` 字段/`OPEN` 表示, ADR-0004 `principal_id`;user/chat/
|
||||
department/user_group/app 子类型学未定)。 -/
|
||||
principal : I.Principal
|
||||
/-- 授予的角色(`PINNED`, ADR-0004 `role`;read⊂edit⊂manage 见 `Permission.Role`)。 -/
|
||||
role : Role
|
||||
|
||||
/-- 资源策略设置(`PINNED` 结构 + 六旋钮, ADR-0004 `PermissionSettings`):与 grant 分离,
|
||||
控制"此资源是否开某类操作"。六旋钮由 ADR 逐字列名;各旋钮值域 `OPEN`(ADR 未定,非本层
|
||||
分歧点)。共享同一 opaque `Policy` 类型:契约只钉死"旋钮存在且相互独立",不钉死"各旋钮
|
||||
值域互异"——值域是实现/后续 ADR 的事。 -/
|
||||
structure PermissionSettings where
|
||||
/-- 设置所属资源(`PINNED`, ADR-0004)。 -/
|
||||
resource : Resource I ArtifactId
|
||||
/-- 对外分享策略(`PINNED` 旋钮名, ADR-0004 `external_share_policy`;值域 `OPEN`)。 -/
|
||||
externalShare : Policy
|
||||
/-- 评论策略(`PINNED` 旋钮名, ADR-0004 `comment_policy`;值域 `OPEN`)。 -/
|
||||
comment : Policy
|
||||
/-- 复制/下载策略(`PINNED` 旋钮名, ADR-0004 `copy_download_policy`;值域 `OPEN`)。 -/
|
||||
copyDownload : Policy
|
||||
/-- 协作者管理策略(`PINNED` 旋钮名, ADR-0004 `collaborator_management_policy`;
|
||||
值域 `OPEN`)。 -/
|
||||
collaboratorMgmt : Policy
|
||||
/-- agent 触发策略(`PINNED` 旋钮名, ADR-0004 `agent_trigger_policy`;值域 `OPEN`。与
|
||||
`agentCancel` 分立——"谁能触发"≠"谁能取消",ADR-0004 故意拆开)。 -/
|
||||
agentTrigger : Policy
|
||||
/-- agent 取消策略(`PINNED` 旋钮名, ADR-0004 `agent_cancel_policy`;值域 `OPEN`。与
|
||||
`agentTrigger` 分立,见上)。 -/
|
||||
agentCancel : Policy
|
||||
|
||||
end Spec.System
|
||||
@@ -1,40 +0,0 @@
|
||||
import Spec.Prelude
|
||||
|
||||
/-!
|
||||
# ProjectGroup —— 飞书项目群作为协作空间(ADR-0001)
|
||||
|
||||
ADR-0001 的核心:一个 project 对应一个**长生命周期**飞书项目群;群是协作空间,**不是锁
|
||||
owner**(锁归 `AgentRun`,见 `Lock` / ADR-0002),不是临时处理 session。群可在无 Claude
|
||||
处理时保持开启;教师离群/静音与项目权限、与 Claude 生命周期相互独立。本模块钉死
|
||||
project↔group 的一对一绑定——likec4 画得出"project has group",画不出"恰好一个、且群
|
||||
不持锁"。
|
||||
|
||||
**群失效态与绑定快照(`OPEN`, ADR-0001 Consequences):** 群解散/归档/不可达时,
|
||||
`GroupBinding` 快照应变为 `none`(解绑、允许 rebind)还是保持 `some` 但指向失效 chat
|
||||
(悬挂、待管理员干预)未决策。ADR-0001 已点名 "rebinding or group archival needs
|
||||
explicit product rules";本模块只刻画健康态 1:1 不变式,不臆造失效态语义。实现遇到
|
||||
群解散必须 surface,不得默认任一方。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
variable (I : Identifiers)
|
||||
|
||||
/-- 飞书项目群(`PINNED` 长生命周期协作空间, ADR-0001)。承载 project 与飞书 chat 的绑定;
|
||||
**不是锁 owner**(锁归 `AgentRun`,见 `Lock`);不是临时 session。 -/
|
||||
structure ProjectGroup where
|
||||
/-- 群对应的飞书 chat(`PINNED` 关系, ADR-0001 "one project has one Feishu project
|
||||
group";chat 标识见 `Identifiers.ChatId`)。 -/
|
||||
chat : I.ChatId
|
||||
|
||||
/-- 项目↔群绑定表(`PINNED` 每项目至多一个群, ADR-0001)。`ProjectId → Option ChatId` 的
|
||||
结构本身即"一个 project 至多绑一个群"(由 `Option` 自带);良构补另一半——单射。 -/
|
||||
def GroupBinding := I.ProjectId → Option I.ChatId
|
||||
|
||||
/-- 绑定良构:**单射**——不同 project 不绑同一 chat(`PINNED` 1:1 的另一半, ADR-0001)。
|
||||
"每 project 至多一个群"由 `Option` 结构自带;这条钉死"每群至多属于一个 project"。群
|
||||
rebinding/archival 是生命周期事件(ADR-0001 Consequences),不在本快照不变式内。 -/
|
||||
def GroupBinding.WellFormed (b : GroupBinding I) : Prop :=
|
||||
∀ p₁ p₂ c, b p₁ = some c → b p₂ = some c → p₁ = p₂
|
||||
|
||||
end Spec.System
|
||||
+14
-20
@@ -1,28 +1,22 @@
|
||||
/-!
|
||||
# Run —— AgentRun 状态机
|
||||
import Spec.Prelude
|
||||
|
||||
一次 `@Claude` 创建一个 `AgentRun`(ADR-0001),它在终止时释放项目锁(ADR-0002)。
|
||||
合法转移关系在任何 ADR / likec4 散文里都未定下,故本模块只刻画**状态**与**终止
|
||||
判定**(后者是 Lock 排他不变式的依赖),不臆造转移边。
|
||||
/-!
|
||||
# Run —— AgentRun 的终止判定
|
||||
|
||||
一次 `@Claude` 创建一个 AgentRun(ADR-0001),它在终止时释放项目锁(ADR-0002)。
|
||||
|
||||
run 的具体状态集合没定(OPEN):ADR-0001..0003 列了一些状态名,但从未声明"状态恰好
|
||||
这些",实现若需新状态(如 pending)要提出来,不要默认已穷尽。所以这里不钉状态枚举,
|
||||
只钉一条契约需要的事实:一个 run 是否处于终止态。终止态由实现判定(状态集合本身未定,
|
||||
没法在契约里算)。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
/-- AgentRun 运行状态(状态名 `PINNED`, ADR-0001..0003 + likec4;**完整性 `OPEN`**
|
||||
——散文从未声明"状态恰好这些";实现若需新状态(如 pending)须 surface,不得默认
|
||||
本枚举已穷尽)。终止态见 `RunState.Terminal`。 -/
|
||||
inductive RunState where
|
||||
| active
|
||||
| waitingForUser
|
||||
| completed
|
||||
| failed
|
||||
| timedOut
|
||||
| canceled
|
||||
variable (I : Identifiers)
|
||||
|
||||
/-- run 处于**终止态**(`PINNED`, ADR-0002:锁在 completes/fails/timesOut/canceled
|
||||
时释放)。`active`/`waitingForUser` 非终止——后者仍占用项目(锁未释放)。 -/
|
||||
def RunState.Terminal : RunState → Prop
|
||||
| .completed | .failed | .timedOut | .canceled => True
|
||||
| .active | .waitingForUser => False
|
||||
/-- run 是否处于终止态(ADR-0002)。真值由实现给——状态集合未定(OPEN),故此处不钉
|
||||
具体状态名,只钉"存在终止与否的判定"。锁在 run 终止时释放(见 `Lock`)。 -/
|
||||
opaque Terminal : I.RunId → Prop
|
||||
|
||||
end Spec.System
|
||||
|
||||
Reference in New Issue
Block a user