Files

T

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>

2026-06-21 22:00:18 +08:00

1.0 KiB

Raw Permalink Blame History

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.

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.

1.0 KiB Raw Permalink Blame History