forked from bai/curriculum-project-hub
chore: scaffold monorepo with spec/ Lean project and governance docs
- spec/: freshly initialized Lean library project (lake init, v4.31.0), no deps - .gitea/workflows/spec-check.yml: CI running lake build on spec/ (well-formedness gate, not a spec-to-impl gate) - README.md: monorepo overview + the 5 "constitution" rules positioning spec/ as upstream semantic master - CLAUDE.md: global agent manual - spec/README.md: contract writing conventions (prose+type, PINNED/OPEN/ADR tags, no sorry) - docs/adr/0001-0004: system-level decision records (retrieved from main) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
@@ -0,0 +1,20 @@
|
||||
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
|
||||
@@ -0,0 +1,6 @@
|
||||
# Lean / Lake build artifacts (spec/ has its own .gitignore too)
|
||||
.lake/
|
||||
**/.lake/
|
||||
|
||||
# OS / editor
|
||||
.DS_Store
|
||||
@@ -0,0 +1,20 @@
|
||||
# CLAUDE.md —— agent 操作手册(全 repo)
|
||||
|
||||
本 repo 是 monorepo。先读根 `README.md` 的"宪法"5 条,那是一切工作的前提。本文件是给在这里干活的 coding agent 的纪律。
|
||||
|
||||
## 这个 repo 是什么
|
||||
|
||||
- `spec/` 是一份**人机共识的契约**(Lean 语义母本),是产品语义的上游参照。
|
||||
- 其余部件(将来的 `spec/` 外文件夹)是**向 `spec/` 对齐的实现**。
|
||||
|
||||
## 纪律
|
||||
|
||||
1. **不得用预训练先验脑补本领域。** 这个领域很新,你没有相关先验。契约里 prose doc 注释是语义的唯一权威来源;契约没写的,就是没定的。
|
||||
|
||||
2. **凡契约未写明者,不得假设。** 遇到标了 `OPEN` 的地方,或契约根本没覆盖的地方,**显式 surface 出来**让开发者决定,绝不擅自替它选一个解。
|
||||
|
||||
3. **改 `spec/` 必须保持其 `lake build` 通过。** 在 `spec/` 目录下跑 `lake build`。新增声明必须带 `/-- … -/` doc 注释和恰当标签(`PINNED` / `OPEN` / `ADR-NNNN`)。规范见 `spec/README.md`。不准用 `sorry` 把 build 糊绿。
|
||||
|
||||
4. **实现向契约对齐;偏离必须 surface。** 没有 CI gate 替你把关 spec↔实现的一致性(见宪法第 2 条)——这道对齐靠 review 和你巡逻 diff。发现实现与契约不一致时,报告它,不要默默让其中一边将就另一边。
|
||||
|
||||
5. **写操作谨慎。** 线上操作、git 写操作前与开发者确认(这是开发者的全局偏好)。
|
||||
@@ -0,0 +1,42 @@
|
||||
# curriculum-project-hub
|
||||
|
||||
教研生产的数字化解决方案。核心思路:课程像 DAW / 剪辑软件那样有一个**结构化的工程文件**;coding agent 协助编辑它;一个 rule-based checker(类编译器)校验其合法性并给出 helpful fix hint。目标是把教研从一次性的文档,沉淀成**可累积、可校验、可复用的资产**。
|
||||
|
||||
这是一个 **monorepo**。它的组织方式本身就表达了一条原则:**`spec/` 是上游的语义母本,其余部件是向它对齐的实现。**
|
||||
|
||||
## 仓库布局
|
||||
|
||||
```
|
||||
README.md ← 本文件:总览 + 宪法(下面 5 条)
|
||||
CLAUDE.md ← 全局 agent 操作手册(管整个 repo)
|
||||
docs/adr/ ← 系统级架构决策记录(跨部件,被 spec 契约引用)
|
||||
spec/ ← Lean 语义母本(自包含的 Lean 工程)。见 spec/README.md
|
||||
(hub/ checker/ …) ← 将来的各部件实现,平级于 spec/。尚未创建
|
||||
```
|
||||
|
||||
`spec/` 与实现部件**物理分离、平级共存**:谁是上游、谁向谁对齐,一眼可见。
|
||||
|
||||
## 宪法
|
||||
|
||||
这 5 条是 `spec/` 这份语义母本的定位与约束,是本仓库一切工作的前提。
|
||||
|
||||
1. **角色 —— Lean 是研发侧的上游参照。**
|
||||
`spec/` 用 Lean 编写,是开发者(领域专家)与 coding agent **共用**的 spec 工具,用来沉淀产品各部件的**语义**。它**不进入产品运行时**——产品里"站在 Lean 这个位置"的那个 checker 用什么技术实现,尚未决定;但那个东西的语义,先在 `spec/` 里固定下来。
|
||||
|
||||
2. **对齐机制 —— Lean 只做上游参照。**
|
||||
不做 extract / codegen,不派生 conformance test,CI 里**没有** spec→实现的 gate。实现对齐 spec,由"开发者 review + agent 巡逻 diff"这个人肉环节承载。
|
||||
(CI 里的 `spec check` 只验 spec **自身**能否 type-check,即契约内部良构,不是 spec↔实现的对齐检查。)
|
||||
|
||||
3. **资产性 —— 由 review 纪律承载,无机器兜底。**
|
||||
这份仓库给你的是"精确、自洽、机器验内部良构的语义共识",**不是**"实现正确性保证"。spec 与实现之间那道缝,是我们自愿用人来守的——清醒地守,它就是资产;放任实现漂移而不回头同步,它就退化成最贵的过期文档。
|
||||
|
||||
4. **形态 —— 它是人机共识的契约。**
|
||||
契约必须**自包含**:凡契约未明文规定的,开发者与 agent 双方都不该假设。这比"文档"严格——type checker 会逼这份契约在结构上无洞。
|
||||
|
||||
5. **深度判据 —— 只收录分歧点。**
|
||||
一条语义该不该写进 Lean,取决于一句话:**"不写明,开发者与 agent 会不会各自做出不同假设?"** 会 → 进契约;显然的东西 / 纯 plumbing / 普通 CRUD 字段 → 不进(写进去只稀释信噪比、增加维护面)。
|
||||
深度上限不是 Lean 的表达力,而是**你愿意在每次实现变更时手动回头同步的量**——写得比你能维护的更深,多出来的部分会率先过期、反过来误导实现。
|
||||
|
||||
## CI
|
||||
|
||||
`.gitea/workflows/spec-check.yml` 在每次 push / PR 时于 `spec/` 下跑 `lake build`,确保契约始终 type-check 通过(从第一天起就是"绿"的)。这是良构 gate,见宪法第 2 条。
|
||||
@@ -0,0 +1,29 @@
|
||||
# ADR 0001: Feishu Project Group Is The Collaboration Space
|
||||
|
||||
## Status
|
||||
|
||||
Accepted.
|
||||
|
||||
## Context
|
||||
|
||||
Teachers need to work on multiple curriculum projects at the same time. The previous mental model tied a teacher to one active project session, which makes multi-open workflows awkward and turns "exit project" into a confusing concept.
|
||||
|
||||
The revised product model is:
|
||||
|
||||
- one project has one long-lived Feishu project group;
|
||||
- teachers discuss freely in the group;
|
||||
- Claude does not process every group message;
|
||||
- a teacher explicitly `@Claude` when Claude should join the current context and do work.
|
||||
|
||||
## Decision
|
||||
|
||||
Treat the project group as a long-lived collaboration space, not as a lock owner and not as a temporary processing session.
|
||||
|
||||
The group can stay open while no Claude processing is active. A teacher leaving or muting a group is separate from project permissions and from Claude processing lifecycle.
|
||||
|
||||
## Consequences
|
||||
|
||||
- Multi-open is natural: a teacher participates in multiple project groups.
|
||||
- Normal group discussion does not occupy the project.
|
||||
- "Exit project" should not be the normal action in the group workflow.
|
||||
- Project rebinding or group archival needs explicit product rules, separate from run cancellation.
|
||||
@@ -0,0 +1,30 @@
|
||||
# ADR 0002: Project Lock Is Owned By AgentRun
|
||||
|
||||
## Status
|
||||
|
||||
Accepted.
|
||||
|
||||
## Context
|
||||
|
||||
The older model effectively made a long-lived teacher/project session hold the project lock. That breaks down once project groups become long-lived collaboration spaces and Claude is invoked on demand.
|
||||
|
||||
We need to prevent concurrent Claude executions from modifying the same project, while still allowing teachers to keep discussing the project in the group.
|
||||
|
||||
## Decision
|
||||
|
||||
Use a project-scoped lock whose owner is the current `AgentRun`.
|
||||
|
||||
```text
|
||||
scope = project_id
|
||||
owner = run_id
|
||||
lifetime = one Claude processing task
|
||||
```
|
||||
|
||||
The lock is acquired after `@Claude` creates an `AgentRun`, and released when the run completes, fails, times out or is canceled.
|
||||
|
||||
## Consequences
|
||||
|
||||
- Group membership, teacher identity and Claude provider session do not directly own the lock.
|
||||
- The same long-lived `AgentSession` can be reused by many runs.
|
||||
- `cancel current processing` releases the lock by `run_id`.
|
||||
- Admin `force release` remains an exceptional operation for stuck runs or lost processes.
|
||||
@@ -0,0 +1,29 @@
|
||||
# ADR 0003: Read Feishu Context On Demand
|
||||
|
||||
## Status
|
||||
|
||||
Proposed.
|
||||
|
||||
## Context
|
||||
|
||||
The system needs to give Claude enough context when a teacher invokes it from a project group. Storing full Feishu group history in the Hub adds retention and privacy concerns, while fixed time windows such as "recent 24 hours" are brittle.
|
||||
|
||||
Feishu provides message history APIs, so the Hub can keep stable anchors and read nearby context when needed.
|
||||
|
||||
## Decision
|
||||
|
||||
For the first architecture, the Hub stores minimal anchors and project memory instead of full Feishu message history:
|
||||
|
||||
- chat id and project binding;
|
||||
- trigger message id;
|
||||
- run id and status card id;
|
||||
- reply/thread anchors;
|
||||
- project memory, decisions and artifact references.
|
||||
|
||||
Claude gets seed context from the current trigger message, project memory and recent anchors. If more context is needed, Claude calls MCP tools to read current message, reply chain, thread history or recent group messages through Feishu APIs.
|
||||
|
||||
## Consequences
|
||||
|
||||
- The Hub avoids becoming a full chat history store.
|
||||
- Search over old vague discussions is limited until we add summary or indexing.
|
||||
- MCP tools must authorize by run/project context; Claude cannot pass arbitrary chat ids.
|
||||
@@ -0,0 +1,54 @@
|
||||
# ADR 0004: Use Feishu Docs-like Permission Grants
|
||||
|
||||
## Status
|
||||
|
||||
Proposed.
|
||||
|
||||
## Context
|
||||
|
||||
Project collaboration needs more nuance than a hard-coded `owner / teacher / admin` model. Teachers may need to view a project, discuss it, trigger Claude, edit artifacts, manage members, or handle exceptional cancellation. These are related but not identical privileges.
|
||||
|
||||
Feishu cloud docs separates collaborators from operation settings:
|
||||
|
||||
- collaborators can be users, groups, departments, user groups, apps, or wiki members;
|
||||
- collaborator roles are read, edit, or manage;
|
||||
- settings separately control sharing outside the organization, copying/downloading, commenting, and collaborator management.
|
||||
|
||||
That split maps well to Curriculum Project Hub.
|
||||
|
||||
## Decision
|
||||
|
||||
Model project permissions as:
|
||||
|
||||
```text
|
||||
PermissionGrant
|
||||
- resource_type: project | artifact | project_group
|
||||
- resource_id
|
||||
- principal_type: user | feishu_chat | department | user_group | app
|
||||
- principal_id
|
||||
- role: read | edit | manage
|
||||
|
||||
PermissionSettings
|
||||
- resource_type
|
||||
- resource_id
|
||||
- external_share_policy
|
||||
- comment_policy
|
||||
- copy_download_policy
|
||||
- collaborator_management_policy
|
||||
- agent_trigger_policy
|
||||
- agent_cancel_policy
|
||||
```
|
||||
|
||||
Use role-derived capabilities for ordinary actions, and settings for policy knobs:
|
||||
|
||||
- `read`: view project, artifacts, run history and project group metadata.
|
||||
- `edit`: read plus discuss, comment, edit artifacts, trigger Claude runs and answer Claude choice cards.
|
||||
- `manage`: edit plus manage collaborators, project settings, group binding and normal run cancellation policy.
|
||||
- admin-only override: force release stuck locks and perform exceptional audit operations.
|
||||
|
||||
## Consequences
|
||||
|
||||
- We can grant access to a teacher, a whole Feishu project group, a department, or a custom user group using the same model.
|
||||
- Claude invocation is explicit policy, not just "anyone in the group can run it" forever.
|
||||
- "Who can cancel current processing" can be different from "who can force release a stuck lock".
|
||||
- The model stays close to Feishu users' expectations without copying every Feishu-specific API detail.
|
||||
@@ -0,0 +1 @@
|
||||
/.lake
|
||||
@@ -0,0 +1,55 @@
|
||||
# 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.Run`、`Spec.Courseware.Validity`。
|
||||
- **类型**:PascalCase。
|
||||
- **谓词 / `Prop`**:用意图清晰的命名,如 `Legal…`、`ValidTransition`、`Can…`。
|
||||
- **文件粒度**:原则上"一个带独立不变式的概念一个文件"。
|
||||
@@ -0,0 +1,3 @@
|
||||
-- This module serves as the root of the `Spec` library.
|
||||
-- Import modules here that should be built as part of the library.
|
||||
import Spec.Basic
|
||||
@@ -0,0 +1 @@
|
||||
def hello := "world"
|
||||
@@ -0,0 +1,6 @@
|
||||
{"version": "1.2.0",
|
||||
"packagesDir": ".lake/packages",
|
||||
"packages": [],
|
||||
"name": "Spec",
|
||||
"lakeDir": ".lake",
|
||||
"fixedToolchain": false}
|
||||
@@ -0,0 +1,6 @@
|
||||
name = "Spec"
|
||||
version = "0.1.0"
|
||||
defaultTargets = ["Spec"]
|
||||
|
||||
[[lean_lib]]
|
||||
name = "Spec"
|
||||
@@ -0,0 +1 @@
|
||||
leanprover/lean4:v4.31.0
|
||||
Reference in New Issue
Block a user