[Autoform] Harden collaborative textbook workflows

.claude-plugin/marketplace.json

@@ -1,15 +1,15 @@
 {
   "$schema": "https://anthropic.com/claude-code/marketplace.schema.json",
   "name": "autoform",
-  "description": "Lean repository setup, Markdown-vault roadmaps, proving, and human or agent review with Lean LSP and REPL tools.",
+  "description": "Lean repository setup, Markdown-vault roadmaps, publication, and human or agent review with Lean LSP and REPL tools.",
   "owner": {
     "name": "Vivien Cabannes",
     "url": "https://github.com/facebookresearch/autoform-bot"
   },
   "plugins": [
     {
       "name": "autoform",
-      "description": "Set up, plan, publish, prove, and review Lean formalizations as linked Markdown nodes checked through Lean LSP and REPL.",
+      "description": "Set up, plan, publish, and review Lean formalizations as linked Markdown nodes checked through Lean LSP and REPL.",
       "source": "./",
       "category": "productivity"
     }

.claude-plugin/plugin.json

@@ -1,6 +1,6 @@
 {
   "name": "autoform",
-  "description": "Set up Lean repositories, build source-grounded Markdown roadmaps, and support human or agent review with Lean LSP and REPL tools.",
+  "description": "Set up Lean repositories, build source-grounded Markdown roadmaps, orchestrate ready work, and support human or agent review with Lean LSP and REPL tools.",
   "version": "0.5.0",
   "author": {
     "name": "Vivien Cabannes",

.codex-plugin/plugin.json

@@ -1,7 +1,7 @@
 {
   "name": "autoform",
   "version": "0.5.0+codex.20260812000640",
-  "description": "Set up Lean repositories, build source-grounded Markdown roadmaps, and support human or agent review.",
+  "description": "Set up Lean repositories, build source-grounded Markdown roadmaps, orchestrate ready work, and support human or agent review.",
   "author": {
     "name": "Vivien Cabannes"
   },
@@ -21,6 +21,7 @@
     "defaultPrompt": [
       "Set up this Lean repository with an Autoform vault, verification CI, and GitHub Pages without planning the mathematics.",
       "Build or refine an Autoform roadmap from my mathematical sources.",
+      "Work through ready nodes using the Autoform CLI and durable claims.",
       "Prepare the visual blueprint surfaces so I can review this formalization.",
       "Judge this roadmap or Lean formalization with evidence-based review rubrics.",
       "Develop Autoform itself through its executable formalization example."

.github/workflows/tests.yml

@@ -2,15 +2,72 @@ name: tests
 
 on:
   push:
+    branches: [main]
   pull_request:
 
 permissions:
   contents: read
 
+concurrency:
+  group: tests-${{ github.ref }}
+  cancel-in-progress: true
+
 jobs:
-  test:
+  deterministic:
+    name: deterministic (Python ${{ matrix.python-version }})
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    strategy:
+      fail-fast: false
+      matrix:
+        python-version: ["3.10", "3.13"]
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
+        with:
+          version: "0.12.1"
+          python-version: ${{ matrix.python-version }}
+          enable-cache: true
+      - name: Install locked development environment
+        run: timeout --signal=TERM --kill-after=30s 3m uv sync --frozen --extra dev --extra repl
+      - name: Run deterministic tests
+        run: timeout --signal=TERM --kill-after=30s 8m make test-deterministic
+      - name: Lint
+        if: matrix.python-version == '3.13'
+        run: timeout --signal=TERM --kill-after=30s 2m make lint
+      - name: Validate and build the example
+        if: matrix.python-version == '3.13'
+        run: timeout --signal=TERM --kill-after=30s 4m make check-example
+
+  daemon:
+    name: daemon (Python ${{ matrix.python-version }})
+    runs-on: ubuntu-latest
+    timeout-minutes: 12
+    strategy:
+      fail-fast: false
+      matrix:
+        python-version: ["3.10", "3.13"]
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
+        with:
+          version: "0.12.1"
+          python-version: ${{ matrix.python-version }}
+          enable-cache: true
+      - name: Install locked development environment
+        run: timeout --signal=TERM --kill-after=30s 3m uv sync --frozen --extra dev --extra repl
+      - name: Run detached runtime tests
+        env:
+          AUTOFORM_REPL_TOTAL_WORKERS: "1"
+          AUTOFORM_MAX_LEAN_PROJECTS: "1"
+        run: timeout --signal=TERM --kill-after=30s 8m make test-daemon
+
+  installed-wheel:
+    name: installed wheel (Python ${{ matrix.python-version }})
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     strategy:
+      fail-fast: false
       matrix:
         python-version: ["3.10", "3.13"]
     steps:
@@ -20,7 +77,60 @@ jobs:
           version: "0.12.1"
           python-version: ${{ matrix.python-version }}
           enable-cache: true
-      - run: uv sync --extra dev --extra repl
-      - run: uv run ruff check autoform_cli servers tests
-      - run: uv run pytest -q
-      - run: make check-example
+      - name: Install locked development environment
+        run: timeout --signal=TERM --kill-after=30s 3m uv sync --frozen --extra dev --extra repl
+      - name: Build, install, and probe the wheel
+        run: timeout --signal=TERM --kill-after=30s 10m make test-wheel
+
+  real-lean:
+    name: real Lean (pinned v4.32.2)
+    runs-on: ubuntu-latest
+    timeout-minutes: 45
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
+        with:
+          version: "0.12.1"
+          python-version: "3.13"
+          enable-cache: true
+      - name: Install locked development environment
+        run: timeout --signal=TERM --kill-after=30s 3m uv sync --frozen --extra dev --extra repl
+      - name: Verify the repository Lean and Mathlib pins
+        run: |
+          set -euo pipefail
+          test "$(tr -d '\r\n' < skills/setup/assets/cabannes-thesis-project/lean-toolchain)" = "leanprover/lean4:v4.32.2"
+          grep -Fq 'rev = "v4.32.2"' skills/setup/assets/cabannes-thesis-project/lakefile.toml
+          uv run python - <<'PY'
+          import json
+          from pathlib import Path
+
+          catalog = json.loads(Path("autoform_cli/project/releases.json").read_text(encoding="utf-8"))
+          pinned = [
+              release
+              for release in catalog["releases"]
+              if release["lean"]["toolchain"] == "leanprover/lean4:v4.32.2"
+              and release["mathlib"]["revision"] == "v4.32.2"
+          ]
+          assert len(pinned) == 1
+          PY
+      - name: Install pinned Elan
+        run: |
+          set -euo pipefail
+          timeout --signal=TERM --kill-after=15s 2m curl -sSfL \
+            https://github.com/leanprover/elan/releases/download/v4.2.3/elan-x86_64-unknown-linux-gnu.tar.gz \
+            -o elan.tar.gz
+          echo "df0b2b3a439961ffcbb3985214365ffe40f49bc871df04dff268c7d8e21ca8b2  elan.tar.gz" \
+            | sha256sum --check --strict
+          tar xzf elan.tar.gz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - name: Install and verify pinned Lean
+        run: |
+          set -euo pipefail
+          timeout --signal=TERM --kill-after=30s 10m elan toolchain install leanprover/lean4:v4.32.2
+          version="$(timeout --signal=TERM --kill-after=10s 30s elan run leanprover/lean4:v4.32.2 lean --version)"
+          printf '%s\n' "$version"
+          grep -Fq "Lean (version 4.32.2" <<<"$version"
+          command -v lake
+      - name: Run mandatory real-Lean tests
+        run: timeout --signal=TERM --kill-after=30s 25m make test-real-lean

.muse-plugin/plugin.json

@@ -3,7 +3,7 @@
   "name": "autoform",
   "displayName": "AutoForm Bot",
   "version": "0.5.0",
-  "description": "Set up Lean repositories, build Markdown roadmaps, and support human or agent review.",
+  "description": "Set up Lean repositories, build Markdown roadmaps, orchestrate ready work, and support human or agent review.",
   "compat": {
     "source": "native",
     "manifestDir": ".muse-plugin"
@@ -21,6 +21,11 @@
         "path": "skills/roadmap/SKILL.md",
         "enabledDefault": true
       },
+      {
+        "id": "orchestrate",
+        "path": "skills/orchestrate/SKILL.md",
+        "enabledDefault": true
+      },
       {
         "id": "human-review",
         "path": "skills/human-review/SKILL.md",

Makefile

@@ -1,12 +1,25 @@
-.PHONY: setup test lint check-example
+.PHONY: setup test test-deterministic test-daemon test-wheel test-real-lean lint check-example
 
 THESIS_EXAMPLE := skills/setup/assets/cabannes-thesis-project
+PYTEST := uv run pytest -q
 
 setup:
 	uv sync --extra dev --extra repl
 
 test:
-	uv run pytest -q
+	$(PYTEST)
+
+test-deterministic:
+	$(PYTEST) -m "not daemon and not installed_wheel and not real_lean"
+
+test-daemon:
+	$(PYTEST) -m daemon
+
+test-wheel:
+	$(PYTEST) -m installed_wheel
+
+test-real-lean:
+	$(PYTEST) -m real_lean
 
 lint:
 	uv run ruff check autoform_cli servers tests