forked from EduCraft/curriculum-project-hub
Compare commits
2 Commits
4234ba4c96
...
dc2d1c2f9e
| Author | SHA1 | Date | |
|---|---|---|---|
 hongjr03
|
dc2d1c2f9e | ||
|
hongjr03
|
3f9b60f692 |
@@ -1,12 +1,12 @@
|
||||
name: checker check
|
||||
|
||||
# Builds and lints the Rust implementation crates under crates/ (the rule-based
|
||||
# checker that "stands in Lean's position" at product runtime).
|
||||
# lesson checker).
|
||||
#
|
||||
# Like spec-check, this is an INTERNAL gate on the implementation's own health
|
||||
# (does it build, pass its tests, satisfy clippy + rustfmt?). It is NOT a
|
||||
# spec-to-implementation conformance gate — implementations align to the Lean
|
||||
# contract by human review, not by CI. See the repo README.
|
||||
# This is an INTERNAL gate on the implementation's own health
|
||||
# (does it build, pass its tests, satisfy clippy + rustfmt?). There is no
|
||||
# decision-to-implementation conformance gate — implementations align to the
|
||||
# ADRs by human review, not by CI. See the repo README.
|
||||
|
||||
on:
|
||||
push:
|
||||
|
||||
@@ -1,8 +1,8 @@
|
||||
name: hub check
|
||||
|
||||
# Builds, type-checks, and tests the Hub TS package under hub/.
|
||||
# The Hub is the Feishu-group collaboration + agent runtime half
|
||||
# (spec/System implementation). This is an INTERNAL gate on the Hub's own
|
||||
# The Hub is the Feishu-group collaboration + agent runtime half.
|
||||
# This is an INTERNAL gate on the Hub's own
|
||||
# health, like checker-check is for the Rust half.
|
||||
|
||||
on:
|
||||
|
||||
@@ -1,20 +0,0 @@
|
||||
name: spec check
|
||||
|
||||
# Builds the Lean semantic master spec under spec/.
|
||||
# This is an INTERNAL well-formedness gate (does the contract type-check?),
|
||||
# NOT a spec-to-implementation conformance gate — implementations align to the
|
||||
# contract by human review, not by CI. See repo README.
|
||||
|
||||
on:
|
||||
push:
|
||||
pull_request:
|
||||
workflow_dispatch:
|
||||
|
||||
jobs:
|
||||
spec-check:
|
||||
runs-on: ubuntu-latest
|
||||
steps:
|
||||
- uses: actions/checkout@v5
|
||||
- uses: leanprover/lean-action@v1
|
||||
with:
|
||||
lake-package-directory: spec
|
||||
@@ -1,7 +1,3 @@
|
||||
# Lean / Lake build artifacts (spec/ has its own .gitignore too)
|
||||
.lake/
|
||||
**/.lake/
|
||||
|
||||
# Rust / Cargo build artifacts (repo-wide cargo workspace at root)
|
||||
/target
|
||||
**/*.pdf
|
||||
|
||||
@@ -29,7 +29,7 @@ workload brakes.
|
||||
|
||||
The full current-state inventory, accepted behavior, and release evidence are
|
||||
recorded in [Initial abuse and capacity controls](../assets/initial-abuse-capacity-controls.md),
|
||||
with the durable decision in ADR-0022 and `Spec.System.Capacity`. Numerical
|
||||
with the durable decision in ADR-0022. Numerical
|
||||
ceilings remain open until production-like calibration.
|
||||
|
||||
The implementation frontier is:
|
||||
|
||||
@@ -7,6 +7,6 @@ Blocked by: 01, 02, 03, 04, 05, 06, 07, 09, 10, 11, 12, 13, 14, 15, 16, 17, 18,
|
||||
## Question
|
||||
|
||||
After the readiness investigations and resulting fixes are resolved, can one
|
||||
repeatable release procedure prove build/test/spec health, deploy a clean
|
||||
repeatable release procedure prove build/test health, deploy a clean
|
||||
production-like environment, exercise critical tenant and agent journeys,
|
||||
verify observability and recovery, and either roll forward or roll back safely?
|
||||
|
||||
@@ -8,7 +8,7 @@ Blocked by: 04
|
||||
|
||||
Separate or unify run-bound audit entries, pre-run security/permission events,
|
||||
structured messages, and operational recovery events without weakening
|
||||
`Spec.System.Audit`'s pinned AuditEntry-to-run relation. Decide durability,
|
||||
the pinned AuditEntry-to-run relation. Decide durability,
|
||||
failure, retention, and query semantics; then enforce referential integrity and
|
||||
observable/recoverable writes instead of silently swallowing lost evidence.
|
||||
Do not merge these customer Project/Run records with ADR-0023's already-decided
|
||||
|
||||
+1
-3
@@ -40,9 +40,7 @@ an off-host recovery key, an incident and reason, and issues only an expiring
|
||||
Emergency Platform Grant.
|
||||
|
||||
The complete accepted decision and implementation divergences are in
|
||||
[ADR-0023](../../../docs/adr/0023-platform-administrator-identity-and-audit.md).
|
||||
The pinned semantic invariants are in
|
||||
[`Spec.System.PlatformAdministration`](../../../spec/Spec/System/PlatformAdministration.lean),
|
||||
[ADR-0023](../../../docs/adr/0023-platform-administrator-identity-and-audit.md),
|
||||
and the canonical terms are in [`CONTEXT.md`](../../../CONTEXT.md).
|
||||
|
||||
Exact numeric session/invitation/step-up limits and browser mechanics remain
|
||||
|
||||
@@ -1,29 +1,25 @@
|
||||
# AGENTS.md —— agent 操作手册(全 repo)
|
||||
|
||||
本 repo 是 monorepo。先读根 `README.md` 的"宪法"5 条,那是一切工作的前提。本文件是给在这里干活的 coding agent 的纪律。
|
||||
本 repo 是 monorepo。先读根 `README.md` 的"宪法"4 条,那是一切工作的前提。本文件是给在这里干活的 coding agent 的纪律。
|
||||
|
||||
## 这个 repo 是什么
|
||||
|
||||
- `spec/` 是一份**人机共识的契约**(Lean 语义母本),是产品语义的上游参照。
|
||||
- 其余部件(将来的 `spec/` 外文件夹)是**向 `spec/` 对齐的实现**。
|
||||
- `docs/adr/` 是系统级决策的唯一权威来源;`CONTEXT.md` 是平台语言词汇表;代码注释把关键不变量锚到 ADR 编号,可 grep。
|
||||
- `hub/` 的平台层按 SaaS 形态演进:`Organization` 是 tenant root;`Project`/`Team`
|
||||
必须归属 org,TEAM→PROJECT 授权不得跨 org(见 ADR-0020 / `Spec.System.Organization`)。
|
||||
必须归属 org,TEAM→PROJECT 授权不得跨 org(见 ADR-0020)。
|
||||
- org 后台 project explorer 里 `Folder` 是透明组织节点,不是权限资源;project 仍是权限边界。
|
||||
普通老师可在飞书群自助建 project 但受 org policy 控制(见 ADR-0021 /
|
||||
`Spec.System.ProjectWorkspace`)。
|
||||
普通老师可在飞书群自助建 project 但受 org policy 控制(见 ADR-0021)。
|
||||
- 每个 org 自选 BYOK 或平台托管 model provider connection;平台托管也必须是该 org
|
||||
独享的 key/base URL,不得让无关 org 共用 process-global provider key(见 ADR-0021 /
|
||||
`Spec.System.Organization`)。
|
||||
独享的 key/base URL,不得让无关 org 共用 process-global provider key(见 ADR-0021)。
|
||||
- Feishu/provider secret 使用本地版本化 master-key keyring 的信封加密;生产由 systemd
|
||||
credential 注入,运行时只允许显式 org/project scope 的 fail-closed resolver,不得回退
|
||||
process-global credential;Agent child 只接收 run-scoped loopback proxy capability,
|
||||
不接收 org provider credential(见 ADR-0024 / `Spec.System.Organization`)。
|
||||
不接收 org provider credential(见 ADR-0024)。
|
||||
- 生产容量按不可突破的 platform ceiling 与 org 可下调 policy 分层;有效限制取两者较低值。
|
||||
Agent admission 必须持久、有界、跨 org 公平且显式背压(见 ADR-0022 /
|
||||
`Spec.System.Capacity`)。
|
||||
Agent admission 必须持久、有界、跨 org 公平且显式背压(见 ADR-0022)。
|
||||
- 平台管理员只通过独立的 platform-owned 飞书应用与可撤销 Platform Session 认证,不复用
|
||||
客户 `User`/org membership;平台写操作与 append-only audit 同事务,break-glass 只走
|
||||
双因子的离线恢复流程(见 ADR-0023 / `Spec.System.PlatformAdministration`)。
|
||||
双因子的离线恢复流程(见 ADR-0023)。
|
||||
- 受控 alpha 暂采用一 Organization 一具名 systemd Silo:独立 database role/database、
|
||||
service identity、workspace、keyring 与 Feishu/provider connection；进程必须由
|
||||
`HUB_SILO_ORGANIZATION_ID` fail-closed 绑定唯一 org，平台后台不开放。共享 SaaS
|
||||
@@ -44,12 +40,12 @@
|
||||
|
||||
## 纪律
|
||||
|
||||
1. **不得用预训练先验脑补本领域。** 这个领域很新,你没有相关先验。契约里 prose doc 注释是语义的唯一权威来源;契约没写的,就是没定的。
|
||||
1. **不得用预训练先验脑补本领域。** 这个领域很新,你没有相关先验。ADR 与 `CONTEXT.md` 是语义的唯一权威来源;没写的,就是没定的。
|
||||
|
||||
2. **凡契约未写明者,不得假设。** 遇到标了 `OPEN` 的地方,或契约根本没覆盖的地方,**显式 surface 出来**让开发者决定,绝不擅自替它选一个解。
|
||||
2. **凡 ADR 未写明者,不得假设。** 遇到没覆盖的地方,**显式 surface 出来**让开发者决定,绝不擅自替它选一个解。
|
||||
|
||||
3. **改 `spec/` 必须保持其 `lake build` 通过。** 在 `spec/` 目录下跑 `lake build`。新增声明必须带 `/-- … -/` doc 注释和恰当标签(`PINNED` / `OPEN` / `ADR-NNNN`)。规范见 `spec/README.md`。不准用 `sorry` 把 build 糊绿。
|
||||
3. **新语义决策进 ADR。** 跨部件的语义分歧点按编号顺延新增 `docs/adr/NNNN-*.md`;代码里的关键不变量用注释锚到 ADR 编号,保持可 grep。已有 ADR 正文不改写历史——推翻旧决策就写新 ADR 标记 supersede。
|
||||
|
||||
4. **实现向契约对齐;偏离必须 surface。** 没有 CI gate 替你把关 spec↔实现的一致性(见宪法第 2 条)——这道对齐靠 review 和你巡逻 diff。发现实现与契约不一致时,报告它,不要默默让其中一边将就另一边。
|
||||
4. **实现向 ADR 对齐;偏离必须 surface。** 没有 CI gate 替你把关 ADR↔实现的一致性(见宪法第 2 条)——这道对齐靠 review 和你巡逻 diff。发现实现与决策不一致时,报告它,不要默默让其中一边将就另一边。
|
||||
|
||||
5. **写操作谨慎。** 线上操作、git 写操作前与开发者确认(这是开发者的全局偏好)。
|
||||
|
||||
@@ -1,25 +1,23 @@
|
||||
# CLAUDE.md —— agent 操作手册(全 repo)
|
||||
|
||||
本 repo 是 monorepo。先读根 `README.md` 的"宪法"5 条,那是一切工作的前提。本文件是给在这里干活的 coding agent 的纪律。
|
||||
本 repo 是 monorepo。先读根 `README.md` 的"宪法"4 条,那是一切工作的前提。本文件是给在这里干活的 coding agent 的纪律。
|
||||
|
||||
## 这个 repo 是什么
|
||||
|
||||
- `spec/` 是一份**人机共识的契约**(Lean 语义母本),是产品语义的上游参照。
|
||||
- 其余部件(将来的 `spec/` 外文件夹)是**向 `spec/` 对齐的实现**。
|
||||
- `docs/adr/` 是系统级决策的唯一权威来源;`CONTEXT.md` 是平台语言词汇表;代码注释把关键不变量锚到 ADR 编号,可 grep。
|
||||
- `hub/` 的平台层按 SaaS 形态演进:`Organization` 是 tenant root;`Project`/`Team`
|
||||
必须归属 org,TEAM→PROJECT 授权不得跨 org(见 ADR-0020 / `Spec.System.Organization`)。
|
||||
必须归属 org,TEAM→PROJECT 授权不得跨 org(见 ADR-0020)。
|
||||
- org 后台 project explorer 里 `Folder` 是透明组织节点,不是权限资源;project 仍是权限边界。
|
||||
普通老师可在飞书群自助建 project 但受 org policy 控制(见 ADR-0021 /
|
||||
`Spec.System.ProjectWorkspace`)。
|
||||
普通老师可在飞书群自助建 project 但受 org policy 控制(见 ADR-0021)。
|
||||
|
||||
## 纪律
|
||||
|
||||
1. **不得用预训练先验脑补本领域。** 这个领域很新,你没有相关先验。契约里 prose doc 注释是语义的唯一权威来源;契约没写的,就是没定的。
|
||||
1. **不得用预训练先验脑补本领域。** 这个领域很新,你没有相关先验。ADR 与 `CONTEXT.md` 是语义的唯一权威来源;没写的,就是没定的。
|
||||
|
||||
2. **凡契约未写明者,不得假设。** 遇到标了 `OPEN` 的地方,或契约根本没覆盖的地方,**显式 surface 出来**让开发者决定,绝不擅自替它选一个解。
|
||||
2. **凡 ADR 未写明者,不得假设。** 遇到没覆盖的地方,**显式 surface 出来**让开发者决定,绝不擅自替它选一个解。
|
||||
|
||||
3. **改 `spec/` 必须保持其 `lake build` 通过。** 在 `spec/` 目录下跑 `lake build`。新增声明必须带 `/-- … -/` doc 注释和恰当标签(`PINNED` / `OPEN` / `ADR-NNNN`)。规范见 `spec/README.md`。不准用 `sorry` 把 build 糊绿。
|
||||
3. **新语义决策进 ADR。** 跨部件的语义分歧点按编号顺延新增 `docs/adr/NNNN-*.md`;代码里的关键不变量用注释锚到 ADR 编号,保持可 grep。已有 ADR 正文不改写历史——推翻旧决策就写新 ADR 标记 supersede。
|
||||
|
||||
4. **实现向契约对齐;偏离必须 surface。** 没有 CI gate 替你把关 spec↔实现的一致性(见宪法第 2 条)——这道对齐靠 review 和你巡逻 diff。发现实现与契约不一致时,报告它,不要默默让其中一边将就另一边。
|
||||
4. **实现向 ADR 对齐;偏离必须 surface。** 没有 CI gate 替你把关 ADR↔实现的一致性(见宪法第 2 条)——这道对齐靠 review 和你巡逻 diff。发现实现与决策不一致时,报告它,不要默默让其中一边将就另一边。
|
||||
|
||||
5. **写操作谨慎。** 线上操作、git 写操作前与开发者确认(这是开发者的全局偏好)。
|
||||
|
||||
@@ -2,7 +2,7 @@
|
||||
|
||||
教研生产的数字化解决方案。核心思路:课程像 DAW / 剪辑软件那样有一个**结构化的工程文件**;coding agent 协助编辑它;一个 rule-based checker(类编译器)校验其合法性并给出 helpful fix hint。目标是把教研从一次性的文档,沉淀成**可累积、可校验、可复用的资产**。
|
||||
|
||||
这是一个 **monorepo**。它的组织方式本身就表达了一条原则:**`spec/` 是上游的语义母本,其余部件是向它对齐的实现。**
|
||||
这是一个 **monorepo**。它的组织方式本身就表达了一条原则:**`docs/adr/` 是系统级决策的唯一权威来源,代码注释把关键不变量锚到 ADR 编号,可 grep。**
|
||||
|
||||
## 安装 `cph` 命令行
|
||||
|
||||
@@ -33,47 +33,40 @@ cph completions zsh > ~/.zfunc/_cph # 或 bash/fish/powershell/elvish
|
||||
```
|
||||
README.md ← 本文件:总览 + 宪法(下面 5 条)
|
||||
CLAUDE.md ← 全局 agent 操作手册(管整个 repo)
|
||||
docs/adr/ ← 系统级架构决策记录(跨部件,被 spec 契约引用)
|
||||
spec/ ← Lean 语义母本(自包含的 Lean 工程)。见 spec/README.md
|
||||
docs/adr/ ← 系统级架构决策记录(跨部件,决策的唯一权威来源)
|
||||
CONTEXT.md ← 平台语言词汇表(术语与禁用说法)
|
||||
Cargo.toml ← 仓库级 cargo workspace(实现部件共用,便于跨部件复用 crate)
|
||||
crates/ ← 实现:rule-based checker(向 spec 对齐)。见 crates/README.md
|
||||
crates/ ← 实现:rule-based checker(语义由 ADR 锚定)。见 crates/README.md
|
||||
cph-diag / cph-model / cph-schema / cph-typst ← 可复用基础(模型/校验/typst 引擎)
|
||||
cph-check / cph-cli ← checker 本体 + `cph` 命令行
|
||||
render/ ← typst 渲染包 cph-render(母本的渲染后端之一,ADR-0005)
|
||||
render/ ← typst 渲染包 cph-render(checker 的渲染后端,ADR-0005)
|
||||
examples/ ← 样例工程文件(如 TH-141),流水线的真实输入
|
||||
hub/ ← SaaS Hub:飞书协作、org 管理、agent runtime 与生产部署
|
||||
(exporter/ …) ← 将来的其他部件,平级于 spec/
|
||||
(exporter/ …) ← 将来的其他部件,平级于 crates/
|
||||
```
|
||||
|
||||
`spec/` 与实现部件**物理分离、平级共存**:谁是上游、谁向谁对齐,一眼可见。
|
||||
实现部件共用一个仓库根的 cargo workspace,使基础 crate(模型、typst 引擎)能被
|
||||
未来部件(如 exporter)复用,而非各自重造。
|
||||
|
||||
## 宪法
|
||||
|
||||
这 5 条是 `spec/` 这份语义母本的定位与约束,是本仓库一切工作的前提。
|
||||
这 4 条是本仓库的协作约定,是一切工作的前提。
|
||||
|
||||
1. **角色 —— Lean 是研发侧的上游参照。**
|
||||
`spec/` 用 Lean 编写,是开发者(领域专家)与 coding agent **共用**的 spec 工具,用来沉淀产品各部件的**语义**。它**不进入产品运行时**——产品里"站在 Lean 这个位置"的那个 checker 用什么技术实现,尚未决定;但那个东西的语义,先在 `spec/` 里固定下来。
|
||||
1. **角色 —— ADR 是决策真相。**
|
||||
跨部件的语义决策只记录在 `docs/adr/`,一份决策一份 ADR,编号顺延、正文不改写历史。代码里的关键不变量用注释锚到 ADR 编号,保持可 grep。没有第二份权威文档。
|
||||
|
||||
2. **对齐机制 —— Lean 只做上游参照。**
|
||||
不做 extract / codegen,不派生 conformance test,CI 里**没有** spec→实现的 gate。实现对齐 spec,由"开发者 review + agent 巡逻 diff"这个人肉环节承载。
|
||||
(CI 里的 `spec check` 只验 spec **自身**能否 type-check,即契约内部良构,不是 spec↔实现的对齐检查。)
|
||||
2. **对齐机制 —— 人肉承载,无机器兜底。**
|
||||
CI 只验各部件自身良构(build / test / clippy),**没有**决策↔实现的一致性 gate。实现对齐 ADR,由"开发者 review + agent 巡逻 diff"这个人肉环节承载。发现漂移,报告它,不要默默让其中一边将就另一边。
|
||||
|
||||
3. **资产性 —— 由 review 纪律承载,无机器兜底。**
|
||||
这份仓库给你的是"精确、自洽、机器验内部良构的语义共识",**不是**"实现正确性保证"。spec 与实现之间那道缝,是我们自愿用人来守的——清醒地守,它就是资产;放任实现漂移而不回头同步,它就退化成最贵的过期文档。
|
||||
3. **形态 —— 自包含。**
|
||||
凡 ADR 未明文规定的,开发者与 agent 双方都不该假设;遇到没覆盖的地方,**显式 surface** 出来让开发者决定。
|
||||
|
||||
4. **形态 —— 它是人机共识的契约。**
|
||||
契约必须**自包含**:凡契约未明文规定的,开发者与 agent 双方都不该假设。这比"文档"严格——type checker 会逼这份契约在结构上无洞。
|
||||
|
||||
5. **深度判据 —— 只收录分歧点。**
|
||||
一条语义该不该写进 Lean,取决于一句话:**"不写明,开发者与 agent 会不会各自做出不同假设?"** 会 → 进契约;显然的东西 / 纯 plumbing / 普通 CRUD 字段 → 不进(写进去只稀释信噪比、增加维护面)。
|
||||
深度上限不是 Lean 的表达力,而是**你愿意在每次实现变更时手动回头同步的量**——写得比你能维护的更深,多出来的部分会率先过期、反过来误导实现。
|
||||
4. **深度判据 —— 只收录分歧点。**
|
||||
一条语义该不该写进 ADR,取决于一句话:**"不写明,开发者与 agent 会不会各自做出不同假设?"** 会 → 进 ADR;显然的东西 / 纯 plumbing / 普通 CRUD 字段 → 不进(写进去只稀释信噪比、增加维护面)。
|
||||
深度上限是**你愿意在每次实现变更时手动回头同步的量**——写得比你能维护的更深,多出来的部分会率先过期、反过来误导实现。
|
||||
|
||||
## CI
|
||||
|
||||
`.gitea/workflows/spec-check.yml` 在每次 push / PR 时于 `spec/` 下跑 `lake build`,确保契约始终 type-check 通过(从第一天起就是"绿"的)。这是良构 gate,见宪法第 2 条。
|
||||
|
||||
Rust checker 的本地与 CI 工具链由根 `rust-toolchain.toml` 固定;`.gitea/workflows/checker-check.yml`
|
||||
必须安装同一精确版本并执行 `cargo fmt --all --check`、Clippy `-D warnings` 与 workspace
|
||||
全测试。升级 Rust 时这两处必须在同一提交更新并通过完整 checker gate。
|
||||
|
||||
+3
-2
@@ -1,7 +1,8 @@
|
||||
# crates/
|
||||
|
||||
These crates implement the rule-based lesson checker that aligns to the
|
||||
semantic master in `spec/`: it reads an engineering-file (one lesson, ADR-0005)
|
||||
These crates implement the rule-based lesson checker whose semantics are
|
||||
pinned by the ADRs in `docs/adr/`: it reads an engineering-file (one lesson,
|
||||
ADR-0005)
|
||||
laid out per ADR-0008 (declarative `manifest.toml` + per-element
|
||||
`element.toml`), validates structure and content, and emits diagnostics.
|
||||
`cph-diag` (the shared diagnostic vocabulary), `cph-model` (the ADR-0008 loader),
|
||||
|
||||
@@ -19,13 +19,11 @@ const DEFAULT_TARGET: &str = "student";
|
||||
|
||||
/// Severity of the render-coverage ("element ignored under a target") diagnostic.
|
||||
///
|
||||
/// **PINNED to `warning` by the contract.** Mirrors the Lean master's
|
||||
/// `Spec.Courseware.renderIgnoredSeverity : Severity := .warning`
|
||||
/// (`spec/Spec/Courseware/Check/Diagnostic.lean`), itself citing ADR-0005: when a
|
||||
/// **PINNED to `warning` by ADR-0005:** when a
|
||||
/// `(kind, target)` pair has no render rule the checker reports that the element
|
||||
/// is ignored under that target and **does not block the export**. Naming the
|
||||
/// severity as a const makes "it is a warning, not an error" a greppable,
|
||||
/// alignable fact rather than an inline literal.
|
||||
/// severity as a const makes "it is a warning, not an error" a greppable
|
||||
/// fact rather than an inline literal.
|
||||
const RENDER_IGNORED_SEVERITY: Severity = Severity::Warning;
|
||||
|
||||
/// The result of running [`check`] (or the check phases of [`build`]).
|
||||
@@ -57,12 +55,12 @@ impl CheckReport {
|
||||
|
||||
/// Whether any collected diagnostic is `Error`-severity.
|
||||
///
|
||||
/// **Legality decision (spec alignment).** `!has_errors()` is the
|
||||
/// implementation of `Spec.Courseware.Legal` (`spec/Spec/Courseware/Check/Diagnostic.lean`):
|
||||
/// a lesson is *legal* iff its diagnostics contain no error-level diagnostic
|
||||
/// (warnings are non-blocking — see `Severity` / ADR-0010). There is no CI
|
||||
/// gate enforcing this alignment (repo constitution); it is kept greppable
|
||||
/// here so a reviewer can tie the orchestrator's gate to the Lean master.
|
||||
/// **Legality decision (ADR-0010).** `!has_errors()` decides lesson
|
||||
/// legality: a lesson is *legal* iff its diagnostics contain no error-level
|
||||
/// diagnostic (warnings are non-blocking — see `Severity`). There is no CI
|
||||
/// gate enforcing ADR↔implementation alignment (repo constitution); it is
|
||||
/// kept greppable here so a reviewer can tie the orchestrator's gate to
|
||||
/// the ADR.
|
||||
pub fn has_errors(&self) -> bool {
|
||||
self.diagnostics
|
||||
.iter()
|
||||
|
||||
+10
-15
@@ -2,7 +2,7 @@
|
||||
//!
|
||||
//! Every other crate in the workspace depends on these types to report
|
||||
//! problems. The vocabulary is intentionally small and stable: a [`Severity`]
|
||||
//! (mirroring the Lean master), a closed set of machine-stable [`DiagCode`]s, an
|
||||
//! (two-valued, ADR-0010), a closed set of machine-stable [`DiagCode`]s, an
|
||||
//! optional [`SourceSpan`] pointing back at the offending source, and a
|
||||
//! [`Diagnostic`] tying them together with a human message and a fix hint.
|
||||
//!
|
||||
@@ -17,32 +17,27 @@ use serde::Serialize;
|
||||
|
||||
/// Severity of a diagnostic.
|
||||
///
|
||||
/// **Mirrors `Spec.Courseware.Diagnostic.Severity`** in the Lean semantic
|
||||
/// master (`spec/Spec/Courseware/Check/Diagnostic.lean`), whose definition is
|
||||
/// exactly:
|
||||
/// **Pinned by ADR-0005 / ADR-0010: exactly two values.**
|
||||
///
|
||||
/// ```text
|
||||
/// inductive Severity where
|
||||
/// | warning
|
||||
/// | error
|
||||
/// warning | error
|
||||
/// ```
|
||||
///
|
||||
/// This two-valued shape is a **contract decision**, not an accident: the Lean
|
||||
/// module pins `Severity` to exactly `warning | error` and states the finer
|
||||
/// levels (`info` / `hint` / `note`) are deliberately undecided. We therefore
|
||||
/// This two-valued shape is a **contract decision**, not an accident: the
|
||||
/// finer levels (`info` / `hint` / `note`) are deliberately undecided, so we
|
||||
/// do **not** add an info/note level here. `error` blocks (the artifact is
|
||||
/// invalid); `warning` does not block (the artifact still exports, but with
|
||||
/// loss / an ignored element — e.g. ADR-0005's "missing render ⇒ warning").
|
||||
///
|
||||
/// There is no CI gate enforcing this alignment (see the repo constitution);
|
||||
/// it is maintained by review, which is why this correspondence is documented
|
||||
/// here rather than only in the spec.
|
||||
/// There is no CI gate enforcing ADR↔implementation alignment (see the repo
|
||||
/// constitution); it is maintained by review, which is why the decision is
|
||||
/// documented here rather than only in the ADR.
|
||||
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
|
||||
pub enum Severity {
|
||||
/// Non-blocking: the artifact still exports, but is lossy / has an ignored
|
||||
/// element. Mirrors Lean `Severity.warning`.
|
||||
/// element. ADR-0010 `warning`.
|
||||
Warning,
|
||||
/// Blocking: the artifact is invalid. Mirrors Lean `Severity.error`.
|
||||
/// Blocking: the artifact is invalid. ADR-0010 `error`.
|
||||
Error,
|
||||
}
|
||||
|
||||
|
||||
+25
-38
@@ -3,9 +3,7 @@
|
||||
//! This crate is the **loader**, not the full checker. It reads
|
||||
//! `<root>/manifest.toml` (project / info / ordered `[[parts]]` / declared
|
||||
//! `[targets.*]`) and each part's `<root>/<path>/element.toml`, and produces an
|
||||
//! ordered [`Lesson`] — mirroring the Lean master's `Lesson = List (Element P)`
|
||||
//! (`spec/Spec/Courseware/Model/Lesson.lean`), where the order of `parts` carries
|
||||
//! teaching semantics.
|
||||
//! ordered [`Lesson`], where the order of `parts` carries teaching semantics.
|
||||
//!
|
||||
//! Scope boundaries (deliberately staying in lane):
|
||||
//! - It validates **structure** only: manifest shape, element.toml shape, and
|
||||
@@ -23,7 +21,7 @@ use serde::{Deserialize, Serialize};
|
||||
|
||||
/// An ordered, in-memory lesson loaded from an engineering file.
|
||||
///
|
||||
/// Mirrors the Lean master's `Lesson = List (Element P)`: `parts` is an ordered
|
||||
/// `parts` is an ordered
|
||||
/// `Vec`, and that order is the lesson's order (ADR-0008 §"the lesson manifest
|
||||
/// is declarative" — the `[[parts]]` array order is the single source of truth).
|
||||
#[derive(Debug, Clone, PartialEq, Serialize)]
|
||||
@@ -86,9 +84,8 @@ pub struct TargetConfig {
|
||||
/// with template `exports/<name>.typ` when no `[[steps]]` are given.
|
||||
pub steps: Vec<Step>,
|
||||
/// The **render-coverage declaration**: which element kinds this target
|
||||
/// renders. Realizes `Spec.Courseware.TargetSpec.covers : KindId → Prop`
|
||||
/// (`spec/Spec/Courseware/Export/Render.lean`) and ADR-0011's "render
|
||||
/// coverage is a declaration, not a payload": the contract keeps *which
|
||||
/// renders. Realizes ADR-0011's "render
|
||||
/// coverage is a declaration, not a payload": the declaration keeps *which
|
||||
/// kinds a target renders* (used by the `renderIgnored` seed diagnostic),
|
||||
/// while the rendering "how" lives in the template/steps.
|
||||
///
|
||||
@@ -102,13 +99,10 @@ pub struct TargetConfig {
|
||||
|
||||
/// The artifact an export target produces (ADR-0009/0011).
|
||||
///
|
||||
/// **Mirrors `Spec.Courseware.Artifact`** in the Lean semantic master
|
||||
/// (`spec/Spec/Courseware/Export/Artifact.lean`), whose definition is exactly:
|
||||
/// **Pinned by ADR-0011** as an ADT with fields:
|
||||
///
|
||||
/// ```text
|
||||
/// inductive Artifact where
|
||||
/// | singleFile (filepath : String)
|
||||
/// | fileTree (root : String) (outputs : String)
|
||||
/// Artifact = singleFile (filepath) | fileTree (root, outputs)
|
||||
/// ```
|
||||
///
|
||||
/// ADR-0011 pinned the artifact as an ADT **with fields**: "what the product
|
||||
@@ -120,20 +114,20 @@ pub struct TargetConfig {
|
||||
/// `"single-file"` → [`Artifact::SingleFile`], `"file-tree"` →
|
||||
/// [`Artifact::FileTree`].
|
||||
///
|
||||
/// As with `cph-diag`'s `Severity`, there is no CI gate enforcing this
|
||||
/// alignment (see the repo constitution) — it is maintained by review, which is
|
||||
/// why the correspondence is documented here.
|
||||
/// As with `cph-diag`'s `Severity`, there is no CI gate enforcing ADR↔
|
||||
/// implementation alignment (see the repo constitution) — it is maintained by
|
||||
/// review, which is why the decision is documented here.
|
||||
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
|
||||
pub enum Artifact {
|
||||
/// One bundled document landing at `filepath` (relative to the engineering
|
||||
/// root). Mirrors Lean `Artifact.singleFile`. The default artifact shape.
|
||||
/// root). ADR-0011 `singleFile`. The default artifact shape.
|
||||
SingleFile {
|
||||
/// Where the single product is written (relative to the engineering
|
||||
/// root), e.g. `build/student.pdf`.
|
||||
filepath: PathBuf,
|
||||
},
|
||||
/// A set of files under `root` matching the `outputs` glob. Mirrors Lean
|
||||
/// `Artifact.fileTree`.
|
||||
/// A set of files under `root` matching the `outputs` glob. ADR-0011
|
||||
/// `fileTree`.
|
||||
FileTree {
|
||||
/// The output directory (relative to the engineering root).
|
||||
root: PathBuf,
|
||||
@@ -156,14 +150,10 @@ impl Artifact {
|
||||
|
||||
/// One typed build step (ADR-0011).
|
||||
///
|
||||
/// **Mirrors `Spec.Courseware.Step`** in the Lean semantic master
|
||||
/// (`spec/Spec/Courseware/Export/Render.lean`), whose definition is exactly:
|
||||
/// **Pinned by ADR-0011** as an ADT:
|
||||
///
|
||||
/// ```text
|
||||
/// inductive Step where
|
||||
/// | typstCompile (template : String)
|
||||
/// | shell (run : String)
|
||||
/// | assembleMarkdown (field : String)
|
||||
/// Step = typstCompile (template) | shell (run) | assembleMarkdown (field)
|
||||
/// ```
|
||||
///
|
||||
/// A step is a *typed* operation (extensible): `TypstCompile` compiles a
|
||||
@@ -183,20 +173,20 @@ impl Artifact {
|
||||
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
|
||||
pub enum Step {
|
||||
/// Compile a template file (relative to the engineering root) into the
|
||||
/// artifact; the framework injects the manifest. Mirrors Lean
|
||||
/// `Step.typstCompile`.
|
||||
/// artifact; the framework injects the manifest. ADR-0011
|
||||
/// `typstCompile`.
|
||||
TypstCompile {
|
||||
/// The template file to compile as main, e.g. `exports/student.typ`.
|
||||
template: PathBuf,
|
||||
},
|
||||
/// Run a shell command — the escape hatch. Mirrors Lean `Step.shell`.
|
||||
/// Run a shell command — the escape hatch. ADR-0011 `shell`.
|
||||
Shell {
|
||||
/// The command line to run.
|
||||
run: String,
|
||||
},
|
||||
/// Assemble a single-file markdown deliverable by concatenating each
|
||||
/// element's `field` markdown content file in `[[parts]]` order. Mirrors
|
||||
/// Lean `Step.assembleMarkdown` (ADR-0015). Not a typst build — the
|
||||
/// element's `field` markdown content file in `[[parts]]` order. ADR-0011
|
||||
/// `assembleMarkdown` (ADR-0015). Not a typst build — the
|
||||
/// framework owns the read/concatenate/write itself.
|
||||
AssembleMarkdown {
|
||||
/// The per-element markdown content field to assemble (e.g. `slides`,
|
||||
@@ -226,12 +216,11 @@ pub struct Project {
|
||||
|
||||
/// `[info]` table (passed through to render targets verbatim).
|
||||
///
|
||||
/// **Mirrors `Spec.Courseware.Info`** in the Lean semantic master
|
||||
/// (`spec/Spec/Courseware/Model/Info.lean`): the *canonical* model whose
|
||||
/// The *canonical* model whose
|
||||
/// `authors` is always a list. The authoring-surface form (string-or-array
|
||||
/// `author`) is the separate [`RawInfo`] / [`RawAuthor`], normalized into this
|
||||
/// at the load boundary — mirroring the Lean `RawInfo` / `RawAuthor` split. No
|
||||
/// CI gate enforces this alignment (repo constitution); it is kept greppable.
|
||||
/// at the load boundary. No
|
||||
/// CI gate enforces ADR↔implementation alignment (repo constitution); it is kept greppable.
|
||||
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
|
||||
pub struct Info {
|
||||
/// Lesson title.
|
||||
@@ -240,7 +229,6 @@ pub struct Info {
|
||||
/// so this is a list, not a single name. Empty when `[info]` declares no
|
||||
/// `author`. The on-disk `author` accepts either a bare string (one author)
|
||||
/// or an array of strings (see [`RawAuthor`]); both load into this `Vec`.
|
||||
/// Mirrors Lean `Info.authors : List String`.
|
||||
pub authors: Vec<String>,
|
||||
}
|
||||
|
||||
@@ -290,8 +278,7 @@ struct RawProject {
|
||||
name: String,
|
||||
}
|
||||
|
||||
/// The authoring-surface `[info]` (mirrors Lean `RawInfo` in
|
||||
/// `spec/Spec/Courseware/Model/Info.lean`): the raw form that exists for
|
||||
/// The authoring-surface `[info]`: the raw form that exists for
|
||||
/// fill-in convenience, normalized into the canonical [`Info`] at the load
|
||||
/// boundary. Not the form the rest of the model traffics in.
|
||||
#[derive(Debug, Deserialize)]
|
||||
@@ -301,7 +288,7 @@ struct RawInfo {
|
||||
}
|
||||
|
||||
/// On-disk `author`: either a single name (`author = "…"`) or a list
|
||||
/// (`author = ["…", "…"]`). Mirrors Lean `RawAuthor`: a fill-in convenience whose
|
||||
/// (`author = ["…", "…"]`). A fill-in convenience whose
|
||||
/// string-or-array union lives **only** at the load boundary — [`RawAuthor::into_vec`]
|
||||
/// folds it into the canonical [`Info::authors`] `Vec`, after which it never appears.
|
||||
#[derive(Debug, Deserialize)]
|
||||
@@ -312,7 +299,7 @@ enum RawAuthor {
|
||||
}
|
||||
|
||||
impl RawAuthor {
|
||||
/// Flatten to the ordered author list (Lean `RawAuthor.normalize`): a single
|
||||
/// Flatten to the ordered author list: a single
|
||||
/// name becomes a one-element list; a list passes through verbatim.
|
||||
fn into_vec(self) -> Vec<String> {
|
||||
match self {
|
||||
|
||||
+1
-1
@@ -30,7 +30,7 @@
|
||||
"axios": "1.18.1"
|
||||
}
|
||||
},
|
||||
"description": "Curriculum Project Hub — org-scoped Feishu collaboration and confined Agent runtime. Aligns to spec/System through ADR-0024.",
|
||||
"description": "Curriculum Project Hub — org-scoped Feishu collaboration and confined Agent runtime. Semantics pinned by docs/adr/ (ADR-0001 through ADR-0027).",
|
||||
"scripts": {
|
||||
"dev": "npm run prisma:migrate && tsx watch src/server.ts",
|
||||
"build": "tsc -p tsconfig.json && npm run admin:build",
|
||||
|
||||
+1
-1
@@ -1,6 +1,6 @@
|
||||
-- ADR-0023 rejected the legacy `PlatformRoleAssignment` / `PlatformRole`{ADMIN,TEACHER}
|
||||
-- model: the platform administration control plane is a separate identity/session/
|
||||
-- audit surface (see `Spec.System.PlatformAdministration`), intentionally not built
|
||||
-- audit surface, intentionally not built
|
||||
-- in alpha (ADR-0025, `hub/deploy/README.md`). The legacy table has no runtime
|
||||
-- reader — no guard, route, or service queries it for an authorization decision —
|
||||
-- and ADR-0023 requires it to be migrated/replaced before the platform panel ships.
|
||||
|
||||
@@ -1,6 +1,6 @@
|
||||
// Prisma schema for Curriculum Project Hub.
|
||||
//
|
||||
// Aligns to spec/System (ADR-0001..0004, 0017). Key divergences from the
|
||||
// Aligns to ADR-0001..0004, 0017. Key divergences from the
|
||||
// legacy teaching-material-host-service schema, each deliberate:
|
||||
//
|
||||
// - AgentSession is provider/model-bound. Provider runtime cursors such as
|
||||
@@ -11,8 +11,8 @@
|
||||
// - 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).
|
||||
// - AgentRunStatus adds WAITING_FOR_USER + TIMED_OUT (the run-state set is
|
||||
// open — add states without a schema migration war).
|
||||
|
||||
generator client {
|
||||
provider = "prisma-client-js"
|
||||
@@ -61,7 +61,7 @@ enum OrganizationStatus {
|
||||
}
|
||||
|
||||
/// Org-scoped membership role. Distinct from project PermissionRole and from
|
||||
/// the platform administrator surface (ADR-0023 / Spec.System.PlatformAdministration),
|
||||
/// the platform administrator surface (ADR-0023),
|
||||
/// which is a separate control plane not modeled in alpha (ADR-0025).
|
||||
model OrganizationMembership {
|
||||
id String @id @default(cuid())
|
||||
|
||||
@@ -24,10 +24,10 @@
|
||||
* denied by default and re-opened only for the workspace plus named system
|
||||
* runtimes, and `failIfUnavailable` hard-fails if the sandbox can't start. The
|
||||
* subprocess gets a minimal environment and SDK credential protection removes
|
||||
* provider secrets from Bash. This upholds `AgentFileOp.Authorized`
|
||||
* (ADR-0018 / `Spec.System.AgentSurface`) without re-implementing the
|
||||
* provider secrets from Bash. This upholds the workspace-bounded file-op
|
||||
* invariant (ADR-0018) without re-implementing the
|
||||
* `workspace.ts` `confine()` path validator as a tool wrapper — the OS sandbox
|
||||
* is the mechanism, the contract pins the invariant.
|
||||
* is the mechanism, the ADR pins the invariant.
|
||||
*/
|
||||
import { query, type HookCallback, type McpServerConfig, type SDKMessage, type SDKAssistantMessage, type SDKUserMessage, type SDKResultMessage, type SDKPartialAssistantMessage, type SDKSystemMessage } from "@anthropic-ai/claude-agent-sdk";
|
||||
import type { PrismaClient } from "@prisma/client";
|
||||
|
||||
@@ -1,6 +1,6 @@
|
||||
/**
|
||||
* ADR-0022 capacity dimensions (spec `Spec.System.Capacity.CapacityDimension`).
|
||||
* The 23 PINNED dimensions; exact numeric ceilings are `OPEN` and calibrated by
|
||||
* ADR-0022 capacity dimensions.
|
||||
* The 23 pinned dimensions; exact numeric ceilings are open and calibrated by
|
||||
* capacity testing. This module is the single source of the dimension set shared
|
||||
* by the platform-ceiling config and the org capacity-policy service.
|
||||
*/
|
||||
|
||||
@@ -1,9 +1,9 @@
|
||||
/**
|
||||
* Org capacity policy service (ADR-0022 / spec `Spec.System.Capacity`).
|
||||
* Org capacity policy service (ADR-0022).
|
||||
*
|
||||
* Stores per-Organization lower `organizationLimit` overrides per
|
||||
* `CapacityDimension`. Enforces `LayeredLimit.Valid`: a set limit must be ≤ the
|
||||
* platform ceiling for that dimension. `LayeredLimit.effective` (min of the two)
|
||||
* `CapacityDimension`. Enforces the layered-limit invariant: a set limit must be ≤ the
|
||||
* platform ceiling for that dimension. The effective limit (min of the two)
|
||||
* is the value capacity admission should use; dimensions with no org override
|
||||
* fall back to the platform ceiling.
|
||||
*/
|
||||
|
||||
@@ -1,7 +1,7 @@
|
||||
/**
|
||||
* Organization membership management for org admin (ADR-0021).
|
||||
*
|
||||
* Role rules (product pin, not yet in Lean):
|
||||
* Role rules (product pin, not yet recorded in an ADR):
|
||||
* 1. Actor must be OWNER or ADMIN (enforced at HTTP layer).
|
||||
* 2. Only OWNER can grant/revoke OWNER or modify another OWNER.
|
||||
* 3. Cannot revoke or demote the last remaining OWNER.
|
||||
|
||||
@@ -1 +0,0 @@
|
||||
/.lake
|
||||
@@ -1,55 +0,0 @@
|
||||
# spec —— Lean 语义母本
|
||||
|
||||
这是本 monorepo 的**契约**:产品各部件语义的上游参照,用 Lean 编写。它的定位与约束见仓库根 `README.md` 的"宪法"5 条——本文件只讲**怎么往这份契约里写东西**。
|
||||
|
||||
## 现状
|
||||
|
||||
刚初始化的 Lean 工程(`lake init`),目前只有占位内容(`Spec/Basic.lean`)。实质领域内容(System 平台层、Courseware 产品层)将逐个概念加入,每个都遵循下面的规范。
|
||||
|
||||
## 构建
|
||||
|
||||
```sh
|
||||
cd spec
|
||||
lake build
|
||||
```
|
||||
|
||||
工具链锁定在 `lean-toolchain`(`leanprover/lean4:v4.31.0`)。无外部依赖——Mathlib / Batteries 等留待第一个真正需要它的定理出现时再引入(依赖碰到再加)。
|
||||
|
||||
## 写作规范
|
||||
|
||||
### 双半契约:prose + type
|
||||
|
||||
每个 top-level 声明**必须**带 `/-- … -/` doc 注释,用自然语言陈述其语义意图。两半缺一不可:
|
||||
|
||||
- **prose 半**给人读——说清"这在领域里是什么、为什么"。
|
||||
- **type 半**给机器读、给 type checker 把关——保证结构无洞。
|
||||
|
||||
agent 不得用预训练先验脑补本领域(领域很新,无先验);prose 是 agent 理解语义的唯一权威来源。
|
||||
|
||||
### 标签分类法
|
||||
|
||||
在 doc 注释里用以下标签标注每条语义的状态:
|
||||
|
||||
- **`PINNED`** —— 已解决的分歧点,契约在此处权威,双方据此对齐。
|
||||
- **`OPEN`** —— 故意未规定。双方均**不得假设**其解;实现遇到时必须 surface 出来讨论,而不是擅自决定。
|
||||
- **`ADR-NNNN`** —— 链接到根 `docs/adr/` 下的对应决策记录(如 `ADR-0002`),交代该语义的决策出处。
|
||||
|
||||
### 分歧点测试(写之前先过一遍)
|
||||
|
||||
新增任何概念前,先问:**"不写明,开发者与 agent 会不会各自做出不同假设?"**
|
||||
|
||||
- 会 → 它是分歧点,入契约。
|
||||
- 不会(显然的东西 / 纯 plumbing / 普通 CRUD 字段)→ 不入。
|
||||
|
||||
详见根 README 宪法第 5 条。
|
||||
|
||||
### 不用 `sorry`
|
||||
|
||||
无法陈述清楚的东西,用 `OPEN` 在 prose 里标注,而**不是**用 `sorry` 留一个假装成立的定理。`sorry` 会让 `lake build` 仍然变绿,却在契约里埋一个谎——这与"契约自包含、无洞"直接冲突。
|
||||
|
||||
### 命名
|
||||
|
||||
- **模块 / 命名空间**:PascalCase,对应分层,如 `Spec.System.Agent.Run`、`Spec.Courseware.Validity`。
|
||||
- **类型**:PascalCase。
|
||||
- **谓词 / `Prop`**:用意图清晰的命名,如 `Legal…`、`ValidTransition`、`Can…`。
|
||||
- **文件粒度**:原则上"一个带独立不变式的概念一个文件"。
|
||||
@@ -1,5 +0,0 @@
|
||||
-- This module serves as the root of the `Spec` library.
|
||||
-- Import modules here that should be built as part of the library.
|
||||
import Spec.Prelude
|
||||
import Spec.System
|
||||
import Spec.Courseware
|
||||
@@ -1,21 +0,0 @@
|
||||
import Spec.Courseware.Model
|
||||
import Spec.Courseware.Export
|
||||
import Spec.Courseware.Check
|
||||
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 骨架(核心关系 OPEN,已 surface):题库 `QuestionBank`、
|
||||
课程编排 `Course`。
|
||||
-/
|
||||
@@ -1,9 +0,0 @@
|
||||
import Spec.Courseware.Check.Diagnostic
|
||||
import Spec.Courseware.Check.Pipeline
|
||||
|
||||
/-!
|
||||
# Courseware.Check —— checker 语义
|
||||
|
||||
诊断分类与合法 lesson(`Diagnostic`)、检查管线的阶段与序(`Pipeline`)。决策出处
|
||||
ADR-0010。
|
||||
-/
|
||||
@@ -1,107 +0,0 @@
|
||||
import Spec.Courseware.Model.Lesson
|
||||
import Spec.Courseware.Export.Render
|
||||
|
||||
/-!
|
||||
# Diagnostic —— checker 诊断:分类、严重级别、合法 lesson
|
||||
|
||||
产品里"站在 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 类。
|
||||
-/
|
||||
|
||||
namespace Spec.Courseware
|
||||
|
||||
/-- 诊断严重级别(`PINNED` 二分, 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`。 -/
|
||||
inductive DiagKind where
|
||||
/-- manifest 的 part 指向不存在的文件夹(或经 `..` 逃出根)。结构型。 -/
|
||||
| partPathMissing
|
||||
/-- part 声明了未知 kind(含 part 与 element.toml 的 kind 不一致)。结构型。 -/
|
||||
| unknownKind
|
||||
/-- kind schema 要求的某 `content` 字段缺对应 `<field>.typ`。结构/schema 型。 -/
|
||||
| missingContentFile
|
||||
/-- 实例数据不合其 kind 的 JSON Schema;亦作 manifest/element.toml 畸形的兜底。 -/
|
||||
| schemaViolation
|
||||
/-- 拼装出的 typst 源编译失败:语法错、未解析的交叉引用 `@ref`、越界或缺失的相对
|
||||
`import`/`include`(后两者即旧 `danglingReference` 的两种情形——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 处理。 -/
|
||||
| cphVersionMismatch
|
||||
|
||||
/-- 每类诊断的**严重级别**(`PINNED`, ADR-0010)。六类 `error`(阻断);**唯
|
||||
`renderIgnored` 为 `warning`**——ADR-0005 种子规则"缺渲染 ⇒ warning,不阻断导出"。
|
||||
全函数使"哪类阻断"成为可引用、可对齐的事实(实现侧 `DiagCode` 级别据此对齐)。 -/
|
||||
def DiagKind.severity : DiagKind → Severity
|
||||
| .partPathMissing => .error
|
||||
| .unknownKind => .error
|
||||
| .missingContentFile => .error
|
||||
| .schemaViolation => .error
|
||||
| .typstCompile => .error
|
||||
| .renderIgnored => .warning
|
||||
| .cphVersionMismatch => .error
|
||||
|
||||
/-- 缺渲染诊断的级别 = **warning**(`PINNED`, 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。 -/
|
||||
def renderIgnored (l : Lesson P) (c : RenderConfig P) (t : P.TargetId) : Prop :=
|
||||
∃ e ∈ l, ¬ c.covers e.kind t
|
||||
|
||||
/-!
|
||||
## 模型外设施型诊断:抽象谓词 + 实现边界(ADR-0010)
|
||||
|
||||
`typstCompile`/`schemaViolation`(的 schema-合规面)断言的是模型自身无法判定的事实——
|
||||
要跑 typst 编译器、schema 校验器。契约把它们建成**抽象谓词**,真值由实现提供的 oracle
|
||||
给出。下面用 `Oracle` 收口这些判定:它不是要在 Lean 里实现 checker,而是把"这些事实
|
||||
来自模型外"显式化、类型化。
|
||||
-/
|
||||
|
||||
/-- **实现侧判定 oracle**(`PINNED` 实现边界, ADR-0010)。每个字段是一个谓词,真值由
|
||||
实现(checker)提供。结构型诊断(part 路径、未知 kind)不入此 oracle——那些模型自身可判。 -/
|
||||
structure Oracle (l : Lesson P) (c : RenderConfig P) where
|
||||
/-- target `t` 下拼装源可编译(否 ⇒ `typstCompile`)。**含引用解析**:源能编译即蕴含
|
||||
其 `@ref`、相对 import 全部解析(ADR-0012 已把引用诊断并入 `typstCompile`)。 -/
|
||||
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` 的可枚举性。 -/
|
||||
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)
|
||||
|
||||
end Spec.Courseware
|
||||
@@ -1,54 +0,0 @@
|
||||
import Spec.Courseware.Check.Diagnostic
|
||||
|
||||
/-!
|
||||
# Pipeline —— checker 检查管线的阶段与序(ADR-0010)
|
||||
|
||||
checker 的 `check` 按**固定顺序**跑五个阶段,逐阶段收集诊断;`compile` 阶段有**门控**。
|
||||
顺序与门控是契约——它决定用户看到哪些诊断(藏在缺文件背后的语法错,在文件补齐前不
|
||||
显示,这是有意的)。每阶段的**算法**不进 Lean(深度上限:只定**阶段、序、
|
||||
门控**)。阶段对应上游模块:`load`←`cph-model`;`structural`←part 路径/未知 kind;
|
||||
`schema`←`cph-schema`;`compile`←`cph-typst`(模型外设施);`coverage`←`renderIgnored`。
|
||||
-/
|
||||
|
||||
namespace Spec.Courseware
|
||||
|
||||
/-- 检查管线的**阶段**(`PINNED` 5 阶段, ADR-0010)。
|
||||
|
||||
- `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`);**不**受门控,总跑。 -/
|
||||
inductive Phase where
|
||||
| load
|
||||
| structural
|
||||
| schema
|
||||
| compile
|
||||
| coverage
|
||||
deriving DecidableEq
|
||||
|
||||
/-- 管线阶段的**执行序**(`PINNED`, ADR-0010)。`order p` 越小越先跑。序是契约:
|
||||
`compile`(3)排在 `structural`(1)/`schema`(2)之后,正因前者门控于后者无 error。 -/
|
||||
def Phase.order : Phase → Nat
|
||||
| .load => 0
|
||||
| .structural => 1
|
||||
| .schema => 2
|
||||
| .compile => 3
|
||||
| .coverage => 4
|
||||
|
||||
/-- 某阶段是否**受"前序零 error"门控**(`PINNED`, ADR-0010)。唯 `compile` 受门控:藏在
|
||||
结构/schema 错背后的编译错,在前者修好前不显示——有意降噪。 -/
|
||||
def Phase.gated : Phase → Bool
|
||||
| .compile => true
|
||||
| _ => false
|
||||
|
||||
/-- 管线在 `load` 硬失败时**停**(`PINNED`, ADR-0010)。`load` 拿不到可解析 lesson 时,
|
||||
无 lesson 可喂下游,整条管线终止——唯一会截断后续所有阶段的情形(区别于 `compile`
|
||||
门控只跳过自己)。 -/
|
||||
def Phase.haltsPipelineOnFailure : Phase → Bool
|
||||
| .load => true
|
||||
| _ => false
|
||||
|
||||
end Spec.Courseware
|
||||
@@ -1,8 +0,0 @@
|
||||
import Spec.Courseware.Export.Artifact
|
||||
import Spec.Courseware.Export.Render
|
||||
|
||||
/-!
|
||||
# Courseware.Export —— export target = artifact + 有序 typed steps
|
||||
|
||||
产物 ADT(`Artifact`)、build 规格与渲染覆盖(`Render`)。决策出处 ADR-0009 / 0011。
|
||||
-/
|
||||
@@ -1,23 +0,0 @@
|
||||
/-!
|
||||
# Artifact —— export target 的产物(ADR-0009 / 0011)
|
||||
|
||||
ADR-0009:一个 export target 是**一次 build**,产出一个**有类型的产物**。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)。 -/
|
||||
inductive Artifact where
|
||||
/-- 单文件产物,落在 `filepath`(相对工程根)。讲义/教案 PDF 即此。 -/
|
||||
| singleFile (filepath : String)
|
||||
/-- 多文件产物:`root` 目录下匹配 `outputs` **glob** 的文件集(第三方平台 archive
|
||||
即此)。用 glob 而非显式清单:轻,又让消费方/checker 知道该产出哪些文件、可校验
|
||||
完整性。 -/
|
||||
| fileTree (root : String) (outputs : String)
|
||||
|
||||
end Spec.Courseware
|
||||
@@ -1,93 +0,0 @@
|
||||
import Spec.Courseware.Model.Primitives
|
||||
import Spec.Courseware.Export.Artifact
|
||||
|
||||
/-!
|
||||
# Render —— export target = artifact + 有序 typed steps(ADR-0009 / 0011)
|
||||
|
||||
ADR-0009:export target 是一次 build,产出一个有类型的 `Artifact`。ADR-0011 固定 build
|
||||
的**形状**:一个 target 是 `artifact` + 一串**有序 typed step**。
|
||||
|
||||
- `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 稳。
|
||||
|
||||
**渲染覆盖**:ADR-0011 废止了 per-target `RenderRule` 载荷——渲染的"how"已移进模板。
|
||||
契约只保留覆盖声明 `covers`(该 target 渲染哪些 kind),供种子诊断用。
|
||||
|
||||
**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(教具包即此)由
|
||||
执行器跑命令,而非走 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)。
|
||||
-/
|
||||
|
||||
namespace Spec.Courseware
|
||||
|
||||
variable (P : Primitives)
|
||||
|
||||
/-- 一个 build **step**(`PINNED` typed, 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 : 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)。 -/
|
||||
| assembleMarkdown (field : String)
|
||||
|
||||
/-- 一个 export target 的 build 规格(`PINNED` artifact + 有序 steps, ADR-0011)。 -/
|
||||
structure TargetSpec where
|
||||
/-- 产物(带字段, ADR-0011)。决定 build 折叠成单文件还是文件树。 -/
|
||||
artifact : Artifact
|
||||
/-- **有序** build steps。按序执行;MVP 仅一个 `typstCompile`。 -/
|
||||
steps : List Step
|
||||
/-- **覆盖声明**:`covers k` 表示此 target 渲染 kind `k`。ADR-0011 把旧
|
||||
`renders : KindId → Option RenderRule` 降级后的产物——契约只声明"渲染哪些 kind"
|
||||
(种子诊断 `renderIgnored` 用),"how"由 `steps` 的模板实现。 -/
|
||||
covers : P.KindId → Prop
|
||||
|
||||
/-- 渲染配置(`PINNED` target-中心, 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` 隐式以便点记法。 -/
|
||||
def RenderConfig.covers {P : Primitives} (c : RenderConfig P)
|
||||
(k : P.KindId) (t : P.TargetId) : Prop :=
|
||||
match c.spec t with
|
||||
| none => False
|
||||
| some s => s.covers k
|
||||
|
||||
end Spec.Courseware
|
||||
@@ -1,13 +0,0 @@
|
||||
import Spec.Courseware.Model.Primitives
|
||||
import Spec.Courseware.Model.RichContent
|
||||
import Spec.Courseware.Model.Element
|
||||
import Spec.Courseware.Model.Lesson
|
||||
import Spec.Courseware.Model.Info
|
||||
|
||||
/-!
|
||||
# Courseware.Model —— 工程文件的内容模型
|
||||
|
||||
基元(`Primitives`)、富内容锚点(`RichContent`)、原子单位(`Element`)、单节课
|
||||
(`Lesson`)、课时元信息(`Info`:canonical author 为列表 vs `RawInfo` 撰写态)。
|
||||
决策出处 ADR-0005 / 0006 / 0008。
|
||||
-/
|
||||
@@ -1,24 +0,0 @@
|
||||
import Spec.Courseware.Model.Primitives
|
||||
|
||||
/-!
|
||||
# Element —— 课程内容的原子单位
|
||||
|
||||
ADR-0005:element 实例 = 一个 kind 标签 + 符合该 kind schema 的数据。把它编码成
|
||||
依赖结构,使"数据必须匹配其 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` 不同,重实现在模型之外。 -/
|
||||
structure Element where
|
||||
/-- 该 element 的 kind。 -/
|
||||
kind : P.KindId
|
||||
/-- 符合 `kind` schema 的数据(类型随 `kind` 而变)。 -/
|
||||
data : P.ElementData kind
|
||||
|
||||
end Spec.Courseware
|
||||
@@ -1,58 +0,0 @@
|
||||
/-!
|
||||
# Info —— 课时元信息:canonical 模型 vs 撰写态(authoring surface)
|
||||
|
||||
`[info]`(标题、作者)大多是 passthrough 元数据(ADR-0008),本不入契约。但**作者的
|
||||
基数**是一个真分歧点:一节课可由多人(教研组)署名,故 canonical 模型里 author 是一个
|
||||
**有序列表**,不是单值或可选单值。
|
||||
|
||||
另一条模式: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` 折叠后不再出现。 -/
|
||||
inductive RawAuthor where
|
||||
/-- 单作者裸字符串 `author = "…"`。 -/
|
||||
| one (name : String)
|
||||
/-- 多作者数组 `author = ["…", "…"]`。 -/
|
||||
| many (names : List String)
|
||||
|
||||
/-- raw 作者归一化为**有序作者列表**(`PINNED`, 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 在此**已**是列表,不再是
|
||||
"字符串或数组"。 -/
|
||||
structure Info where
|
||||
/-- 标题(passthrough 元数据)。 -/
|
||||
title : String
|
||||
/-- 作者**有序列表**(空 = 未署名)。canonical 始终是列表。 -/
|
||||
authors : List String
|
||||
|
||||
/-- 撰写态的 `[info]`(`PINNED` 仅填写便利, ADR-0008)。`author` 用 `RawAuthor`
|
||||
(字符串或数组),`author` 缺省即未署名。此结构刻画"为便于填写而存在的 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`。 -/
|
||||
def RawInfo.toInfo (r : RawInfo) : Info :=
|
||||
{ title := r.title
|
||||
authors := (r.author.map RawAuthor.normalize).getD [] }
|
||||
|
||||
end Spec.Courseware
|
||||
@@ -1,16 +0,0 @@
|
||||
import Spec.Courseware.Model.Element
|
||||
|
||||
/-!
|
||||
# Lesson —— 单节课工程文件
|
||||
|
||||
ADR-0005:一个工程文件 = 一节课,是 element 实例的**有序序列**。课程/单元不是工程
|
||||
文件,而是 lesson 的编排(见 `Spec.Courseware.Course`,OPEN)。
|
||||
-/
|
||||
|
||||
namespace Spec.Courseware
|
||||
|
||||
/-- 一节课(`PINNED`, ADR-0005)。用 `List` 因为 **element 次序承载教学语义**(先讲
|
||||
定义再举例 ≠ 反过来);**不建模时长**——ADR-0005 决定 lesson 是内容编排而非时间轴。 -/
|
||||
abbrev Lesson (P : Primitives) := List (Element P)
|
||||
|
||||
end Spec.Courseware
|
||||
@@ -1,34 +0,0 @@
|
||||
/-!
|
||||
# Primitives —— Courseware 契约的基元
|
||||
|
||||
课程工程文件模型(ADR-0005)依赖一组基元:element kind 怎么标识、某 kind 的数据
|
||||
schema 是什么、export target 怎么标识。收口成载体 `Primitives`,让模型在其上参数化
|
||||
——契约谈得了 element / lesson / 渲染**之间的关系**,而把每个基元的**内部表示**留给
|
||||
实现。注意:某基元语义已 PINNED(如 schema 形态由 ADR-0006 固定)与其表示进 Lean
|
||||
是两回事——JSON Schema / typst 的内部结构属实现细节,不入 Lean,故基元在此仍以抽象
|
||||
类型承载。富内容的母本见 `Courseware.RichContent`。
|
||||
-/
|
||||
|
||||
namespace Spec.Courseware
|
||||
|
||||
/-- Courseware 契约基元载体(关系 `PINNED`, ADR-0005;各基元表示留给实现, ADR-0006)。 -/
|
||||
structure Primitives where
|
||||
/-- element kind 标识(`PINNED` **开放宇宙**, ADR-0005;表示 `OPEN`)。用抽象
|
||||
类型而非 `inductive`:ADR-0005 决定 kind 是开放可扩展宇宙(stdlib + 第三方),
|
||||
封闭枚举会违背它——此处开放是**已决策的**(区别于 `RunState` 的"尚未封闭")。 -/
|
||||
KindId : Type
|
||||
/-- 某 kind 的合法数据类型(`PINNED` 依赖关系, ADR-0005;schema 形态 `PINNED`
|
||||
ADR-0006,表示仍抽象)。以 kind 为索引:`ElementData k` 即"符合 `k` schema 的
|
||||
数据"。schema 形态(声明式 JSON Schema + `content` 叶子 = typst 源)由 ADR-0006
|
||||
固定,但属 JSON/typst 内部结构、实现细节,不进 Lean;契约只锚定"数据符合
|
||||
kind schema"这条关系,故此处仍是抽象类型。 -/
|
||||
ElementData : KindId → Type
|
||||
/-- export target 标识(`PINNED` 角色, ADR-0005;表示 `OPEN`)。一个 target 是一次
|
||||
build,产出对 lesson 的一种投影(讲义/教案/PPT/平台 archive…),见 `Render`。 -/
|
||||
TargetId : Type
|
||||
|
||||
-- 注:原 `RenderRule : Type` 已随 ADR-0011 移除。渲染的"how"不再是契约层 per-target
|
||||
-- 载荷,而由 `Render.TargetSpec.steps` 里 `typstCompile` step 引用的**模板文件**承载;
|
||||
-- 契约只保留覆盖声明 `TargetSpec.covers`(该 target 渲染哪些 kind),供种子诊断用。
|
||||
|
||||
end Spec.Courseware
|
||||
@@ -1,44 +0,0 @@
|
||||
/-!
|
||||
# RichContent —— 富内容(ADR-0006 的母本)
|
||||
|
||||
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"这一步。
|
||||
|
||||
关键约束(均 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`)。
|
||||
|
||||
只立锚点 + 最小抽象签名:typst 的 `Content`/`Module` 内部结构、JSON Schema 形状、format 的
|
||||
具体判别属实现细节,不进 Lean,只承诺"富内容由一个虚拟路径定位"+"叶子带 format"这两条关系。
|
||||
-/
|
||||
|
||||
namespace Spec.Courseware
|
||||
|
||||
/-- 富内容在工程文件路径结构中的**虚拟路径**(`OPEN` 表示, ADR-0006)。把一段富内容
|
||||
定位为 World 里的一等文件(span 可解析、相对 import 可锚定)。落盘后即真实相对路径
|
||||
(ADR-0007),不在本层承诺,故 opaque。 -/
|
||||
opaque VPath : Type
|
||||
|
||||
/-- 富内容的 **format**(`PINNED`, ADR-0015)。`content` 叶子带 format:typst 叶子被 typst 求值;
|
||||
markdown 叶子原样保留(markdown+KaTeX 源,不经求值)。 -/
|
||||
inductive ContentFormat where
|
||||
/-- typst 源:求值为 typst `Content`(讲义/教案面)。 -/
|
||||
| typst
|
||||
/-- markdown + KaTeX 源:原样保留,不经 typst 求值(slides 大纲面 / 逐字稿口播面;ADR-0015)。 -/
|
||||
| markdown
|
||||
|
||||
/-- 对一段富内容的**引用**:它坐落在某个虚拟路径上(`PINNED` 关系, ADR-0006),并带一个
|
||||
**format**(`PINNED`, ADR-0015)。不建模源文本、不建模求值出的 `Content`(那是实现侧的事);
|
||||
"富内容经由一个 `VPath` 定位 + 带 format",作为 `Primitives.ElementData` 里 `content` 叶子的语义锚点。 -/
|
||||
structure RichContentRef where
|
||||
/-- 该富内容所在的虚拟路径(ADR-0006;落盘后为真实相对路径, ADR-0007)。 -/
|
||||
vpath : VPath
|
||||
/-- 该富内容的 format(ADR-0015)。 -/
|
||||
format : ContentFormat
|
||||
|
||||
end Spec.Courseware
|
||||
@@ -1,9 +0,0 @@
|
||||
import Spec.Courseware.Open.QuestionBank
|
||||
import Spec.Courseware.Open.Course
|
||||
|
||||
/-!
|
||||
# Courseware.Open —— OPEN 骨架(核心关系)
|
||||
|
||||
题库与 element 的关系(`QuestionBank`)、课程编排规则(`Course`)。两者均为已 surface
|
||||
但未决策的 OPEN 分歧点,待专门 ADR 落定。
|
||||
-/
|
||||
@@ -1,10 +0,0 @@
|
||||
/-!
|
||||
# Course —— 课程编排(骨架,规则 OPEN)
|
||||
|
||||
ADR-0005:工程文件的粒度是**单节课**;course / 单元**不是**工程文件,而是 lesson 的
|
||||
**编排**。但"编排"的具体规则未决策:有序列表还是带层级(单元 → 课)的树?lesson 被
|
||||
引用还是被包含?跨 lesson 有无约束(目标覆盖、前后置)?这些都是 `OPEN`。
|
||||
|
||||
此处不替它选解——不建 `Course := List Lesson`(那会偷偷承诺
|
||||
"扁平有序、无层级")。只在此 surface:课程编排待专门 ADR。本文件当前不引入任何承诺性声明。
|
||||
-/
|
||||
@@ -1,10 +0,0 @@
|
||||
/-!
|
||||
# QuestionBank —— 题库(骨架,核心关系 OPEN)
|
||||
|
||||
题库是与工程文件并列的资产(类比 DAW 的 sample library):有自身结构的实体,又是最
|
||||
典型的可复用单元,lesson 会引用它。但**题库与 element 的关系尚未决策**,且用户明确
|
||||
指出"纯引用可能不够"——element 内联题目数据 / lesson 持指向题库条目的引用 / 两者并存?
|
||||
|
||||
这是一个 `OPEN` 分歧点。此处不替它选解——不建 `QuestionRef` 也不建
|
||||
内联结构,只在此 surface。待专门 ADR 落定后再填。本文件当前不引入任何承诺性声明。
|
||||
-/
|
||||
@@ -1,67 +0,0 @@
|
||||
/-!
|
||||
# Prelude —— System 层共享标识符
|
||||
|
||||
平台层引用一组标识符(项目、run、session、principal、chat、platform identity/audit)。
|
||||
其内部表示从未被决策(UUID / 复合键、principal 子类型学),也非分歧点,故收口成 opaque
|
||||
载体 `Identifiers`,System 各模块在其上参数化——契约谈得了"锁 owner 是哪个 run"这类
|
||||
关系,却不对标识符表示作承诺。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
/-- System 层标识符载体(关系结构 `PINNED`;各字段表示 `OPEN`)。 -/
|
||||
structure Identifiers where
|
||||
/-- 课程项目标识(`OPEN` 表示;聚合根,likec4 `Project`)。 -/
|
||||
ProjectId : Type
|
||||
/-- SaaS 租户/组织标识(`OPEN` 表示;ADR-0020 tenant root)。 -/
|
||||
OrganizationId : Type
|
||||
/-- 租户层用户标识(`OPEN` 表示;独立实体,非飞书身份派生;见 `Hierarchy.User`)。 -/
|
||||
UserId : Type
|
||||
/-- 飞书用户 open_id(`OPEN` 表示;单应用作用域内唯一)。 -/
|
||||
FeishuOpenId : Type
|
||||
/-- 飞书 user_id(`OPEN` 表示;租户内唯一,换 app 不变)。 -/
|
||||
FeishuUserId : Type
|
||||
/-- 飞书企业应用 app_id(`OPEN` 表示)。 -/
|
||||
FeishuAppId : Type
|
||||
/-- 飞书 app_secret 信封引用(`OPEN` 表示;ADR-0024)。 -/
|
||||
FeishuAppSecretRef : Type
|
||||
/-- Hub teacher team 标识(`OPEN` 表示;ADR-0020 org-scoped team)。 -/
|
||||
TeamId : Type
|
||||
/-- Project explorer folder 标识(`OPEN` 表示;ADR-0021 透明组织节点,非权限资源)。 -/
|
||||
FolderId : Type
|
||||
/-- 一次 agent 任务的标识(`OPEN` 表示;锁的 owner、审计主体,`AgentRun`。provider 无关,
|
||||
ADR-0017;`@bot` 仅为触发品牌,不承诺 provider)。 -/
|
||||
RunId : Type
|
||||
/-- 长生命周期 agent 会话标识(`OPEN` 表示;**provider/model 绑定, ADR-0017**——一次
|
||||
session 不跨 provider/model;切 model 即新 session,跨 session 连续性由 ADR-0003 项目
|
||||
记忆/锚点重建,不由 session 自带。同 provider/model 内可跨多 run 复用, ADR-0002)。 -/
|
||||
SessionId : Type
|
||||
/-- Organization-scoped Agent role 标识(`OPEN` 表示, ADR-0017);role 是动态运行配置,
|
||||
不是 slash command 枚举。 -/
|
||||
AgentRoleId : Type
|
||||
/-- 权限主体标识(`OPEN` 表示及其子类型学;ADR-0004 的 user/chat/department/…
|
||||
子类型学未定且非分歧点,故只留 opaque 键)。 -/
|
||||
Principal : Type
|
||||
/-- 飞书项目群 chat 标识(`OPEN` 表示;ADR-0001 协作空间、ADR-0003 锚点引用、
|
||||
ADR-0004 `feishu_chat` principal 三处共用同一实体。独立成载体而非 `Principal` 子
|
||||
类型——principal 子类型学 OPEN,这里不预设"chat 是 principal 的哪种子型")。 -/
|
||||
ChatId : Type
|
||||
/-- 平台管理员身份标识(`OPEN` 表示;ADR-0023,不复用客户 `User` 标识)。 -/
|
||||
PlatformIdentityId : Type
|
||||
/-- 平台自有飞书应用标识(`OPEN` 表示;ADR-0023,与各 org 客户应用分离)。 -/
|
||||
PlatformFeishuApplicationId : Type
|
||||
/-- 平台应用所验证的外部飞书用户标识(`OPEN` 表示;ADR-0023,其具体 open_id/user_id
|
||||
表示与迁移方式不在本层固定)。 -/
|
||||
PlatformExternalUserId : Type
|
||||
/-- 可撤销 Platform Session 标识(`OPEN` 表示;ADR-0023)。 -/
|
||||
PlatformSessionId : Type
|
||||
/-- Platform Administrator invitation 标识(`OPEN` 表示;ADR-0023)。 -/
|
||||
PlatformInvitationId : Type
|
||||
/-- 一次平台控制面 mutation 标识(`OPEN` 表示;ADR-0023)。 -/
|
||||
PlatformMutationId : Type
|
||||
/-- 独立 Platform Audit Entry 标识(`OPEN` 表示;ADR-0023)。 -/
|
||||
PlatformAuditEntryId : Type
|
||||
/-- 平台离线恢复所声明的 incident 标识(`OPEN` 表示;ADR-0023)。 -/
|
||||
PlatformIncidentId : Type
|
||||
|
||||
end Spec.System
|
||||
@@ -1,57 +0,0 @@
|
||||
import Spec.System.Hierarchy
|
||||
import Spec.System.ProjectGroup
|
||||
import Spec.System.Organization
|
||||
import Spec.System.User
|
||||
import Spec.System.Connections
|
||||
import Spec.System.ProjectWorkspace
|
||||
import Spec.System.Capacity
|
||||
import Spec.System.PlatformAdministration
|
||||
import Spec.System.Agent.Run
|
||||
import Spec.System.Agent.AgentRole
|
||||
import Spec.System.Agent.Memory
|
||||
import Spec.System.Agent.AgentSurface
|
||||
import Spec.System.Agent.Usage
|
||||
import Spec.System.Agent.Capability
|
||||
import Spec.System.Lock
|
||||
import Spec.System.Permission
|
||||
import Spec.System.PermissionGrant
|
||||
import Spec.System.Audit
|
||||
/-!
|
||||
# System —— Hub 平台层契约
|
||||
|
||||
协作与执行的平台:项目、飞书群、AgentRun、锁、权限、审计、按需上下文。
|
||||
likec4 已画出结构;这里补语义:
|
||||
|
||||
- `Hierarchy` —— 三层主体:平台 → 组织 → 用户。
|
||||
- `User` —— 用户创建路径(管理员直接创建;飞书注册 `OPEN`)。
|
||||
- `Connections` —— 外部连接:提供商枚举(当前仅飞书) + 绑定/信息类型。
|
||||
- `ProjectGroup` —— project↔飞书群 1:1 长生命周期绑定(ADR-0001);群是协作空间,不持锁。
|
||||
- `Organization` —— SaaS 租户(ADR-0020);project/team 单归属,TEAM grant 不跨 org;
|
||||
connection secret 信封与 fail-closed resolver(ADR-0024);
|
||||
owner/admin/member(`OrganizationRole`)及其管理规则(最后所有者保护)。
|
||||
- `ProjectWorkspace` —— org 后台 project explorer:folder 是透明组织节点,project 仍是权限边界
|
||||
(ADR-0021)。
|
||||
- `Capacity` —— platform ceiling 与 org policy 的分层限制、持久 admission request 状态和
|
||||
平台紧急工作负载制动(ADR-0022)。
|
||||
- `PlatformAdministration` —— 独立平台身份/会话、单一管理员角色、绑定邀请、最后管理员
|
||||
保护、fail-closed 平台审计与离线 emergency grant(ADR-0023)。
|
||||
- `AgentRole` —— org-scoped agent 角色配置 + 技能(ADR-0017/0018)。
|
||||
- `Run` —— AgentRun 状态与终止判定(状态集合完整性 OPEN)。
|
||||
- `Lock` —— 锁 owner=run(ADR-0002),及"持锁者必为非终止 run"的核心不变式。
|
||||
- `Memory` —— 按需上下文:锚点类别(ADR-0003)+ MCP 工具按 run/project 上下文授权。
|
||||
- `AgentSurface` —— agent 执行面被 run 的工作区所界定(ADR-0018);与 Lock 正交——
|
||||
Lock 限定并发,Surface 限定波及面。机制 OPEN。
|
||||
- `Usage` —— Run 内 append-only 用量计量事实账本(ADR-0026);主模型 completion、
|
||||
外部能力调用、代理网关旁路共用同一账本。fact 不持锁、不跨 run;`costUsd = none`
|
||||
表示未知而非零(ADR-0022)。Run 上的 cost/token 标量是其 rollup cache。
|
||||
- `Capability` —— 外部能力(PDF→MD、音视频→文本等)注册与调用(ADR-0027);
|
||||
org-scoped 凭证连接复用 ADR-0024 信封但独立于 model-provider;调用是 Run 内副作用,
|
||||
产物落 workspace,消耗记 UsageFact。capability credential 不进 Agent 进程。
|
||||
- `Permission` —— read⊂edit⊂manage 角色体系、能力推导、单调性;force-release 在格外。
|
||||
- `PermissionGrant` —— grant(resource×principal×role)与 settings(六 policy 旋钮)
|
||||
(ADR-0004);组合规则 OPEN。
|
||||
- `Audit` —— customer Project/Run 审计从简(内容 OPEN);Platform Audit 由
|
||||
`PlatformAdministration` 独立承载。
|
||||
|
||||
标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004, 0018, 0020..0027。
|
||||
-/
|
||||
@@ -1,60 +0,0 @@
|
||||
import Spec.Prelude
|
||||
|
||||
/-!
|
||||
# AgentRole —— Agent 角色与技能配置 (ADR-0017, ADR-0018)
|
||||
|
||||
AgentRole 是 org-scoped 运行时配置:system prompt、tool allowlist、default model
|
||||
和 skill 绑定。通过 CLI 管理,不需重启进程生效。
|
||||
|
||||
Role 的执行面(model/prompt/tools/skill 内容)变更时,该 role 的 active sessions
|
||||
归档——下次 run 不能在旧指令下创建的 provider context 上恢复。
|
||||
仅 label/排序变更不影响会话连续性(ADR-0017)。
|
||||
|
||||
Run 时只读加载 role 选中的 skill 不可变版本到 run-scoped 目录,
|
||||
run 结束后删除(ADR-0018)。Skill 管理是 org-scoped;存储机制 `OPEN`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
variable (I : Identifiers)
|
||||
|
||||
/-- Agent 角色(`PINNED`, org-scoped, ADR-0017)。 -/
|
||||
structure AgentRole where
|
||||
/-- 所属组织(`PINNED`)。 -/
|
||||
organization : I.OrganizationId
|
||||
/-- 斜杠命令名(`OPEN` 表示;如 /draft)。 -/
|
||||
roleId : String
|
||||
/-- system prompt(`PINNED`)。 -/
|
||||
systemPrompt : String
|
||||
/-- tool allowlist(`PINNED`;tool 标识集合 `OPEN`)。 -/
|
||||
tools : List String
|
||||
/-- 默认 model(`PINNED`;model ID 表示 `OPEN`)。 -/
|
||||
defaultModel : String
|
||||
|
||||
/-- Agent 技能(`PINNED`, org-scoped, ADR-0017/0018)。 -/
|
||||
structure AgentSkill where
|
||||
/-- 所属组织(`PINNED`)。 -/
|
||||
organization : I.OrganizationId
|
||||
/-- 名称(`PINNED`)。 -/
|
||||
name : String
|
||||
/-- 版本(`PINNED`)。 -/
|
||||
version : String
|
||||
/-- 内容摘要(`PINNED`;SHA-256 content-addressed)。 -/
|
||||
contentDigest : String
|
||||
/-- 描述(`OPEN`)。 -/
|
||||
description : String
|
||||
|
||||
/-- Role-Skill 绑定(`PINNED`, ADR-0017)。一个 role 可绑定零或多个 skill。 -/
|
||||
structure AgentRoleSkillBinding where
|
||||
/-- 所属组织(`PINNED`)。 -/
|
||||
organization : I.OrganizationId
|
||||
/-- 绑定的 role(`PINNED`)。 -/
|
||||
roleId : String
|
||||
/-- skill 名称(`PINNED`)。 -/
|
||||
skillName : String
|
||||
/-- skill 版本(`PINNED`)。 -/
|
||||
skillVersion : String
|
||||
/-- 排序(`PINNED`)。 -/
|
||||
sortOrder : Nat
|
||||
|
||||
end Spec.System
|
||||
@@ -1,40 +0,0 @@
|
||||
import Spec.Prelude
|
||||
import Spec.System.Agent.Run
|
||||
|
||||
/-!
|
||||
# AgentSurface —— Agent 执行面边界(ADR-0018)
|
||||
|
||||
Agent 在一次 run 内发起的文件操作,其路径必须落在该 run 所属 project 的工作区目录内
|
||||
(ADR-0007)。逃逸即越权,拒绝。
|
||||
|
||||
与 `Lock`(ADR-0002)正交:Lock 限定并发(谁在改),Surface 限定波及面(能改到哪)。
|
||||
二者都按 run × project 作用域。
|
||||
|
||||
shell 面的边界(命令的文件效果同样不得逃逸工作区)是同一不变式的推论。机制
|
||||
——路径校验、OS 级沙箱、SDK 权限钩子,或其组合——`OPEN`(ADR-0018)。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
variable (I : Identifiers) (Path : Type)
|
||||
|
||||
/-- Agent 在一次 run 内发起的文件操作(`PINNED` 关系, ADR-0018)。由某 run 发起、
|
||||
指向某路径;是否越权由下方 `Authorized` 约束。 -/
|
||||
structure AgentFileOp where
|
||||
/-- 发起操作的 run(授权上下文主体, ADR-0018;与 `Lock` 同作用域 run × project)。 -/
|
||||
run : I.RunId
|
||||
/-- 操作目标路径(`PINNED`, ADR-0018)。 -/
|
||||
path : Path
|
||||
|
||||
|
||||
/-- 工作区边界良构:run 的文件操作路径必须落在该 run 所属 project 的工作区目录内
|
||||
(`PINNED` 安全不变式, ADR-0018)。`runWorkspace` 与 `pathWithin` 由平台提供
|
||||
(表示 `OPEN`);本谓词约束"操作路径必须以 run 的工作区为根",杜绝 agent 越权读写
|
||||
宿主任意文件。 -/
|
||||
def AgentFileOp.Authorized
|
||||
(op : AgentFileOp I Path)
|
||||
(runWorkspace : I.RunId → Option Path)
|
||||
(pathWithin : Path → Path → Prop) : Prop :=
|
||||
∃ w, runWorkspace op.run = some w ∧ pathWithin op.path w
|
||||
|
||||
end Spec.System
|
||||
@@ -1,104 +0,0 @@
|
||||
import Spec.Prelude
|
||||
import Spec.System.Agent.Run
|
||||
import Spec.System.Agent.Usage
|
||||
|
||||
/-!
|
||||
# Capability —— 外部能力注册与调用(ADR-0027)
|
||||
|
||||
`AgentRun` 内可能调用**外部能力**:PDF→MD bundle、音视频→文本、OCR 等。这些能力
|
||||
不是主 agent loop 的模型 completion,不持项目锁,不占 session 语义(ADR-0026 已拒绝
|
||||
nested Run)。它们是 Run 内的副作用:读 workspace 输入、调外部服务、产物落 workspace、
|
||||
写一条 `UsageFact`。
|
||||
|
||||
本模块 pin 三件事:
|
||||
|
||||
1. **ExternalCapability** —— 平台注册的、org 启用的文档/媒体转换服务,由稳定
|
||||
`capabilityId` 标识。
|
||||
2. **CapabilityConnection** —— org-scoped 凭证连接,复用 ADR-0024 信封机制但独立于
|
||||
model-provider connection。只有 `active` connection 可被 resolver 使用。
|
||||
3. **CapabilityInvocation 良构** —— 调用的输入/输出必须落在 run 的 workspace 内
|
||||
(ADR-0018 `AgentSurface`),且调用产生的消耗必须以 `UsageFact` 记录。
|
||||
|
||||
凭证不经 Agent 子进程:Agent 只通过 capability adapter 间接调用,adapter 在 Hub 侧
|
||||
解析 org-scoped 凭证并调用外部服务(ADR-0024 resolver boundary)。这与 model-provider
|
||||
的 loopback proxy 是不同的机制——capability 调用不走 agent 的网络面,走 Hub 直连。
|
||||
|
||||
不变式(`PINNED`, ADR-0027):
|
||||
|
||||
- **凭证隔离** —— capability credential 不进 Agent 进程环境;adapter 在 Hub 侧解析。
|
||||
- **workspace 边界** —— 输入路径与输出目录都必须落在 run 的 workspace 内(ADR-0018)。
|
||||
- **必记 fact** —— 一次成功调用必须产生 ≥1 条 `UsageFact`(`kind = externalCapability`),
|
||||
即使 `costUsd = none`(unknown ≠ 零,ADR-0022/0026)。
|
||||
|
||||
`CapabilityInvocation` 作为一等持久记录(status/retries/partial output)在 pilot 不做;
|
||||
`UsageFact` 的 `capabilityId + correlationId` 是唯一可追溯痕迹(ADR-0027 Deferred)。
|
||||
-/
|
||||
|
||||
namespace Spec.System.Agent
|
||||
|
||||
variable (I : Identifiers) (Path : Type)
|
||||
|
||||
/-- 外部能力的输入种类(`PINNED`, ADR-0027)。集合 `OPEN`——新增 kind 须 surface。 -/
|
||||
inductive CapabilityInputKind where
|
||||
/-- PDF 文档(`PINNED`)。 -/
|
||||
| pdf
|
||||
/-- 图片(`PINNED`)。 -/
|
||||
| image
|
||||
/-- 音频(`PINNED`)。 -/
|
||||
| audio
|
||||
/-- 视频(`PINNED`)。 -/
|
||||
| video
|
||||
|
||||
/-- 外部能力(`PINNED`, ADR-0027)。平台注册的文档/媒体转换服务,由 org 启用。
|
||||
|
||||
一个 capability 由稳定 `capabilityId` 标识(如 `pdf_to_md_bundle`),声明接受的输入
|
||||
种类与计量单位。org 通过 `CapabilityConnection` 启用它;adapter 是平台侧实现。 -/
|
||||
structure ExternalCapability where
|
||||
/-- 稳定能力标识(`PINNED`;如 `pdf_to_md_bundle`、`audio_video_to_text`)。 -/
|
||||
capabilityId : String
|
||||
/-- 接受的输入种类(`PINNED`, ADR-0027)。 -/
|
||||
inputKind : CapabilityInputKind
|
||||
/-- 计量单位(`OPEN`;如 `"pages"`、`"audio_seconds"`)。与 UsageFact.unit 对齐。 -/
|
||||
meteringUnit : String
|
||||
|
||||
/-- capability connection 的运行态(`PINNED`, ADR-0024/0027):与 model-provider /
|
||||
Feishu connection 同构,只有 `active` 可被 resolver 使用。 -/
|
||||
inductive CapabilityConnectionStatus where
|
||||
| draft
|
||||
| active
|
||||
| disabled
|
||||
|
||||
/-- Organization 的外部能力凭证连接(`PINNED`, ADR-0027)。复用 ADR-0024 信封机制
|
||||
但独立于 model-provider connection:capability 服务(如 MinerU、Whisper)有自己的 auth
|
||||
形状与 readiness probe,不走 OpenRouter `/v1/models`。唯一性键为
|
||||
`(organization, capabilityId)`。 -/
|
||||
structure OrganizationCapabilityConnection where
|
||||
/-- connection 所属 organization(`PINNED`, ADR-0027)。 -/
|
||||
organization : I.OrganizationId
|
||||
/-- 该 connection 启用的 capability(`PINNED`, ADR-0027)。 -/
|
||||
capability : ExternalCapability
|
||||
/-- 运行态(`PINNED`, ADR-0024/0027)。 -/
|
||||
status : CapabilityConnectionStatus
|
||||
|
||||
/-- 一次 capability 调用的良构约束(`PINNED`, ADR-0027)。输入路径与输出目录都必须落在
|
||||
发起 run 的 workspace 内(ADR-0018 `AgentSurface`);`runWorkspace` 与 `pathWithin`
|
||||
由平台提供(表示 `OPEN`)。逃逸即越权,拒绝。 -/
|
||||
structure CapabilityInvocation where
|
||||
/-- 发起调用的 run(`PINNED`;调用是 Run 内副作用,不跨 run,ADR-0026/0027)。 -/
|
||||
run : I.RunId
|
||||
/-- 被调用的 capability(`PINNED`)。 -/
|
||||
capability : ExternalCapability
|
||||
/-- 输入路径(workspace 内,`PINNED`, ADR-0018)。 -/
|
||||
inputPath : Path
|
||||
/-- 输出目录(workspace 内,`PINNED`, ADR-0018)。 -/
|
||||
outputDir : Path
|
||||
|
||||
/-- capability 调用良构:输入与输出路径都落在 run 的 workspace 内(`PINNED`,
|
||||
ADR-0018/0027)。这是 `AgentFileOp.Authorized` 在 capability 调用上的对应物。 -/
|
||||
def CapabilityInvocation.Authorized
|
||||
(inv : CapabilityInvocation I Path)
|
||||
(runWorkspace : I.RunId → Option Path)
|
||||
(pathWithin : Path → Path → Prop) : Prop :=
|
||||
∃ w, runWorkspace inv.run = some w ∧ pathWithin inv.inputPath w ∧ pathWithin inv.outputDir w
|
||||
|
||||
end Spec.System.Agent
|
||||
@@ -1,48 +0,0 @@
|
||||
import Spec.Prelude
|
||||
|
||||
/-!
|
||||
# Memory —— 按需上下文:锚点与项目记忆(ADR-0003)
|
||||
|
||||
ADR-0003:Hub 只存锚点与项目记忆,不存全量飞书消息历史;Claude 需要更多上下文时经
|
||||
飞书 API 按需读取。这里刻画所存锚点的类别(ADR 列定,枚举完整性 OPEN),并约束
|
||||
一条安全不变式:MCP 工具按 run/project 上下文授权,Claude 不得传任意 chat id
|
||||
(ADR-0003 Consequences 末条)。
|
||||
|
||||
"chat id 与 project 绑定"这一锚点类别由 `ProjectGroup.GroupBinding`(ADR-0001)权威承载,
|
||||
这里只覆盖其余飞书侧指针(触发消息、状态卡片、回复、线程)。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
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)。"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,30 +0,0 @@
|
||||
/-!
|
||||
# Run —— AgentRun 状态机
|
||||
|
||||
一次 `@bot` 创建一个 `AgentRun`(ADR-0001),它在终止时释放项目锁(ADR-0002)。
|
||||
转移关系在任何 ADR 里都未定,这里只刻画状态与终止判定(后者是 Lock 排他不变式的
|
||||
依赖),不定义转移边。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
/-- AgentRun 运行状态(状态名 `PINNED`, ADR-0001..0003, ADR-0022;完整性 `OPEN`
|
||||
——ADR 从未声明"状态就是这些";实现若需新状态(如 pending)须 surface)。终止态
|
||||
见 `RunState.Terminal`。 -/
|
||||
inductive RunState where
|
||||
| active
|
||||
| waitingForUser
|
||||
| completed
|
||||
| failed
|
||||
| timedOut
|
||||
| limitExceeded
|
||||
| canceled
|
||||
|
||||
/-- run 处于**终止态**(`PINNED`, ADR-0002, ADR-0022:锁在 completes/fails/
|
||||
timesOut/limitExceeded/canceled 时释放)。`active`/`waitingForUser` 非终止——后者仍
|
||||
占用项目(锁未释放)。 -/
|
||||
def RunState.Terminal : RunState → Prop
|
||||
| .completed | .failed | .timedOut | .limitExceeded | .canceled => True
|
||||
| .active | .waitingForUser => False
|
||||
|
||||
end Spec.System
|
||||
@@ -1,92 +0,0 @@
|
||||
import Spec.Prelude
|
||||
|
||||
/-!
|
||||
# Usage —— Run 内用量计量事实账本(ADR-0026)
|
||||
|
||||
一次 `AgentRun` 内可能产生**多条**可计费消耗:主模型 completion、外部能力调用
|
||||
(PDF→MD bundle、音视频转写等)、或代理网关侧旁路调用。这些消耗**不**是子 Run——
|
||||
它们不持项目锁、不占 session 语义、不复用 `AgentRun` 状态机。它们是 Run 内的
|
||||
append-only **计量事实**(`UsageFact`)。
|
||||
|
||||
`AgentRun` 上的 cost/token 标量是 facts 的派生 rollup cache,不是真相来源;真相在
|
||||
`UsageFact` 行。这一层抽象让"主模型"与"外部能力"两类消耗共享同一账本,而非给后者
|
||||
各开一种特化字段或 nested Run。
|
||||
|
||||
核心不变式(`PINNED`, ADR-0022 + ADR-0026):
|
||||
|
||||
- **append-only** —— fact 一旦写入只读不更不删;`costUsd` 修正走新 fact,不改旧行。
|
||||
- **`costUsd = none` 表示"未知",不是"零成本"** —— ADR-0022:missing provider cost
|
||||
remains unknown rather than zero。聚合时不得把 none 当 0 求和。
|
||||
- **fact 不持锁、不跨 run** —— 它是 Run 内的副作用账本,不是又一次 `@bot` 生命周期。
|
||||
外部能力调用亦同:它的语义边界是 `capabilityId` + `correlationId`,不是 `RunId`。
|
||||
- **价目回算是派生** —— `costSource = pricebookDerived` 时,`costUsd` 由
|
||||
`occurredAt × (provider, model)` 查价目表派生;provider 实报(`providerReported`)
|
||||
优先于派生。无价目可查时 `costSource = unknown`,`costUsd = none`。
|
||||
|
||||
外部能力(capability)注册表、价目表(pricebook)、商业结算均 `OPEN`,pilot 不做
|
||||
(ADR-0021 仍 defer commercial billing)。本模块只 pin **账本结构与不变式**。
|
||||
-/
|
||||
|
||||
namespace Spec.System.Agent
|
||||
|
||||
variable (I : Identifiers) (Time Cost Quantity : Type)
|
||||
|
||||
/-- 计量事实类型(`PINNED`, ADR-0026)。集合完整性 `OPEN`——新增 kind 须 surface,
|
||||
不得静默把外部消耗塞进既有 kind。 -/
|
||||
inductive UsageFactKind where
|
||||
/-- 主 agent loop 的模型 completion(`PINNED`)。 -/
|
||||
| modelCompletion
|
||||
/-- 外部能力调用(`PINNED`;如 pdf_to_md_bundle、audio_video_to_text)。 -/
|
||||
| externalCapability
|
||||
/-- 代理网关侧旁路调用(`PINNED`;非主 loop 的模型调用,如嵌入工具内的子请求)。 -/
|
||||
| toolProxy
|
||||
|
||||
/-- 成本来源(`PINNED`, ADR-0026)。优先级:provider 实报 > 价目派生 > unknown。 -/
|
||||
inductive CostSource where
|
||||
/-- provider/gateway 实报(`PINNED`)。 -/
|
||||
| providerReported
|
||||
/-- 用 `occurredAt × (provider, model)` 价目表派生(`PINNED`)。 -/
|
||||
| pricebookDerived
|
||||
/-- 缺失,而非零(`PINNED`;ADR-0022 missing cost ≠ zero)。 -/
|
||||
| unknown
|
||||
|
||||
/-- 一次可计费消耗的计量事实(`PINNED`, ADR-0026)。append-only;一次 run ≥0 条。
|
||||
|
||||
字段分两组:**归属与时间**(run/occurredAt/kind)用于聚合与价目回算;
|
||||
**计量与成本**(tokens/quantity/unit/costUsd/costSource)用于账目本身。
|
||||
非 token 计量(页/秒/次)走 `quantity + unit`,与 token 并存而非取代。 -/
|
||||
structure UsageFact where
|
||||
/-- 所属 run(`PINNED`;fact 不跨 run,fact 不持锁,ADR-0026)。 -/
|
||||
run : I.RunId
|
||||
/-- 消耗发生时刻(`PINNED`);价目回算依赖此字段而非 run.finishedAt,
|
||||
因为外部能力可能早于 run 结束。 -/
|
||||
occurredAt : Time
|
||||
/-- 事实类型(`PINNED`, ADR-0026)。 -/
|
||||
kind : UsageFactKind
|
||||
/-- provider 标识(`PINNED`;如 openrouter、mineru、openai_whisper)。 -/
|
||||
provider : String
|
||||
/-- 模型标识(`OPEN`;非模型计费可为 none)。 -/
|
||||
model : Option String
|
||||
/-- 输入 tokens(`OPEN`;非 token 计量可为 none)。 -/
|
||||
inputTokens : Option Nat
|
||||
/-- 输出 tokens(`OPEN`)。 -/
|
||||
outputTokens : Option Nat
|
||||
/-- 非 token 计量数值(`OPEN`;如页数、音频秒数)。与 tokens 并存。 -/
|
||||
quantity : Option Quantity
|
||||
/-- 计量单位(`OPEN`;如 "pages"、"audio_seconds"、"invocations")。 -/
|
||||
unit : Option String
|
||||
/-- 成本(`PINNED`;none = 未知,非零,ADR-0022)。 -/
|
||||
costUsd : Option Cost
|
||||
/-- 成本来源(`PINNED`;costUsd ≠ none 时必填,costUsd = none 时为 `unknown`)。 -/
|
||||
costSource : CostSource
|
||||
/-- 外部能力标识(`OPEN`;kind = externalCapability 时填,如 pdf_to_md_bundle)。 -/
|
||||
capabilityId : Option String
|
||||
/-- 外部请求关联 id(`OPEN`;对账/幂等用,不参与聚合)。 -/
|
||||
correlationId : Option String
|
||||
|
||||
/-- Fact 的成本是否**已知**(`PINNED`, ADR-0026)。聚合 rollup 时,只对已知成本求和;
|
||||
未知成本的 fact 不贡献 0,而是让汇总保持未知(若所有 fact 均未知)或部分未知。 -/
|
||||
def UsageFact.HasKnownCost (fact : UsageFact I Time Cost Quantity) : Prop :=
|
||||
fact.costUsd ≠ none
|
||||
|
||||
end Spec.System.Agent
|
||||
@@ -1,20 +0,0 @@
|
||||
import Spec.Prelude
|
||||
|
||||
/-!
|
||||
# Audit —— Project/Run 审计日志
|
||||
|
||||
审计记录里装什么(事件 schema、保留策略、可查询维度)在任何 ADR 里都未决策,
|
||||
且大多是实现细节。这里只固定"审计以 run 为主体记录其生命周期事件"这一条已决策
|
||||
关系,其余 `OPEN`。ADR-0023 的 Platform Audit 是另一个控制面,见
|
||||
`Spec.System.PlatformAdministration`,不复用本结构。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
/-- 审计条目的最小骨架(关系 `PINNED` / 内容 `OPEN`, likec4)。只承诺"一条审计记录
|
||||
关联到某个 run";事件类型、时间、actor、详情等字段 `OPEN`。 -/
|
||||
structure AuditEntry (I : Identifiers) where
|
||||
/-- 该审计条目所属的 run(`PINNED` 关系, likec4)。 -/
|
||||
run : I.RunId
|
||||
|
||||
end Spec.System
|
||||
@@ -1,89 +0,0 @@
|
||||
import Spec.Prelude
|
||||
|
||||
/-!
|
||||
# Capacity —— SaaS capacity admission and abuse controls (ADR-0022)
|
||||
|
||||
初始生产服务共享有限的单机资源,但不能让一个 Organization 垄断容量或让无界输入拖垮
|
||||
其他租户。ADR-0022 定义分层限制、持久 admission、显式背压和紧急制动;具体数值由
|
||||
生产式容量测试校准,保持 `OPEN`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
/-- 首个生产版本必须有硬边界的容量维度(`PINNED`, ADR-0022)。金额与 token 用量是
|
||||
统计和软告警,不在本硬限制集合中;各维度的具体数值为 `OPEN`,须由容量测试决定。 -/
|
||||
inductive CapacityDimension where
|
||||
| requestRate
|
||||
| requestBodySize
|
||||
| agentConcurrency
|
||||
| admissionQueueLength
|
||||
| admissionQueueWait
|
||||
| fileSize
|
||||
| attachmentCount
|
||||
| archiveExpansion
|
||||
| projectStorage
|
||||
| organizationStorage
|
||||
| memberCount
|
||||
| projectCount
|
||||
| teamCount
|
||||
| folderCount
|
||||
| sessionCount
|
||||
| runWallTime
|
||||
| runTurns
|
||||
| runToolCalls
|
||||
| toolWallTime
|
||||
| runOutputSize
|
||||
| processMemory
|
||||
| processCpu
|
||||
| processCount
|
||||
|
||||
/-- 一个容量维度的分层限制(`PINNED`, ADR-0022):platform ceiling 永远存在且不可被
|
||||
Organization 突破;Organization policy 可以缺省,也只能配置更低的限制。 -/
|
||||
structure LayeredLimit where
|
||||
/-- 由版本化生产部署配置提供的不可突破上限(`PINNED`, ADR-0022)。 -/
|
||||
platformCeiling : Nat
|
||||
/-- Organization 管理员可选的更低策略限制(`PINNED`, ADR-0022)。 -/
|
||||
organizationLimit : Option Nat
|
||||
|
||||
/-- 分层限制是良构的 iff Organization policy 未设置或不高于 platform ceiling
|
||||
(`PINNED`, ADR-0022)。不允许用 `none` 表示 platform unlimited。 -/
|
||||
def LayeredLimit.Valid (limit : LayeredLimit) : Prop :=
|
||||
match limit.organizationLimit with
|
||||
| none => True
|
||||
| some organizationLimit => organizationLimit ≤ limit.platformCeiling
|
||||
|
||||
/-- 有效限制(`PINNED`, ADR-0022)取 platform ceiling 与 Organization policy 中较低者;
|
||||
Organization policy 缺省时直接采用 platform ceiling,永不退化为 unlimited。 -/
|
||||
def LayeredLimit.effective (limit : LayeredLimit) : Nat :=
|
||||
match limit.organizationLimit with
|
||||
| none => limit.platformCeiling
|
||||
| some organizationLimit => min limit.platformCeiling organizationLimit
|
||||
|
||||
/-- 已被服务接受的 agent run request 状态(`PINNED`, ADR-0022)。`expired` 和
|
||||
`canceled` 都是可审计终态且不得自动执行;`started` 表示已从 admission queue 移交给
|
||||
一个 AgentRun。被容量规则拒绝的输入从未被接受,因此不伪装成 queued request。 -/
|
||||
inductive RunRequestState where
|
||||
| queued
|
||||
| started
|
||||
| expired
|
||||
| canceled
|
||||
|
||||
/-- 平台紧急工作负载制动模式(`PINNED`, ADR-0022)。`drain` 停止新 admission 与队列
|
||||
启动但允许当前 run 完成;`stopNow` 还会取消当前 run。它们不等同于删除或封禁 org。 -/
|
||||
inductive WorkloadBrakeMode where
|
||||
| open
|
||||
| drain
|
||||
| stopNow
|
||||
|
||||
/-- 紧急制动是否允许接收新的 agent 工作(`PINNED`, ADR-0022):只有 `open` 允许。 -/
|
||||
def WorkloadBrakeMode.AcceptsNew : WorkloadBrakeMode → Prop
|
||||
| .open => True
|
||||
| .drain | .stopNow => False
|
||||
|
||||
/-- 紧急制动是否允许当前 agent run 继续(`PINNED`, ADR-0022):`drain` 允许收尾,
|
||||
`stopNow` 要求取消。 -/
|
||||
def WorkloadBrakeMode.AllowsActive : WorkloadBrakeMode → Prop
|
||||
| .open | .drain => True
|
||||
| .stopNow => False
|
||||
|
||||
end Spec.System
|
||||
@@ -1,24 +0,0 @@
|
||||
import Spec.System.Connections.Prelude
|
||||
import Spec.System.Connections.Feishu
|
||||
|
||||
/-!
|
||||
# Connections —— 连接绑定与用户信息
|
||||
|
||||
组织/用户的外部连接。提供商枚举见 `Connections.Prelude`;
|
||||
飞书具体类型见 `Connections.Feishu`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
|
||||
/-- 组织连接绑定(`PINNED`)。 -/
|
||||
inductive ConnectionBinding (I : Identifiers) where
|
||||
/-- 飞书(`PINNED`)。 -/
|
||||
| feishu : FeishuAppBinding I → ConnectionBinding I
|
||||
|
||||
/-- 用户连接信息(`PINNED`)。 -/
|
||||
inductive ConnectionProfile (I : Identifiers) where
|
||||
/-- 飞书(`PINNED`)。 -/
|
||||
| feishu : FeishuProfile I → ConnectionProfile I
|
||||
|
||||
end Spec.System
|
||||
@@ -1,31 +0,0 @@
|
||||
import Spec.Prelude
|
||||
|
||||
/-!
|
||||
# Feishu —— 飞书连接
|
||||
|
||||
组织绑定一个飞书企业应用(1:1)。用户经此应用登录、调飞书 API。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
variable (I : Identifiers)
|
||||
|
||||
/-- 组织的飞书应用绑定(`PINNED`, 1:1)。 -/
|
||||
structure FeishuAppBinding where
|
||||
/-- 飞书企业应用 app_id(`OPEN` 表示)。 -/
|
||||
appId : I.FeishuAppId
|
||||
/-- app_secret 信封引用(`PINNED`, ADR-0024)。 -/
|
||||
appSecretEnvelope : I.FeishuAppSecretRef
|
||||
|
||||
/-- 用户的飞书信息(`PINNED`)。 -/
|
||||
structure FeishuProfile where
|
||||
/-- 应用内身份(`OPEN`);调 API 的直接句柄,换应用即变。 -/
|
||||
openId : I.FeishuOpenId
|
||||
/-- 租户内身份(`OPEN`);换应用不变,比 open_id 稳定。 -/
|
||||
userId : I.FeishuUserId
|
||||
/-- 显示名(`OPEN`)。 -/
|
||||
name : Option String
|
||||
/-- 头像 URL(`OPEN`)。 -/
|
||||
avatarUrl : Option String
|
||||
|
||||
end Spec.System
|
||||
@@ -1,15 +0,0 @@
|
||||
/-!
|
||||
# Connections.Prelude —— 连接提供商
|
||||
|
||||
用户/组织的外部身份连接。当前仅 IdP 类别(飞书)。
|
||||
模型 provider connection 是独立概念,见 `Spec.System.Organization`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
/-- 连接提供商(`PINNED`;当前仅飞书,未来可扩展钉钉/企微)。 -/
|
||||
inductive ConnectionProvider where
|
||||
/-- 飞书(`PINNED`)。 -/
|
||||
| feishu
|
||||
|
||||
end Spec.System
|
||||
@@ -1,46 +0,0 @@
|
||||
import Spec.Prelude
|
||||
import Spec.System.Connections
|
||||
|
||||
/-!
|
||||
# Hierarchy —— 主体层级
|
||||
|
||||
整个服务中的主体: 平台 → 组织(租户)→ 用户。
|
||||
|
||||
- **平台**(Platform): SaaS 提供方实体
|
||||
|
||||
- **组织**(Organization): SaaS 租户
|
||||
|
||||
- **用户**(User): 租户内的独立实体
|
||||
|
||||
**术语**: "管理员"一词在文档中不单独出现，避免跨层歧义。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
variable (I : Identifiers)
|
||||
/-- 平台(`PINNED`, SaaS 提供方)。只有一个,独立于组织。管理面见 `PlatformAdministration`(ADR-0023)。 -/
|
||||
structure Platform where
|
||||
/-- 平台自有飞书应用(`PINNED`, ADR-0023)。 -/
|
||||
application : I.PlatformFeishuApplicationId
|
||||
/-- 组织(`PINNED`, ADR-0020)。project/team 必须归属且仅归属一个 org。
|
||||
外部连接见 `Connections`。角色/tenancy/凭据见 `Spec.System.Organization`。 -/
|
||||
structure Organization where
|
||||
/-- 组织标识(`OPEN` 表示)。 -/
|
||||
id : I.OrganizationId
|
||||
/-- 外部连接(`PINNED`)。 -/
|
||||
connections : List (ConnectionBinding I)
|
||||
|
||||
/-- 用户(`PINNED`, 租户层独立实体)。必属一个组织。外部连接见 `Connections`。 -/
|
||||
structure User where
|
||||
/-- 用户标识(`OPEN` 表示;组织内唯一,不可改;登录用)。 -/
|
||||
id : I.UserId
|
||||
/-- 所属组织(`PINNED`, ADR-0020)。 -/
|
||||
organization : I.OrganizationId
|
||||
/-- 显示名(`PINNED`, 可改)。 -/
|
||||
displayName : String
|
||||
/-- 密码哈希(`OPEN` 表示;id + 密码登录)。 -/
|
||||
passwordHash : String
|
||||
/-- 外部连接(`PINNED`)。 -/
|
||||
connections : List (ConnectionProfile I)
|
||||
|
||||
end Spec.System
|
||||
@@ -1,34 +0,0 @@
|
||||
import Spec.Prelude
|
||||
import Spec.System.Agent.Run
|
||||
|
||||
/-!
|
||||
# Lock —— 项目锁与排他不变式
|
||||
|
||||
ADR-0002:防止并发 agent 同改一个项目,锁的 owner 是当前 `AgentRun`(不是
|
||||
teacher / chat / session)。持锁者必为非终止 run。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
variable (I : Identifiers)
|
||||
|
||||
/-- 项目级锁(`PINNED`, ADR-0002)。`owner : RunId`从类型上编码"lock owner = run_id":
|
||||
锁不可能被 session / teacher 持有。 -/
|
||||
structure ProjectAgentLock where
|
||||
/-- 作用域:项目级(`PINNED`, ADR-0002)。 -/
|
||||
scope : I.ProjectId
|
||||
/-- 持有者:一个 run(`PINNED`, ADR-0002)。 -/
|
||||
owner : I.RunId
|
||||
|
||||
/-- 锁表:每项目当前持锁 run(`PINNED` 排他性, ADR-0002)。`ProjectId → Option RunId`
|
||||
的结构本身即排他——不可能为同一项目登记两个并发 owner。 -/
|
||||
def LockTable := I.ProjectId → Option I.RunId
|
||||
|
||||
/-- 锁表良构:持锁者必为非终止 run(`PINNED`, ADR-0002)。
|
||||
|
||||
若 `p` 的锁被 `r` 持有,则 `r` 不在终止态。锁在 run 终止时释放。 -/
|
||||
def LockTable.WellFormed
|
||||
(lt : LockTable I) (statusOf : I.RunId → RunState) : Prop :=
|
||||
∀ p r, lt p = some r → ¬ (statusOf r).Terminal
|
||||
|
||||
end Spec.System
|
||||
@@ -1,129 +0,0 @@
|
||||
import Spec.Prelude
|
||||
|
||||
/-!
|
||||
# Organization —— SaaS 租户 (ADR-0020, ADR-0024)
|
||||
|
||||
组织就是租户。project/team 必须归属且仅归属一个 org;team→project grant 必须同 org。
|
||||
组织实体见 `Hierarchy.Organization`;用户见 `Spec.System.User`;平台控制面见
|
||||
`PlatformAdministration`(ADR-0023)。凭据信封见 ADR-0024。Agent 角色配置见
|
||||
`Spec.System.Agent.AgentRole`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
variable (I : Identifiers)
|
||||
|
||||
/-- 课程项目的租户归属(`PINNED`, ADR-0020):每个 project 必须有一个 organization。 -/
|
||||
structure ProjectTenancy where
|
||||
/-- 被归属的课程项目(`PINNED`, ADR-0020)。 -/
|
||||
project : I.ProjectId
|
||||
/-- project 所属 organization(`PINNED`, ADR-0020)。 -/
|
||||
organization : I.OrganizationId
|
||||
|
||||
/-- Hub team 的租户归属(`PINNED`, ADR-0020):team 是 org-scoped principal。 -/
|
||||
structure TeamTenancy where
|
||||
/-- 被归属的 Hub team(`PINNED`, ADR-0020)。 -/
|
||||
team : I.TeamId
|
||||
/-- team 所属 organization(`PINNED`, ADR-0020)。 -/
|
||||
organization : I.OrganizationId
|
||||
|
||||
/-- Team 对 project 的授权作用域(`PINNED`, ADR-0020):`PermissionGrant` 可以把
|
||||
TEAM principal 授给 PROJECT resource,但该 grant 必须同 org。role 本身仍由
|
||||
`PermissionGrant`/`Permission` 定义,这里仅刻画 tenant well-scopedness。 -/
|
||||
structure TeamProjectGrantScope where
|
||||
/-- 被授权的 project(`PINNED`, ADR-0020)。 -/
|
||||
project : I.ProjectId
|
||||
/-- 获得授权的 team principal(`PINNED`, ADR-0020)。 -/
|
||||
team : I.TeamId
|
||||
/-- Team-project grant 是良构的 iff project 与 team 解析到同一 organization
|
||||
(`PINNED`, ADR-0020)。`projectOrg`/`teamOrg` 由平台提供(表示 `OPEN`);跨 org
|
||||
team grant 必须被拒绝。 -/
|
||||
def TeamProjectGrantScope.WellScoped
|
||||
(grant : TeamProjectGrantScope I)
|
||||
(projectOrg : I.ProjectId → Option I.OrganizationId)
|
||||
(teamOrg : I.TeamId → Option I.OrganizationId) : Prop :=
|
||||
∃ o, projectOrg grant.project = some o ∧ teamOrg grant.team = some o
|
||||
|
||||
/- BYOK 由组织所有者/管理员管理;platform-managed 由平台管理员管理。两种模式都不允许
|
||||
跨 org 共用 process-global key。模式切换 `OPEN`。 -/
|
||||
inductive ProviderCredentialMode where
|
||||
| byok
|
||||
| platformManaged
|
||||
|
||||
/-- Organization 的 model provider connection(`PINNED`, ADR-0021, ADR-0024):connection
|
||||
必须归属一个且仅一个 organization,并明确采用哪一种凭据模式。凭据存为由本地版本化
|
||||
master-key keyring 包裹的不可变信封版本;业务代码只能通过显式 organization/project
|
||||
作用域的 fail-closed resolver 获得短生命周期明文,不得回退到 process-global key;Agent
|
||||
执行环境只获得 run-scoped 本地 proxy capability,不得获得 org provider 明文。 -/
|
||||
structure OrganizationProviderConnection where
|
||||
/-- connection 所属 organization(`PINNED`, ADR-0021)。 -/
|
||||
organization : I.OrganizationId
|
||||
/-- connection 的凭据归属模式(`PINNED`, ADR-0021)。 -/
|
||||
mode : ProviderCredentialMode
|
||||
|
||||
/-- Organization connection 的运行态(`PINNED`, ADR-0024):只有 `active` connection
|
||||
可被 resolver 使用;`draft` 与 `disabled` 都必须 fail closed。 -/
|
||||
inductive OrganizationConnectionStatus where
|
||||
| draft
|
||||
| active
|
||||
| disabled
|
||||
|
||||
/-- Organization secret version 的信封绑定上下文(`PINNED`, ADR-0024):认证附加数据必须
|
||||
同时绑定 organization、connection、secret version 与 purpose,因此密文不能跨行、跨 org、
|
||||
跨 connection 或跨用途替换。各标识符的数据库表示为实现细节,这里保持 opaque。 -/
|
||||
structure OrganizationSecretBinding
|
||||
(OrganizationId ConnectionId SecretVersionId Purpose : Type) where
|
||||
/-- secret 所属 organization(`PINNED`, ADR-0024)。 -/
|
||||
organization : OrganizationId
|
||||
/-- secret 所属稳定 connection(`PINNED`, ADR-0024)。 -/
|
||||
connection : ConnectionId
|
||||
/-- 不可变 secret version(`PINNED`, ADR-0024)。 -/
|
||||
secretVersion : SecretVersionId
|
||||
/-- payload 的连接类型/用途(`PINNED`, ADR-0024)。 -/
|
||||
purpose : Purpose
|
||||
|
||||
/-- 生产 secret resolver 的使用条件(`PINNED`, ADR-0024):connection 与 active secret
|
||||
必须属于请求解析出的同一 active organization,connection 必须 active,且信封必须能用其
|
||||
记录的本地 KEK 完整认证并解密。缺失/错误 key、损坏密文和任何 scope 不一致都返回失败;
|
||||
不得尝试全局环境变量凭据;Agent child 也不得接收该明文。`authenticatedEnvelope` 是
|
||||
密码学实现提供的判定。 -/
|
||||
def OrganizationSecretResolvable
|
||||
{OrganizationId ConnectionId SecretVersionId Purpose : Type}
|
||||
[BEq OrganizationId]
|
||||
(requestedOrganization : OrganizationId)
|
||||
(binding : OrganizationSecretBinding OrganizationId ConnectionId SecretVersionId Purpose)
|
||||
(organizationActive connectionActive authenticatedEnvelope : Bool) : Bool :=
|
||||
organizationActive && connectionActive &&
|
||||
(binding.organization == requestedOrganization) && authenticatedEnvelope
|
||||
|
||||
|
||||
/-- 组织成员角色(`PINNED` 封闭三档)。与项目层 `Role`、平台层 `PlatformRole` 互不相交。 -/
|
||||
inductive OrganizationRole where
|
||||
/-- 组织所有者(`PINNED`):bootstrap,独家管 owner 群体,受最后所有者保护。 -/
|
||||
| owner
|
||||
/-- 组织管理员(`PINNED`):管成员/policy/BYOK,不能管 owner 群体。 -/
|
||||
| admin
|
||||
/-- 组织成员(`PINNED`):普通成员。 -/
|
||||
| member
|
||||
|
||||
/-- 组织成员关系(`PINNED`)。 -/
|
||||
structure OrganizationMembership where
|
||||
/-- 成员(`PINNED`;独立实体,见 `Hierarchy.User`)。 -/
|
||||
user : I.UserId
|
||||
/-- 组织(`PINNED`)。 -/
|
||||
organization : I.OrganizationId
|
||||
/-- 角色(`PINNED`)。 -/
|
||||
role : OrganizationRole
|
||||
|
||||
/-- 只有组织所有者能管 owner 群体(`PINNED`)。 -/
|
||||
def CanManageOwnerGroup (actorRole : OrganizationRole) : Prop :=
|
||||
actorRole = .owner
|
||||
|
||||
/-- 最后所有者保护(`PINNED`):撤销 owner 时同 org 必须还有一个不同的 owner。 -/
|
||||
def LastOwnerProtected
|
||||
(target : OrganizationMembership I)
|
||||
(otherOwnersInOrg : List I.UserId) : Prop :=
|
||||
target.role ≠ .owner ∨
|
||||
∃ other, other ∈ otherOwnersInOrg ∧ other ≠ target.user
|
||||
|
||||
end Spec.System
|
||||
@@ -1,66 +0,0 @@
|
||||
import Spec.Prelude
|
||||
|
||||
/-!
|
||||
# Permission —— 角色、能力与授权
|
||||
|
||||
ADR-0004:权限走"飞书云文档式"——grant(`resource + principal + role`)与 settings
|
||||
分离;role 取自封闭的 `read / edit / manage`,且 **read ⊂ edit ⊂ manage** 累积赋能;
|
||||
强制释放锁是 **admin-only**,在 role 体系之外。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
/-- 协作者角色(`PINNED` 封闭, ADR-0004 逐字 "roles are read, edit, or manage")。 -/
|
||||
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` 由 ADR-0023 的 `Spec.System.PlatformAdministration` 独立判定,
|
||||
本层不把平台权力折进 project role。 -/
|
||||
def RequiresAdmin (isAdmin : Prop) : Prop := isAdmin
|
||||
|
||||
end Spec.System
|
||||
@@ -1,67 +0,0 @@
|
||||
import Spec.Prelude
|
||||
import Spec.System.Permission
|
||||
|
||||
/-!
|
||||
# PermissionGrant —— 授权与设置(ADR-0004)
|
||||
|
||||
ADR-0004 的"飞书云文档式"权限:grant(`resource × principal × role`)与 settings
|
||||
(各 policy 旋钮)分离;role 决定能力(见 `Permission`),settings 决定"此资源是否
|
||||
开某类操作"。
|
||||
|
||||
principal 子类型学(user/chat/department/…)与各 policy 值域 `OPEN`。role-capability
|
||||
与 settings-policy 如何组合成最终授权决策亦 `OPEN`——ADR-0004 把二者列为分离的闸,
|
||||
但未明文规定组合规则。ADR-0020 约束 TEAM principal 授权 PROJECT resource 时必须同
|
||||
organization,见 `Spec.System.Organization`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
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,221 +0,0 @@
|
||||
import Spec.Prelude
|
||||
|
||||
/-!
|
||||
# PlatformAdministration —— 平台管理员身份、会话与审计边界(ADR-0023)
|
||||
|
||||
平台控制面可以创建 org、写入连接凭据并制动全平台工作负载,因此不得借用客户
|
||||
`User`、`OrganizationMembership` 或 project role。ADR-0023 决定独立平台飞书 issuer、
|
||||
单一平级管理员角色、绑定身份的 invitation、可撤销服务端 session、mutation 与平台审计
|
||||
同成同败、最后管理员保护,以及无常驻账号的双因子离线恢复。
|
||||
|
||||
这些安全边界语义见下。cookie 属性、token hash、具体 TTL、审计
|
||||
字段表示/保留期、recovery key 介质和 CLI/SQL 机制 `OPEN`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
variable (I : Identifiers)
|
||||
|
||||
/-- 平台管理员的已验证外部身份(`PINNED`, ADR-0023):issuer 必须是专用
|
||||
Platform-owned Feishu Application;该身份与客户 `User`/org membership/project grant
|
||||
是不同的授权根,即使现实中是同一个人也不自动传播权限。 -/
|
||||
structure PlatformIdentity where
|
||||
/-- 平台身份自身标识(`OPEN` 表示,ADR-0023)。 -/
|
||||
id : I.PlatformIdentityId
|
||||
/-- 验证该身份的平台自有飞书应用(`PINNED`, ADR-0023)。 -/
|
||||
application : I.PlatformFeishuApplicationId
|
||||
/-- 在该平台应用作用域内验证的外部飞书用户(`PINNED` 作用域,表示 `OPEN`)。 -/
|
||||
externalUser : I.PlatformExternalUserId
|
||||
|
||||
/-- 平台身份来自当前唯一受信 platform-owned app iff identity 的 issuer 与配置的
|
||||
平台应用相同(`PINNED`, ADR-0023);不能把客户 org app 的 identity 当平台身份。 -/
|
||||
def PlatformIdentity.FromPlatformApplication
|
||||
(identity : PlatformIdentity I)
|
||||
(platformApplication : I.PlatformFeishuApplicationId) : Prop :=
|
||||
identity.application = platformApplication
|
||||
|
||||
/-- 初始平台控制面的 standing role(`PINNED` 封闭, ADR-0023):只有一个平级
|
||||
administrator;不存在 Platform Owner/Super Admin/Teacher 层级。 -/
|
||||
inductive PlatformRole where
|
||||
| administrator
|
||||
|
||||
/-- Standing Platform Administrator grant 的生命周期(`PINNED`, ADR-0023)。 -/
|
||||
inductive StandingPlatformAdminGrantState where
|
||||
| active
|
||||
| revoked
|
||||
|
||||
/-- 一个普通、长期存在的 Platform Administrator grant(`PINNED`, ADR-0023)。 -/
|
||||
structure StandingPlatformAdminGrant where
|
||||
/-- 被授予平台管理员权力的独立平台身份(`PINNED`, ADR-0023)。 -/
|
||||
identity : I.PlatformIdentityId
|
||||
/-- standing role;当前封闭集合只有 administrator(`PINNED`, ADR-0023)。 -/
|
||||
role : PlatformRole
|
||||
/-- grant 当前是否仍有效(`PINNED`, ADR-0023)。 -/
|
||||
state : StandingPlatformAdminGrantState
|
||||
|
||||
/-- Standing grant 仅在 active 状态有效(`PINNED`, ADR-0023)。 -/
|
||||
def StandingPlatformAdminGrant.Active
|
||||
(grant : StandingPlatformAdminGrant I) : Prop :=
|
||||
grant.state = .active
|
||||
|
||||
/-- 首位平台管理员 bootstrap 的前置条件(`PINNED`, ADR-0023):只有 standing admin
|
||||
集合为空时才允许;bootstrap 身份验证、审计与事务机制见 ADR,具体脚本表示 `OPEN`。 -/
|
||||
def CanBootstrapPlatformAdmin
|
||||
(activeStandingAdmins : List I.PlatformIdentityId) : Prop :=
|
||||
activeStandingAdmins = []
|
||||
|
||||
/-- 撤销 standing Platform Administrator 的最后管理员保护(`PINNED`, ADR-0023):
|
||||
target 必须当前有效,且列表中必须另有一个不同的有效管理员。Emergency grant 不计入
|
||||
standing admin 集合,不能用来绕过最后管理员保护。 -/
|
||||
def CanRevokePlatformAdmin
|
||||
(activeStandingAdmins : List I.PlatformIdentityId)
|
||||
(target : I.PlatformIdentityId) : Prop :=
|
||||
target ∈ activeStandingAdmins ∧
|
||||
∃ other, other ∈ activeStandingAdmins ∧ other ≠ target
|
||||
|
||||
/-- Platform Administrator invitation 的生命周期(`PINNED`, ADR-0023):accepted/
|
||||
expired/revoked 都是终态,所以邀请只能成功领取一次。 -/
|
||||
inductive PlatformAdminInvitationState where
|
||||
| pending
|
||||
| accepted
|
||||
| expired
|
||||
| revoked
|
||||
|
||||
/-- 一个短期、单次且绑定具体平台飞书账号的管理员邀请(`PINNED`, ADR-0023)。 -/
|
||||
structure PlatformAdminInvitation where
|
||||
/-- invitation 标识(`OPEN` 表示,ADR-0023)。 -/
|
||||
id : I.PlatformInvitationId
|
||||
/-- 预期账号必须来自这个平台自有飞书应用(`PINNED`, ADR-0023)。 -/
|
||||
application : I.PlatformFeishuApplicationId
|
||||
/-- 只有这个预期飞书账号可领取;链接本身不是 bearer admin 权力(`PINNED`)。 -/
|
||||
expectedExternalUser : I.PlatformExternalUserId
|
||||
/-- 邀请过期的逻辑时刻(`PINNED` 有限寿命,数值单位/上限 `OPEN`)。 -/
|
||||
expiresAt : Nat
|
||||
/-- 邀请当前状态(`PINNED`, ADR-0023)。 -/
|
||||
state : PlatformAdminInvitationState
|
||||
|
||||
/-- 邀请可领取 iff 尚 pending、未过期且已验证 identity 与邀请绑定的 app+用户一致
|
||||
(`PINNED`, ADR-0023)。 -/
|
||||
def PlatformAdminInvitation.CanAccept
|
||||
(invitation : PlatformAdminInvitation I)
|
||||
(identity : PlatformIdentity I)
|
||||
(now : Nat) : Prop :=
|
||||
invitation.state = .pending ∧
|
||||
now < invitation.expiresAt ∧
|
||||
identity.application = invitation.application ∧
|
||||
identity.externalUser = invitation.expectedExternalUser
|
||||
|
||||
/-- 邀请状态转换(`PINNED`, ADR-0023):pending 只能结束为 accepted/expired/revoked;
|
||||
任何终态都不能回到 pending 或再次 accepted。 -/
|
||||
def PlatformAdminInvitation.ValidTransition :
|
||||
PlatformAdminInvitationState → PlatformAdminInvitationState → Prop
|
||||
| .pending, .accepted | .pending, .expired | .pending, .revoked => True
|
||||
| _, _ => False
|
||||
|
||||
/-- 服务端 Platform Session 的生命周期(`PINNED`, ADR-0023)。 -/
|
||||
inductive PlatformSessionState where
|
||||
| active
|
||||
| revoked
|
||||
| expired
|
||||
|
||||
/-- 独立平台会话(`PINNED`, ADR-0023):只绑定 Platform Identity,不携带 org/project
|
||||
权力;opaque cookie/token、hash 与 TTL 表示为 `OPEN`。 -/
|
||||
structure PlatformSession where
|
||||
/-- 平台会话标识(`OPEN` 表示,ADR-0023)。 -/
|
||||
id : I.PlatformSessionId
|
||||
/-- 会话认证的独立平台身份(`PINNED`, ADR-0023)。 -/
|
||||
identity : I.PlatformIdentityId
|
||||
/-- 服务端可立即撤销/过期的状态(`PINNED`, ADR-0023)。 -/
|
||||
state : PlatformSessionState
|
||||
|
||||
/-- 双因子离线恢复授权(`PINNED`, ADR-0023):受控主机权限、主机外 recovery key 与
|
||||
已声明 incident 三项都存在才是受支持的 recovery;具体因子实现与保管介质 `OPEN`。 -/
|
||||
structure PlatformRecoveryAuthorization where
|
||||
/-- 已验证受控生产主机权限(`PINNED`, ADR-0023)。 -/
|
||||
hostControl : Bool
|
||||
/-- 已验证独立的主机外 recovery key(`PINNED`, ADR-0023)。 -/
|
||||
offlineRecoveryKey : Bool
|
||||
/-- 操作绑定了 incident id 与原因(`PINNED`, ADR-0023)。 -/
|
||||
incidentDeclared : Bool
|
||||
|
||||
/-- Recovery authorization 只有三项因子均为真时有效(`PINNED`, ADR-0023)。 -/
|
||||
def PlatformRecoveryAuthorization.Valid
|
||||
(authorization : PlatformRecoveryAuthorization) : Prop :=
|
||||
authorization.hostControl = true ∧
|
||||
authorization.offlineRecoveryKey = true ∧
|
||||
authorization.incidentDeclared = true
|
||||
|
||||
/-- 只有有效双因子 recovery authorization 才能签发 Emergency Platform Grant
|
||||
(`PINNED`, ADR-0023);不存在普通 web session 直接创建 break-glass 权力的路径。 -/
|
||||
def CanIssueEmergencyPlatformGrant
|
||||
(authorization : PlatformRecoveryAuthorization) : Prop :=
|
||||
authorization.Valid
|
||||
|
||||
/-- 无常驻 break-glass 账号的短期紧急授权(`PINNED`, ADR-0023)。它不属于 standing
|
||||
role,必须绑定已声明 incident,自动过期且可在恢复完成时提前关闭。 -/
|
||||
structure EmergencyPlatformGrant where
|
||||
/-- 获得临时平台权力的已验证 Platform Identity(`PINNED`, ADR-0023)。 -/
|
||||
identity : I.PlatformIdentityId
|
||||
/-- 触发该授权的 incident(`PINNED`, ADR-0023)。 -/
|
||||
incident : I.PlatformIncidentId
|
||||
/-- 自动过期的逻辑时刻(`PINNED` 有限寿命,数值单位/上限 `OPEN`)。 -/
|
||||
expiresAt : Nat
|
||||
/-- 恢复完成后是否已显式关闭(`PINNED`, ADR-0023)。 -/
|
||||
closed : Bool
|
||||
|
||||
/-- Emergency grant 仅在未关闭且未到期时有效(`PINNED`, ADR-0023)。 -/
|
||||
def EmergencyPlatformGrant.Active
|
||||
(grant : EmergencyPlatformGrant I) (now : Nat) : Prop :=
|
||||
grant.closed = false ∧ now < grant.expiresAt
|
||||
|
||||
/-- 每次平台请求的授权条件(`PINNED`, ADR-0023):session 必须仍为 active,且请求时
|
||||
重新解析到 active standing grant 或同 identity 的未关闭、未过期 emergency grant。
|
||||
cookie 内曾经出现过 role claim 不能代替这次解析。 -/
|
||||
def PlatformSession.Authorized
|
||||
(session : PlatformSession I)
|
||||
(standingGrants : List (StandingPlatformAdminGrant I))
|
||||
(emergencyGrants : List (EmergencyPlatformGrant I))
|
||||
(now : Nat) : Prop :=
|
||||
session.state = .active ∧
|
||||
((∃ grant, grant ∈ standingGrants ∧
|
||||
grant.identity = session.identity ∧
|
||||
StandingPlatformAdminGrant.Active I grant) ∨
|
||||
∃ grant, grant ∈ emergencyGrants ∧
|
||||
grant.identity = session.identity ∧
|
||||
EmergencyPlatformGrant.Active I grant now)
|
||||
|
||||
/-- 必须做近期 OAuth step-up 的平台敏感操作集合(`PINNED`, ADR-0023;未来新增敏感
|
||||
操作时可扩):管理员生命周期、飞书连接、platform-managed provider 凭据、org 生命周期、
|
||||
workload brake 与 emergency grant 都不能只凭旧 session。 -/
|
||||
inductive PlatformSensitiveAction where
|
||||
| administratorLifecycle
|
||||
| feishuConnection
|
||||
| platformManagedProviderCredential
|
||||
| organizationLifecycle
|
||||
| workloadBrake
|
||||
| emergencyGrant
|
||||
|
||||
/-- 敏感操作授权必须提供"近期重新认证"事实(`PINNED`, ADR-0023);具体时间窗 `OPEN`,
|
||||
由 browser/session 决策给出受检上限。 -/
|
||||
def PlatformSensitiveAction.Authorized
|
||||
(_action : PlatformSensitiveAction)
|
||||
(recentAuthentication : Prop) : Prop :=
|
||||
recentAuthentication
|
||||
|
||||
/-- 一个成功平台 mutation 与其独立 Platform Audit Entry 的原子提交事实(`PINNED`,
|
||||
ADR-0023):没有 audit entry 就不存在合法成功 commit;具体数据库事务机制 `OPEN`。 -/
|
||||
structure PlatformMutationCommit where
|
||||
/-- 成功的平台 mutation(`PINNED`, ADR-0023)。 -/
|
||||
mutation : I.PlatformMutationId
|
||||
/-- 与 mutation 同成同败的 append-only 平台审计条目(`PINNED`, ADR-0023)。 -/
|
||||
auditEntry : I.PlatformAuditEntryId
|
||||
|
||||
/-- Organization 管理员可读的平台审计脱敏投影(`PINNED`, ADR-0023):只关联影响该
|
||||
Organization 的 entry;完整平台审计和其他 org entry 不经此投影暴露。 -/
|
||||
structure OrganizationPlatformAuditProjection where
|
||||
/-- 被投影的平台审计条目(`PINNED`, ADR-0023)。 -/
|
||||
auditEntry : I.PlatformAuditEntryId
|
||||
/-- 唯一可见该投影的受影响 Organization(`PINNED`, ADR-0023)。 -/
|
||||
organization : I.OrganizationId
|
||||
|
||||
end Spec.System
|
||||
@@ -1,75 +0,0 @@
|
||||
import Spec.Prelude
|
||||
|
||||
/-!
|
||||
# ProjectGroup —— 飞书项目群作为协作空间(ADR-0001/0017)
|
||||
|
||||
一个 project 对应一个长生命周期飞书项目群;群是协作空间,不持锁(锁归 `AgentRun`,
|
||||
见 `Lock` / ADR-0002)。群可在无 agent 处理时保持开启;教师离群/静音与项目权限、
|
||||
与 agent 生命周期相互独立。
|
||||
|
||||
**绑定历史(`PINNED`, ADR-0021):** active binding 严格 1:1;实现可保留 archived
|
||||
historical binding rows 供审计,但 `GroupBinding` 谓词只刻画当前 active 快照。
|
||||
群解散/不可达的自动化处理 `OPEN`;pilot 纠错由 org admin 显式归档绑定。
|
||||
|
||||
**当前角色(`PINNED`, ADR-0017):** active binding 选择一个 Organization-scoped Agent
|
||||
role;普通群消息在接收时冻结该 role,随后即使群切换角色,已接收工作也不漂移。切换角色
|
||||
只改变后续工作路由,不把不同 role 的 provider session 合并。每个 Organization 有一个
|
||||
active 默认 role 用于初始化新 binding,role 名称不硬编码。切换共享 role 的 actor 必须同时
|
||||
通过 project `agent.trigger` 与目标 role `role.trigger`;不额外要求 project `MANAGE`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
variable (I : Identifiers)
|
||||
|
||||
/-- 飞书项目群(`PINNED` 长生命周期协作空间, ADR-0001)。承载 project 与飞书 chat 的
|
||||
绑定;不持锁(锁归 `AgentRun`,见 `Lock`)。 -/
|
||||
structure ProjectGroup where
|
||||
/-- 群对应的飞书 chat(`PINNED` 关系, ADR-0001;chat 标识见 `Identifiers.ChatId`)。 -/
|
||||
chat : I.ChatId
|
||||
|
||||
/-- 项目↔active 群绑定表(`PINNED` 每项目至多一个 active 群, ADR-0001/0021)。
|
||||
`ProjectId → Option ChatId` 的结构本身即"一个 project 至多绑一个 active 群"(由 `Option`
|
||||
自带);良构补另一半——单射。 -/
|
||||
def GroupBinding := I.ProjectId → Option I.ChatId
|
||||
|
||||
/-- Active 绑定良构:单射——不同 project 不绑同一 active chat(`PINNED`, ADR-0001/0021)。
|
||||
"每 project 至多一个群"由 `Option` 结构自带;这条约束"每群至多属于一个 project"。
|
||||
archived historical bindings 不在本快照不变式内。 -/
|
||||
def GroupBinding.WellFormed (b : GroupBinding I) : Prop :=
|
||||
∀ p₁ p₂ c, b p₁ = some c → b p₂ = some c → p₁ = p₂
|
||||
|
||||
/-- 每个 Organization 的 active 默认 Agent role(`PINNED`, ADR-0017)。函数形状钉死每个
|
||||
Organization 恰好一个默认值;role 是否 active 及租户归属由 `WellScoped` 约束。 -/
|
||||
def OrganizationDefaultRole := I.OrganizationId → I.AgentRoleId
|
||||
|
||||
/-- 默认 role 必须属于作为其 key 的同一个 Organization(`PINNED`, ADR-0017)。 -/
|
||||
def OrganizationDefaultRole.WellScoped
|
||||
(defaults : OrganizationDefaultRole I)
|
||||
(roleOrg : I.AgentRoleId → Option I.OrganizationId) : Prop :=
|
||||
∀ o, roleOrg (defaults o) = some o
|
||||
|
||||
/-- Active 项目群选择的 Agent role(`PINNED`, ADR-0017)。role 属于项目 Organization;
|
||||
具体外键表示是 plumbing,由 `WellScoped` 钉死租户边界。 -/
|
||||
structure GroupSelectedRole where
|
||||
/-- 被选择 role 的项目。 -/
|
||||
project : I.ProjectId
|
||||
/-- 作用于该项目 active 群的动态 Agent role。 -/
|
||||
role : I.AgentRoleId
|
||||
|
||||
/-- 群所选 role 必须与 project 同 Organization(`PINNED`, ADR-0017)。 -/
|
||||
def GroupSelectedRole.WellScoped
|
||||
(selection : GroupSelectedRole I)
|
||||
(projectOrg : I.ProjectId → Option I.OrganizationId)
|
||||
(roleOrg : I.AgentRoleId → Option I.OrganizationId) : Prop :=
|
||||
∃ o, projectOrg selection.project = some o ∧ roleOrg selection.role = some o
|
||||
|
||||
/-- 已接收群工作冻结其 role(`PINNED`, ADR-0017):调度时使用 admission 中记录的 role,
|
||||
而不是重新读取可能已经变化的群当前 role。 -/
|
||||
structure GroupRunRoleSnapshot where
|
||||
/-- 被接收的一次 run。 -/
|
||||
run : I.RunId
|
||||
/-- 接收时冻结的 role。 -/
|
||||
role : I.AgentRoleId
|
||||
|
||||
end Spec.System
|
||||
@@ -1,53 +0,0 @@
|
||||
import Spec.Prelude
|
||||
|
||||
/-!
|
||||
# ProjectWorkspace —— project explorer 与飞书建项入口(ADR-0021)
|
||||
|
||||
org 后台里的"文件管理器式"项目管理:folder 只负责导航、排序、层级与用量聚合,当前
|
||||
不是权限资源。project 仍是授权边界。
|
||||
|
||||
不变量:folder/project 同 org、folder 不参与权限、普通成员从飞书群创建 project 受
|
||||
org policy 控制。folder visibility/team policy/继承授权 `OPEN`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
variable (I : Identifiers)
|
||||
|
||||
/-- Project explorer folder 的租户归属(`PINNED`, ADR-0021):folder 是 org 内透明节点。 -/
|
||||
structure FolderTenancy where
|
||||
/-- 被归属的 folder(`PINNED`, ADR-0021)。 -/
|
||||
folder : I.FolderId
|
||||
/-- folder 所属 organization(`PINNED`, ADR-0021)。 -/
|
||||
organization : I.OrganizationId
|
||||
|
||||
/-- Project 放入 folder 的作用域(`PINNED`, ADR-0021):project 可以位于某个 folder,
|
||||
但二者必须同 org。folder 不改变 project 权限。 -/
|
||||
structure ProjectFolderPlacement where
|
||||
/-- 被放置的 project(`PINNED`, ADR-0021)。 -/
|
||||
project : I.ProjectId
|
||||
/-- project 所在 folder(`PINNED`, ADR-0021)。 -/
|
||||
folder : I.FolderId
|
||||
|
||||
/-- Project-folder placement 是良构的 iff project 与 folder 解析到同一 organization
|
||||
(`PINNED`, ADR-0021)。 -/
|
||||
def ProjectFolderPlacement.WellScoped
|
||||
(placement : ProjectFolderPlacement I)
|
||||
(projectOrg : I.ProjectId → Option I.OrganizationId)
|
||||
(folderOrg : I.FolderId → Option I.OrganizationId) : Prop :=
|
||||
∃ o, projectOrg placement.project = some o ∧ folderOrg placement.folder = some o
|
||||
|
||||
/-- Folder 当前透明(`PINNED`, ADR-0021):folder 不是权限资源,不持有 grants,移动 project
|
||||
不改变 project 自身授权。未来 folder policy 若出现,须新增显式语义。 -/
|
||||
structure FolderTransparent where
|
||||
/-- 透明性命题本身;字段存在是为了让 contract 明确可引用(`PINNED`, ADR-0021)。 -/
|
||||
current : True
|
||||
|
||||
/-- 普通 org member 是否可从 Feishu 群自助创建 project 的 org policy(`PINNED`, ADR-0021)。 -/
|
||||
structure MemberProjectCreationPolicy where
|
||||
/-- policy 所属 organization(`PINNED`, ADR-0021)。 -/
|
||||
organization : I.OrganizationId
|
||||
/-- 为 true 时普通成员可从未绑定飞书群创建 project;owner/admin 可走后台入口。 -/
|
||||
membersCanCreateProjects : Bool
|
||||
|
||||
end Spec.System
|
||||
@@ -1,12 +0,0 @@
|
||||
import Spec.Prelude
|
||||
|
||||
/-!
|
||||
# User —— 用户创建路径
|
||||
|
||||
用户实体见 `Hierarchy.User`;外部连接见 `Spec.System.Connections`。
|
||||
|
||||
用户创建当前只定义管理员直接创建;飞书自助注册→管理员审批 `OPEN`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
end Spec.System
|
||||
@@ -1,6 +0,0 @@
|
||||
{"version": "1.2.0",
|
||||
"packagesDir": ".lake/packages",
|
||||
"packages": [],
|
||||
"name": "Spec",
|
||||
"lakeDir": ".lake",
|
||||
"fixedToolchain": false}
|
||||
@@ -1,6 +0,0 @@
|
||||
name = "Spec"
|
||||
version = "0.1.0"
|
||||
defaultTargets = ["Spec"]
|
||||
|
||||
[[lean_lib]]
|
||||
name = "Spec"
|
||||
@@ -1 +0,0 @@
|
||||
leanprover/lean4:v4.31.0
|
||||
Reference in New Issue
Block a user