diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 94ce924..d5ffbaf 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -20,8 +20,8 @@ jobs: - uses: actions/setup-python@v6 with: python-version: ${{ matrix.python }} - - run: python -X utf8 -m unittest discover -s template/tests - - run: python -X utf8 -m unittest discover -s tests + - run: python -X utf8 -m unittest discover -s tests/template + - run: python -X utf8 -m unittest discover -s tests/kit harness-contract: runs-on: ubuntu-latest @@ -35,4 +35,4 @@ jobs: node-version: '24' - run: python template/scripts/harness.py prepare - run: npm install --prefix "$RUNNER_TEMP/research-dsh" "$(python template/scripts/harness.py package)" - - run: node template/tests/harness_runtime.mjs "$RUNNER_TEMP/research-dsh/node_modules" + - run: node tests/template/harness_runtime.mjs "$RUNNER_TEMP/research-dsh/node_modules" diff --git a/.gitignore b/.gitignore index c18dd8d..fadfa13 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,3 @@ __pycache__/ +.pytest_cache/ +*.pyc diff --git a/README.md b/README.md index 22f3653..5d4aa29 100644 --- a/README.md +++ b/README.md @@ -1,17 +1,17 @@ -# Шаблон исследовательского проекта: математика, источники, Lean +# Шаблон проекта: математика, источники, Lean -Заготовка проекта, который ведут агенты DeepSeek Harness или Claude Code: постановка, источники, идеи с -независимой критикой, доказательства с рецензией, формализация в Lean 4 с проверкой -соответствия, статья. От темы шаблон не зависит: всё тематическое лежит в двух файлах -нового проекта, `question.md` и `PROJECT.md`. +Набор для исследовательского проекта, который ведут агенты Claude Code или DeepSeek +Harness: постановка, источники, идеи с независимой критикой, доказательства с рецензией, +формализация в Lean 4 с проверкой соответствия, статья. От темы шаблон не зависит: всё +тематическое живёт в двух файлах нового проекта, `question.md` и `PROJECT.md`. -Порядок работы и возможности проекта для нового пользователя описаны в -[GUIDE.md](GUIDE.md). +Порядок работы и возможности для нового пользователя — в [docs/guide.md](docs/guide.md). +Как устроен сам набор — в [docs/architecture.md](docs/architecture.md). ## Новый проект ``` -python create.py ..\Spectra --lib Spectra --title "Название темы" +python tools/create.py ..\Spectra --lib Spectra --title "Название темы" cd ..\Spectra lake exe cache get lake build @@ -21,29 +21,29 @@ python scripts/harness.py run web ``` `--lib` — имя библиотеки Lean и пространства имён. Версии Lean и Mathlib берутся из -шаблона; ключ `--pins-from ПРОЕКТ` берёт их из работающего проекта. Дальнейшие шаги -описаны в `README.md` созданного проекта. +шаблона; ключ `--pins-from ПРОЕКТ` берёт их из работающего проекта. Дальнейшие шаги — +в `README.md` созданного проекта. Для DeepSeek Harness нужны Node.js 22.19+ (ветка 22) или 24+ и npm. Команда запуска -подготовит нативные skills, роли и MCP, затем откроет Harness закреплённой версии. -Модель и ключ настраиваются в Harness. Подробности, headless-запуск и проверки — -[DEEPSEEK.md](template/DEEPSEEK.md). Поддержка Claude Code сохраняется. +подготовит нативные skills, роли и MCP, затем откроет Harness закреплённой версии. Модель +и ключ настраиваются в Harness. Подробности, headless-запуск и проверки — +[template/DEEPSEEK.md](template/DEEPSEEK.md). Поддержка Claude Code сохраняется. ## Обновление инструментов в проекте ``` -python create.py --update ..\Spectra --dry-run -python create.py --update ..\Spectra +python tools/create.py --update ..\Spectra --dry-run +python tools/create.py --update ..\Spectra ``` Обновление переписывает только то, чем владеет шаблон: `AGENTS.md`, `CLAUDE.md`, `scripts/`, `tests/`, `.claude/agents/`, `.claude/commands/`, `.claude/skills/`, -`DEEPSEEK.md`, `sources/README.md`, `experiments/README.md`, CI. Постановка, записи, идеи, источники, -библиотека Lean, статья, `.mcp.json` и `.claude/settings.json` не трогаются. Файлы, -которых в шаблоне больше нет, команда перечисляет, но не удаляет. +`DEEPSEEK.md`, `sources/README.md`, `experiments/README.md`, CI. Постановка, записи, идеи, +источники, библиотека Lean, статья, `.mcp.json` и `.claude/settings.json` не трогаются. +Файлы, которых в шаблоне больше нет, команда перечисляет, но не удаляет. -После обновления пересобираются производные `.dsh/skills/` и Cordis patch для Harness -из актуальных инструкций и локальной `.mcp.json`. `--dry-run` ничего не пишет. +После обновления пересобираются производные `.dsh/skills/` и Cordis patch для Harness из +актуальных инструкций и локальной `.mcp.json`. `--dry-run` ничего не пишет. ## Изменение воркфлоу @@ -51,19 +51,33 @@ python create.py --update ..\Spectra `template/.mcp.json`. Поддержка DeepSeek Harness строится из этих файлов: `template/scripts/harness.py` не содержит имён команд и ролей, тесты берут ожидаемый состав из тех же каталогов, документация ссылается на `python scripts/harness.py list`. -После правки воркфлоу достаточно прогнать тесты: +После правки воркфлоу достаточно прогнать проверки: ``` -python -m unittest discover -s template/tests -python -m unittest discover -s tests +python -m unittest discover -s tests/template +python -m unittest discover -s tests/kit python template/scripts/harness.py --root template list ``` -Таблица соответствия и три случая, когда адаптер всё же правится (поле шапки без правила, -новый встроенный инструмент Claude Code, новая версия Harness), — в разделе «Как -переносится воркфлоу Claude Code» файла [DEEPSEEK.md](template/DEEPSEEK.md). Таблицы -агентов и команд в `template/AGENTS.md`, `template/README.md` и `GUIDE.md` общие для двух -сред и обновляются вместе с воркфлоу. +Таблица соответствия и три случая, когда адаптер всё же правится (поле шапки без +правила, новый встроенный инструмент Claude Code, новая версия Harness), — в разделе «Как +переносится воркфлоу Claude Code» файла [template/DEEPSEEK.md](template/DEEPSEEK.md). +Состав воркфлоу описан в `template/AGENTS.md`; он же попадает в созданный проект, поэтому +его не дублируют ни здесь, ни в руководстве. + +## Устройство набора + +| Слой | Где | Что это | +| --- | --- | --- | +| Продукт | `template/` | проект-заготовка; создание копирует его целиком, подставляя имя библиотеки и название | +| Набор | `tools/` | `create.py` — создание и обновление проекта; `tests/kit/` проверяет его без сети и Lean | +| Проверки продукта | `tests/template/` | инструменты проекта, адаптер Harness, согласованность документации | +| Описание | `docs/`, `README.md` | руководство пользователя, архитектура, эта страница | + +Такое деление — по назначению, а не по типу файла: всё, что копируется в проект, лежит +целиком в `template/`, а всё, что описывает и проверяет копирование, — вне него. Поэтому +`PROJECT.md`, `question.md` и остальные файлы заготовки не встречаются в двух местах. +Полный разбор с обоснованием — в [docs/architecture.md](docs/architecture.md). ## Требования @@ -77,6 +91,7 @@ Python 3.11 или новее, `uv`, `elan` с `lake`, `git`; `pdflatex` — д | --- | --- | | `template/AGENTS.md` | общие правила: карта проекта, статусы, роли агентов, проверки | | `template/scripts/proj.py` | заготовки записей, поля шапок, сводки, проверки, аудит аксиом, отпечатки формулировок, сборка статьи, пакеты Aristotle | +| `template/scripts/records.py` | один разбор записей с шапкой для `proj.py` и `lit.py`: чтение, запись, номера, заготовки | | `template/scripts/lit.py` | источники: zbMATH, arXiv, MathNet, DOI; транскрипции; гибридный поиск по полным текстам | | `template/scripts/*_mcp.py` | те же действия как инструменты MCP-серверов `proj` и `lit` | | `template/scripts/harness.py` | DeepSeek Harness: skills, роли и MCP из `.claude/` и `.mcp.json`, Cordis patch, запуск Web/Headless | @@ -84,27 +99,5 @@ Python 3.11 или новее, `uv`, `elan` с `lake`, `git`; `pdflatex` — д | `template/.claude/agents/` | генератор идей, критик, экспериментатор, рецензент, формализатор, проверяющий соответствие, поиск по Mathlib, поиск литературы, транскрипция PDF, сверка карточек | | `template/.claude/commands/` | `/day`, `/ideas`, `/referee`, `/formalize`, `/fidelity`, `/sources`, `/transcribe` | | `template/.claude/skills/` | оформление текста: `paper-canvas`, `shkalikov-style`, `paper-de-ai`, `exposition`; набор и типографика LaTeX: `math-rigor` | -| `template/tests/` | тесты инструментов без сети и без Lean; `harness_runtime.mjs` сверяет patch со схемами Harness | -| `tests/` | тесты создания и обновления проекта | - -## Устройство - -- Статус утверждения стоит в шапке его записи `results/R*.md`. `blueprint.md` и индекс - идей собирает `proj.py sync`. -- `proj.py check` находит объявления записей в библиотеке, запускает Lean, разбирает - аксиомы и ищет в исходниках `sorry`, `axiom`, `native_decide` и отключённые линтеры. -- Соответствие формулировки Lean утверждению записи проверяет отдельный агент. Отпечаток - формулировки и её определений показывает, что проверка устарела. -- Идею проверяет критик, доказательство — рецензент, карточку источника — сверяющий по - PDF. Каждому передают только написанный текст. -- На запись и на идею — по файлу. -- Тема лежит в `PROJECT.md`, `question.md` и `project.toml`; инструменты обновляются из - шаблона. -- Скрипты написаны на Python и печатают в UTF-8. У каждого действия есть инструмент MCP, - которому строки передаются без оболочки. -- Опыт — папка `experiments/E*/` с кодом и одной командой запуска; она входит в Git. -- В `output/` лежит только восстановимое. -- У транскрипции есть печатные номера страниц и утверждений. Карточку теоремы сверяют с - PDF вместе с условиями раздела, стоящими вне текста теоремы. -- Обозначения не пересекаются: `R` — запись, `I` — идея, `S` — источник, `E` — опыт, - `Q` — открытый вопрос. +| `tests/template/` | тесты инструментов без сети и без Lean; `harness_runtime.mjs` сверяет patch со схемами Harness | +| `tests/kit/` | тесты создания и обновления проекта | diff --git a/docs/architecture.md b/docs/architecture.md new file mode 100644 index 0000000..0e34151 --- /dev/null +++ b/docs/architecture.md @@ -0,0 +1,100 @@ +# Устройство набора + +Разбор того, по какому признаку разложены файлы, что было рассогласовано и что осталось +на будущее. Относится к репозиторию-шаблону; созданный проект устроен по своему описанию +в `AGENTS.md`. + +## Признак деления + +Один признак на весь репозиторий: **что этот файл делает по отношению к проекту**. + +| Слой | Отношение к проекту | Где | +| --- | --- | --- | +| Продукт | копируется в проект целиком | `template/` | +| Набор | создаёт и обновляет проект | `tools/create.py` | +| Проверки набора | проверяют создание и обновление | `tests/kit/` | +| Проверки продукта | проверяют инструменты заготовки | `tests/template/` | +| Описание | рассказывает о наборе | `README.md`, `docs/` | + +Смешивать признаки в одном ряду нельзя: деление по назначению (`tools/` против +`template/`) и деление по типу файла (`*.py` против `*.md`) несовместимы, потому что во +втором ряду члены не подчинены одному основанию. Раньше корень репозитория смешивал +именно это: `create.py` и `tests/` относились к набору, `template/` — к продукту, а +`README.md` и `GUIDE.md` — к описанию, и всё лежало в одном ряду. + +Внутри слоя деление однородно. В `template/` лежит ровно то, что получает проект, и +ничего, что получает только репозиторий: `AGENTS.md`, `question.md`, `PROJECT.md`, +`scripts/`, `.claude/`, `tests/`, `paper/`, `sources/`, `experiments/`, `results/`, +`ideas/`, `output/`. Поэтому `PROJECT.md` и `question.md` не встречаются в двух местах и +не требуют решения «какая копия главная». + +## Правила, по которым проверялось деление + +1. Одно основание на одном уровне: `tools/` — по роли в жизненном цикле проекта, а не по + языку или расширению. +2. Члены не пересекаются. Файл принадлежит одному слою; `tests/template/` не копируется в + проект и потому не может одновременно быть тестом продукта. +3. Сумма членов исчерпывает род. Любой новый файл попадает ровно в один слой: он либо + копируется в проект, либо описывает или проверяет это копирование. +4. Ряд последователен: у слоя один и тот же смысл на всех уровнях. `output/` везде + означает «восстановимое, вне Git», и потому производные `.dsh/skills/` тоже живут под + `output/`-правилом: они не коммитятся. +5. Имя вещи одно. Один вид документа — «запись с шапкой» — разбирается одним модулем + `scripts/records.py`, а не двумя копиями кода. + +## Что было рассогласовано + +**Корень без единого основания.** `create.py`, `tests/`, `template/`, `README.md`, +`GUIDE.md` стояли рядом, хотя относятся к разным родам. `create.py` перенесён в `tools/`, +руководство — в `docs/`, тесты разделены по объекту проверки. + +**Два разбора одного формата.** `proj.py` и `lit.py` независимо читали и писали шапку +записи: `Doc`, `read_doc`, `write_doc`, список полей-списков и три заготовки были +продублированы. Копии могли разойтись при правке формата. Общая часть вынесена в +`scripts/records.py`; `proj.py` и `lit.py` вызывают её. + +**Обратная зависимость.** `proj.py sync` запускал `scripts/lit.py catalog` подпроцессом по +жёсткому пути, то есть инструмент записей знал о внутреннем устройстве инструмента +источников, а смена рабочей папки ломала вызов. Теперь путь строится от расположения +самого модуля, а корень передаётся явно ключом `--root`. + +**Пути, вычисленные при импорте.** `lit.py` считал `ROOT`, `REGISTRY`, `CATALOG`, `CARDS`, +`LIT`, `DB` и `DIRECT_HOSTS` в момент загрузки модуля, поэтому его нельзя было направить +на другой каталог — в отличие от `proj.py`, у которого есть `configure`. Такой же +`configure` появился у `lit.py`; тесты пользуются им. + +**Производное в коммите.** `.dsh/skills/` — результат работы адаптера Harness, а не +исходный текст. В репозитории он лежал в Git, вопреки собственному правилу «производные +файлы не коммитьте», и мог устареть относительно `.claude/`. Каталог убран из +отслеживания и собирается командой `harness.py prepare`. + +**Дубли в документации.** Состав команд и ролей был перечислен в `AGENTS.md`, +`template/README.md`, `GUIDE.md` и корневом `README.md`. Теперь состав описан в +`AGENTS.md`, руководство объясняет порядок работы, а корневой `README.md` — только набор. +Тест `tests/template/test_docs.py` сверяет упомянутые в документации команды, навыки и +пути с фактическим составом и падает при расхождении. + +## Что осталось без изменений и почему + +- Имена записей (`R`, `I`, `S`, `E`, `Q`) и папки `results/`, `ideas/`, `sources/cards/` + не менялись: это словарь проекта, он описан в `AGENTS.md` и в руководстве, и его смена + задела бы существующие проекты без выигрыша в ясности. +- `.claude/commands/` и `.claude/skills/` остаются разными папками: команда Claude Code — + это слэш-команда, навык подключается по описанию. Оба вида сходятся в одно пространство + имён Harness, но исходники у них разные. +- `template/` не переименован в `src/` или `skeleton/`: его содержимое — не заготовки, а + настоящий проект. +- `output/` собирает и сборки, и полные тексты источников. Полные тексты восстановимы + командой `lit.py fetch`, поэтому правило «в `output/` только восстановимое» выполняется. + +## Открытые места + +- `sources/catalog.md` собирает `lit.py`, а `blueprint.md` и `ideas/README.md` — `proj.py`. + Обе сводки выводятся из шапок, но собраны разными инструментами; общий сборщик сводок + напрашивается, пока же вызов `proj.py sync` покрывает оба случая. +- `proj.py check` проверяет документацию только косвенно, через тесты. Если состав + воркфлоу начнут описывать в самом `AGENTS.md` таблицей, собираемой `sync`, проверка + свежести перейдёт в `check`. +- Роли и навыки отображаются в Harness из `.claude/`; поля шапки, для которых нет правила, + печатает `harness.py prepare`. Список правил (`SKILL_HANDLED`, `AGENT_HANDLED`) стоит + держать рядом с разбором шапки, когда полей станет больше. diff --git a/GUIDE.md b/docs/guide.md similarity index 97% rename from GUIDE.md rename to docs/guide.md index f082d5e..bcad88d 100644 --- a/GUIDE.md +++ b/docs/guide.md @@ -29,7 +29,7 @@ Из папки шаблона: ``` -python create.py ..\Spectra --lib Spectra --title "Название темы" +python tools/create.py ..\Spectra --lib Spectra --title "Название темы" cd ..\Spectra lake exe cache get lake build @@ -48,7 +48,7 @@ python scripts/proj.py check Для DeepSeek Harness запустите `python scripts/harness.py run web`, выберите папку проекта и preset Standard, настройте модель и ключ в интерфейсе Harness. Создание проекта уже подготовило skills, роли и MCP; запуск обновит их при необходимости. -Полная инструкция — [DEEPSEEK.md](template/DEEPSEEK.md), она также лежит в созданном проекте. +Полная инструкция — [DEEPSEEK.md](../template/DEEPSEEK.md), она также лежит в созданном проекте. ## Шаг 2. Записать постановку @@ -266,8 +266,8 @@ Lean, агенты и номера записей в тексте статьи Когда шаблон изменился, из папки шаблона: ``` -python create.py --update ..\Spectra --dry-run -python create.py --update ..\Spectra +python tools/create.py --update ..\Spectra --dry-run +python tools/create.py --update ..\Spectra ``` Первая команда показывает, что изменится, вторая переписывает правила, скрипты, агентов, @@ -275,7 +275,7 @@ python create.py --update ..\Spectra как были. Для DeepSeek Harness отдельного обновления нет: его skills и роли собираются из тех же -агентов, команд и скиллов. `create.py --update` пересобирает их сам, а после своей правки +агентов, команд и скиллов. `tools/create.py --update` пересобирает их сам, а после своей правки в `.claude/` или `.mcp.json` это делает `python scripts/harness.py prepare` или следующий `run`. Что получит Harness, показывает `python scripts/harness.py list`. diff --git a/template/AGENTS.md b/template/AGENTS.md index ae4b89f..cd0f756 100644 --- a/template/AGENTS.md +++ b/template/AGENTS.md @@ -1,8 +1,8 @@ # Правила работы Файл общий для проектов, созданных из шаблона, и обновляется из шаблона командой -`create.py --update`. Всё, что относится к теме, записано в `PROJECT.md` и `question.md`; -сюда тему не вносите. +`python tools/create.py --update` (запускается из папки шаблона). Всё, что относится к +теме, записано в `PROJECT.md` и `question.md`; сюда тему не вносите. В начале каждой задачи прочитай `PROJECT.md`; постановку бери из `question.md`. Это относится и к дочерним агентам: импорт `@PROJECT.md` поддерживается не во всех средах. @@ -122,6 +122,10 @@ ## Агенты +Таблица ниже — список ролей проекта: их состав, место записи и порядок вызова. В +`README.md` он не повторяется; что получил Harness, показывает +`python scripts/harness.py list`. + | Агент | Задача | Куда пишет | | --- | --- | --- | | `idea-generator` | новые подходы к открытому вопросу или цели | новые файлы `ideas/I*.md` | diff --git a/template/DEEPSEEK.md b/template/DEEPSEEK.md index 6f7213b..b2abd26 100644 --- a/template/DEEPSEEK.md +++ b/template/DEEPSEEK.md @@ -68,8 +68,8 @@ MCP-серверы в корне проекта; вызов MCP может за ## Как переносится воркфлоу Claude Code Новая команда, роль, навык или MCP-сервер попадают в Harness после `prepare` (его -вызывают `run` и `create.py --update`). В `scripts/harness.py`, тестах и этом файле их -имён нет, править там нечего. +вызывают `run` и `tools/create.py --update` из папки шаблона). В `scripts/harness.py`, +тестах и этом файле их имён нет, править там нечего. | В Claude Code | В Harness | | --- | --- | @@ -105,12 +105,12 @@ MCP-серверы в корне проекта; вызов MCP может за При удалении исходной команды её неизменённые производные файлы убираются по манифесту; чужие файлы не удаляются, ручные изменения устаревших производных требуют переноса. -`create.py` подготавливает интеграцию при создании и обновлении проекта. Для старого -проекта выполните из папки шаблона: +`tools/create.py` из репозитория шаблона подготавливает интеграцию при создании и +обновлении проекта. Для старого проекта выполните из папки шаблона: ```sh -python create.py --update ../Spectra --dry-run -python create.py --update ../Spectra +python tools/create.py --update ../Spectra --dry-run +python tools/create.py --update ../Spectra ``` Собственные настройки `.mcp.json`, `.claude/settings.json` и файлы исследования @@ -122,9 +122,9 @@ python create.py --update ../Spectra сгенерированного: `python scripts/harness.py run web -- --patch /path/to/local.yml`. Адаптер не переносит разрешения Claude и не меняет глобальные настройки Harness. Права задаются в Harness; ограничения мест записи в ролях являются инструкциями. -MCP с `env`/`headers` настраиваются отдельным Cordis patch, чтобы не размножать секреты. -Для такого сервера отметьте запись в `.mcp.json` как `disabled: true` и включите её -локальным patch. Поддерживаются stdio и HTTP; SSE не конвертируется. +Поле `env` stdio-сервера копируется в patch, который лежит в `output/` вне Git; ключи в +`.mcp.json` не храните. HTTP-сервер с `headers` настраивается отдельным Cordis patch: +отметьте запись в `.mcp.json` как `disabled: true` и включите её локальным patch. Поддерживаются stdio и HTTP; SSE не конвертируется. ## Проверка @@ -135,6 +135,10 @@ python -m unittest discover tests python scripts/proj.py check --fast ``` +Тот же набор команд выполняет CI проекта (`.github/workflows/ci.yml`); проверка +`harness.py check` там идёт после `prepare`, а `harness_runtime.mjs` сверяет patch со +схемами закреплённой версии Harness. + `harness.py check` проверяет свежесть файлов, не запускает модель и ничего не пишет. Структуру итоговой конфигурации можно проверить самим Harness без запроса к модели: @@ -146,8 +150,8 @@ python scripts/harness.py run web -- --dump-config ```sh npm install --prefix output/harness/runtime @deepseek-ai/dsh@0.2.1-alpha.2 -node tests/harness_runtime.mjs output/harness/runtime/node_modules -node tests/harness_runtime.mjs output/harness/runtime/node_modules --mcp +node tests/template/harness_runtime.mjs output/harness/runtime/node_modules +node tests/template/harness_runtime.mjs output/harness/runtime/node_modules --mcp ``` Последняя команда проверяет handshake и список инструментов каждого MCP-сервера, diff --git a/template/README.md b/template/README.md index af6843c..e1a039d 100644 --- a/template/README.md +++ b/template/README.md @@ -40,24 +40,17 @@ preset Standard и модель в интерфейсе. Адаптер подк | `__LIB__/`, `__LIB__.lean` | библиотека Lean | | `paper/` | статья | | [blueprint.md](blueprint.md) | сводка записей и граф зависимостей; собирается из шапок | -| `scripts/` | `proj.py` — записи, проверки, сводки; `lit.py` — источники; MCP-серверы | +| `scripts/` | `proj.py` — записи, проверки, сводки; `lit.py` — источники; `records.py` — общий разбор записей; MCP-серверы | | `.claude/` | агенты, команды, скиллы оформления текста | -| `.dsh/skills/` | производные skills для Harness; собираются автоматически | +| `.dsh/skills/` | производные skills для Harness; собираются автоматически, в Git не входят | | [DEEPSEEK.md](DEEPSEEK.md) | запуск, модели, MCP, диагностика и обновление Harness | | `output/` | сборки, полные тексты, индекс; в Git не входит | -## Команды +## Работа -| Команда | Что делает | -| --- | --- | -| `/day` | ежедневный цикл | -| `/ideas [цель]` | идеи и их критика | -| `/referee R07` | рецензия доказательства | -| `/formalize R07` | формализация и проверка соответствия | -| `/fidelity` | проверка соответствия формулировок Lean | -| `/sources [тема]` | поиск и загрузка источников | -| `/transcribe S12` | PDF источника в LaTeX | -| `/exposition` | обновление статьи | +Команды и роли — в `AGENTS.md`: там их состав, куда каждая роль пишет и что запускает. +В Harness те же команды приходят нативными skills, их список печатает +`python scripts/harness.py list`. ## Проверки diff --git a/template/scripts/harness.py b/template/scripts/harness.py index 4655a2e..aea7c67 100644 --- a/template/scripts/harness.py +++ b/template/scripts/harness.py @@ -39,7 +39,8 @@ DELEGATING = {'Agent', 'Task'} PROJECT_NOTE = 'Рабочая папка — корень этого исследовательского проекта.' -READ_NOTE = 'Перед работой прочитай AGENTS.md и PROJECT.md из корня проекта.' +# Файлы правил проекта; в указание «прочитай» попадают те, что есть в проекте. +RULES = ('AGENTS.md', 'PROJECT.md') DELEGATION = """Роли вызываются инструментами research_*; каждый вызов создаёт нового агента без истории родителя. Передавай проверяющему только файлы и предмет проверки, без рассуждений автора. Вызов возвращает id; дождись отчёта и проверь записанный файл @@ -116,6 +117,11 @@ def tool_list(fields: dict) -> list[str] | None: return [item.strip() for item in str(fields['tools']).split(',') if item.strip()] +def read_note(root: Path) -> str: + found = [name for name in RULES if (root / name).is_file()] + return f'Перед работой прочитай {" и ".join(found)} из корня проекта.' + + def mcp_note(servers: list[str]) -> list[str]: return ['MCP: ' + ', '.join(f'mcp__{name}__*' for name in servers) + '.'] if servers else [] @@ -169,7 +175,7 @@ def unported(root: Path) -> list[str]: return notes -def skill_files(agents: dict, skills: dict, servers: list[str]) -> dict[Path, bytes]: +def skill_files(root: Path, agents: dict, skills: dict, servers: list[str]) -> dict[Path, bytes]: # Self-ignoring directory also works in projects upgraded from older templates. result: dict[Path, bytes] = {Path('.dsh/skills/.gitignore'): b'*\n'} by_paths: dict[str, list[str]] = {} @@ -185,7 +191,7 @@ def skill_files(agents: dict, skills: dict, servers: list[str]) -> dict[Path, by header['whenToUse'] = f'При работе с файлами {fields["paths"]}.' lines = host_notes(body) if is_workflow(source, fields): - lines = [PROJECT_NOTE + ' ' + READ_NOTE, *roster(agents), *mcp_note(servers), *scoped, *lines, COMMON] + lines = [PROJECT_NOTE + ' ' + read_note(root), *roster(agents), *mcp_note(servers), *scoped, *lines, COMMON] prefix = '\n'.join(lines) + '\n\n' if lines else '' yaml = '\n'.join(f'{k}: {json.dumps(v, ensure_ascii=False)}' for k, v in header.items()) result[Path('.dsh/skills') / name / 'SKILL.md'] = ( @@ -198,11 +204,11 @@ def skill_files(agents: dict, skills: dict, servers: list[str]) -> dict[Path, by return result -def persona(name: str, agents: dict, servers: list[str]) -> str: +def persona(root: Path, name: str, agents: dict, servers: list[str]) -> str: """Role instructions; the restrictions come from the Claude Code frontmatter of the role.""" _, fields, body = agents[name] tools = tool_list(fields) - lines = [PROJECT_NOTE if fields.get('omitClaudeMd') is True else PROJECT_NOTE + ' ' + READ_NOTE] + lines = [PROJECT_NOTE if fields.get('omitClaudeMd') is True else PROJECT_NOTE + ' ' + read_note(root)] if tools is None or DELEGATING & set(tools): lines += roster(agents, skip=name) else: @@ -235,9 +241,9 @@ def mcp_entries(root: Path) -> list[dict]: config.update(transport='stdio', command=original['command'], args=original.get('args', [])) cwd = Path(original.get('cwd', str(root))) config['cwd'] = str((root / cwd).resolve()) + # The patch stays in the ignored output/; headers below are still refused. if original.get('env'): - raise ValueError(f'MCP {name}: env храните в отдельном локальном Cordis patch; ' - 'адаптер не копирует секреты из .mcp.json') + config['env'] = original['env'] elif transport in ('http', 'streamable-http'): config.update(transport='streamable-http', url=original['url']) if original.get('headers'): @@ -250,19 +256,18 @@ def mcp_entries(root: Path) -> list[dict]: def artifacts(root: Path) -> dict[Path, bytes]: root = root.resolve() - for required in ('AGENTS.md', 'PROJECT.md', 'project.toml'): - if not (root / required).is_file(): - raise ValueError(f'Нет {root / required}; укажите корень созданного проекта') + if not (root / RULES[0]).is_file(): + raise ValueError(f'Нет {root / RULES[0]}; укажите корень проекта') agents, skills = sources(root) entries = mcp_entries(root) servers = [entry['config']['serverName'] for entry in entries] - result = skill_files(agents, skills, servers) + result = skill_files(root, agents, skills, servers) for name in agents: entries.append({ 'id': f'research-role-{name}', 'name': '@deepseek-ai/dsh-tool-subagent', 'config': {'provider': 'spawn', 'toolName': role_tool(name), - 'maxDepth': 2, 'persona': persona(name, agents, servers)}, + 'maxDepth': 2, 'persona': persona(root, name, agents, servers)}, }) # A private provider makes skills discoverable even with --no-git or when the # project is nested inside another checkout. Avoid duplicate default-root scans. diff --git a/template/scripts/lit.py b/template/scripts/lit.py index 76d0f9b..9e29cc0 100644 --- a/template/scripts/lit.py +++ b/template/scripts/lit.py @@ -37,13 +37,8 @@ from datetime import date from pathlib import Path -ROOT = Path(__file__).resolve().parent.parent -REGISTRY = ROOT / 'sources' / 'papers.json' -CATALOG = ROOT / 'sources' / 'catalog.md' -CARDS = ROOT / 'sources' / 'cards' -RESULTS = ROOT / 'sources' / 'results.md' # вариант раскладки: все карточки в одном файле -LIT = ROOT / 'output' / 'literature' -DB = LIT / 'index' / 'lit.sqlite' +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import records # noqa: E402 MODEL = 'intfloat/multilingual-e5-small' CHUNKER = 3 # увеличить после изменения нарезки: индекс пересоберётся @@ -52,15 +47,37 @@ ATOM = {'a': 'http://www.w3.org/2005/Atom', 'x': 'http://arxiv.org/schemas/atom'} DELAYS = {'arxiv.org': 3.0, 'mathnet.ru': 2.0, 'semanticscholar.org': 1.0} # секунд между запросами - -def settings() -> dict: - path = ROOT / 'project.toml' - return tomllib.loads(path.read_text(encoding='utf-8')).get('sources', {}) if path.exists() else {} - - -# Хосты, до которых трафик через VPN-туннель не доходит: к ним идём с адреса другого интерфейса -DIRECT_HOSTS = [host.strip() for host in os.environ.get('LIT_DIRECT_HOSTS', '').split(',') if host.strip()] \ - or settings().get('direct_hosts', ['mathnet.ru']) +# Пути проекта; до configure() действует корень этого файла, тесты подставляют временный. +ROOT: Path +REGISTRY: Path +CATALOG: Path +CARDS: Path +RESULTS: Path # вариант раскладки: все карточки в одном файле +LIT: Path +DB: Path +# Хосты, до которых трафик через VPN-туннель не доходит: к ним идём с адреса другого +# интерфейса. Список берётся из project.toml или переменной LIT_DIRECT_HOSTS. +DIRECT_HOSTS: list[str] = [] + + +def configure(root: Path, direct_hosts: list[str] | None = None) -> None: + """Привязывает пути к корню проекта; тесты вызывают с временным каталогом.""" + global ROOT, REGISTRY, CATALOG, CARDS, RESULTS, LIT, DB, DIRECT_HOSTS + ROOT = Path(root) + REGISTRY = ROOT / 'sources' / 'papers.json' + CATALOG = ROOT / 'sources' / 'catalog.md' + CARDS = ROOT / 'sources' / 'cards' + RESULTS = ROOT / 'sources' / 'results.md' + LIT = ROOT / 'output' / 'literature' + DB = LIT / 'index' / 'lit.sqlite' + configured = tomllib.loads((ROOT / 'project.toml').read_text(encoding='utf-8')) if \ + (ROOT / 'project.toml').exists() else {} + from_env = [host.strip() for host in os.environ.get('LIT_DIRECT_HOSTS', '').split(',') if host.strip()] + DIRECT_HOSTS = direct_hosts if direct_hosts is not None else \ + from_env or configured.get('sources', {}).get('direct_hosts', ['mathnet.ru']) + + +configure(Path(__file__).resolve().parent.parent) # ---------- сеть ---------- @@ -682,7 +699,9 @@ def pages(code: str, first: int = 1, last: int | None = None, dpi: int = 170) -> def cards() -> set[str]: """Коды источников, у которых есть карточка проверенных теорем.""" - found = {path.stem.upper() for path in CARDS.glob('S*.md')} if CARDS.exists() else set() + found: set[str] = set() + if CARDS.exists(): + found = {doc.id for doc in (records.read_doc(path) for path in CARDS.glob('S*.md')) if doc.id} if RESULTS.exists(): headings = ' '.join(re.findall(r'^## (.*)$', RESULTS.read_text(encoding='utf-8'), re.M)) found |= set(re.findall(r'S\d+', headings)) @@ -1212,6 +1231,8 @@ def main() -> None: sys.stdout.reconfigure(encoding='utf-8', errors='replace') sys.stderr.reconfigure(encoding='utf-8', errors='replace') parser = argparse.ArgumentParser(description=__doc__.split('\n')[0]) + parser.add_argument('--root', type=Path, default=ROOT, + help='корень проекта, по умолчанию каталог над scripts/') commands = parser.add_subparsers(dest='command', required=True) p = commands.add_parser('add', help='добавить источники: arXiv, mathnet:rm9740, DOI') @@ -1262,6 +1283,7 @@ def main() -> None: commands.add_parser('list', help='источники реестра и число кусков в индексе') args = parser.parse_args() + configure(args.root) log = lambda line: print(line, file=sys.stderr, flush=True) codes = [code.upper() for code in getattr(args, 'codes', None) or []] or None if args.command == 'add': diff --git a/template/scripts/proj.py b/template/scripts/proj.py index a4703c2..16df32f 100644 --- a/template/scripts/proj.py +++ b/template/scripts/proj.py @@ -14,18 +14,19 @@ import sys import tarfile import tomllib -from dataclasses import dataclass -from datetime import date from pathlib import Path sys.path.insert(0, str(Path(__file__).resolve().parent)) import leandecl # noqa: E402 +import records # noqa: E402 -RESULT_STATUS = ['цель', 'набросок', 'доказано', 'опровергнуто'] -IDEA_STATUS = ['новая', 'выдержала критику', 'в работе', 'отвергнута', 'перенесена'] +RESULT_STATUS = records.RESULT_STATUS +IDEA_STATUS = records.IDEA_STATUS DEFAULT_AXIOMS = ['propext', 'Classical.choice', 'Quot.sound'] -ROOT = Path(__file__).resolve().parent.parent +# Корень проекта подставляется из project.toml; подчёркивание отличает это имя от +# модульной переменной `ROOT`, по которой records строит пути записей. +_ROOT = Path(__file__).resolve().parent.parent LIB = '' AXIOMS: set[str] = set() PAPER = 'paper/main.tex' @@ -33,215 +34,39 @@ def configure(root: Path) -> None: """Читает project.toml; тесты вызывают с временным каталогом.""" - global ROOT, LIB, AXIOMS, PAPER - ROOT = Path(root) - config = tomllib.loads((ROOT / 'project.toml').read_text(encoding='utf-8')) + global _ROOT, LIB, AXIOMS, PAPER + _ROOT = Path(root) + config = tomllib.loads((_ROOT / 'project.toml').read_text(encoding='utf-8')) LIB = config['project']['lib'] AXIOMS = set(config.get('lean', {}).get('allowed_axioms', DEFAULT_AXIOMS)) PAPER = config.get('paper', {}).get('main', PAPER) -# ---------- записи с шапкой ---------- - -@dataclass -class Doc: - path: Path - meta: dict - body: str - - @property - def id(self) -> str: - return re.match(r'[A-Z]+\d+', self.path.stem).group(0) - - def many(self, key: str) -> list[str]: - value = self.meta.get(key) or [] - return value if isinstance(value, list) else [value] - - -def read_doc(path: Path) -> Doc: - text = path.read_text(encoding='utf-8').replace('\r\n', '\n') - if not text.startswith('---\n'): - return Doc(path, {}, text) - head, _, body = text[4:].partition('\n---\n') - meta: dict = {} - for line in head.split('\n'): - key, colon, value = line.partition(':') - if not colon or not key.strip() or key.lstrip().startswith('#'): - continue - value = value.strip() - meta[key.strip()] = [item.strip() for item in value[1:-1].split(',') if item.strip()] \ - if value.startswith('[') and value.endswith(']') else value - return Doc(path, meta, body) - - -def write_doc(doc: Doc) -> None: - lines = [f"{key}: [{', '.join(value)}]" if isinstance(value, list) else f'{key}: {value}'.rstrip() - for key, value in doc.meta.items()] - doc.path.write_text('---\n' + '\n'.join(lines) + '\n---\n' + doc.body, encoding='utf-8', newline='\n') - - -def docs(folder: str, prefix: str) -> list[Doc]: - paths = [path for path in (ROOT / folder).glob(f'{prefix}*.md') if re.fullmatch(rf'{prefix}\d+', path.stem)] - return [read_doc(path) for path in sorted(paths, key=lambda path: int(path.stem[len(prefix):]))] - - -def find_doc(ident: str) -> Doc: - folder = {'R': 'results', 'I': 'ideas', 'S': 'sources/cards'}.get(ident[:1].upper()) - path = ROOT / (folder or '') / f'{ident.upper()}.md' - if not folder or not path.exists(): - raise SystemExit(f'Нет записи {ident}.') - return read_doc(path) +# Общий разбор записей живёт в records.py; здесь только привязка к корню проекта. +Doc = records.Doc def rel(path: Path) -> str: - return path.relative_to(ROOT).as_posix() - - -# ---------- заготовки ---------- - -STUBS = { - 'result': ('results', 'R', '''--- -id: {id} -title: {title} -status: цель -depends: [{depends}] -sources: [] -lean: [] -review: -fidelity: ---- - -## Утверждение - -Точная формулировка: объекты, гипотезы, вывод, область определения. - -## Доказательство - -Пока нет. - -## Границы - -Что утверждение не покрывает; какие гипотезы существенны и почему. -'''), - 'idea': ('ideas', 'I', '''--- -id: {id} -title: {title} -target: {target} -status: новая -created: {today} -critic: ---- + return records.rel(_ROOT, path) -## Формулировка -Гипотезы, вывод, область определения. - -## Набросок - -Шаги по одному. У каждого шага опора: запись R…, карточка источника S…, стандартный факт -с названием или «пробел». - -## Чем убить - -Самая дешёвая проверка, которая опровергла бы идею: частный случай, расчёт, известный пример. - -## Следующий шаг -'''), - 'card': ('sources/cards', 'S', '''--- -source: {id} -verified: ---- - -# {id}. {title} - -## Теорема N, с. P - -**Гипотезы.** Все, включая соглашения раздела и статьи («всюду далее …»). - -**Вывод.** - -**Определения, от которых зависит формулировка.** Как они даны в этой работе. - -**Применимость.** Где используется (R…) и как там проверена каждая гипотеза. -'''), -} - -EXPERIMENT = '''--- -id: {id} -title: {title} -idea: {idea} -status: начат ---- - -## Вопрос - -Что проверяем и какой исход опроверг бы гипотезу. - -## Запуск - -`uv run experiments/{id}/run.py` - -## Проверка метода - -Случай с известным ответом и расхождение с ним. - -## Результат +def find_doc(ident: str) -> Doc: + return records.find_doc(_ROOT, ident) -Таблица чисел с оценкой погрешности. Вывод — «согласуется» или «не согласуется», не «доказано». -''' -RUN_PY = '''# /// script -# requires-python = ">=3.11" -# dependencies = ["numpy", "scipy", "mpmath", "sympy"] -# /// -"""{title}""" -''' +def docs(folder: str, prefix: str) -> list[Doc]: + return records.docs(_ROOT, folder, prefix) def new(kind: str, title: str, **fields) -> Path: - """Создаёт запись со следующим свободным номером; номер занимается созданием файла.""" - if kind == 'experiment': - folder, prefix = ROOT / 'experiments', 'E' - taken = [int(path.name[1:]) for path in folder.glob('E*') if re.fullmatch(r'E\d+', path.name)] - else: - subfolder, prefix, stub = STUBS[kind] - folder = ROOT / subfolder - taken = [int(path.stem[1:]) for path in folder.glob(f'{prefix}*.md') if re.fullmatch(rf'{prefix}\d+', path.stem)] - folder.mkdir(parents=True, exist_ok=True) - if kind == 'card': - path = folder / f"{fields['source']}.md" - with path.open('x', encoding='utf-8', newline='\n') as handle: - handle.write(stub.format(id=fields['source'], title=title)) - return path - number = max(taken, default=0) + 1 - while True: - ident = f'{prefix}{number:02d}' - try: - if kind == 'experiment': - (folder / ident).mkdir() - (folder / ident / 'README.md').write_text( - EXPERIMENT.format(id=ident, title=title, idea=fields.get('idea', '')), encoding='utf-8', newline='\n') - (folder / ident / 'run.py').write_text(RUN_PY.format(title=title), encoding='utf-8', newline='\n') - return folder / ident / 'README.md' - path = folder / f'{ident}.md' - with path.open('x', encoding='utf-8', newline='\n') as handle: - handle.write(stub.format(id=ident, title=title, today=f'{date.today():%Y-%m-%d}', - depends=fields.get('depends', ''), target=fields.get('target', ''))) - return path - except FileExistsError: - number += 1 + return records.create(_ROOT, kind, title, **fields) def set_field(ident: str, key: str, value: str) -> str: - doc = find_doc(ident) vocabulary = {'R': RESULT_STATUS, 'I': IDEA_STATUS}.get(ident[:1].upper()) if key == 'status' and vocabulary and value not in vocabulary: raise SystemExit(f'Статус «{value}» не из списка: {", ".join(vocabulary)}.') - old = doc.meta.get(key) - many = isinstance(old, list) or key in ('depends', 'sources', 'lean') - doc.meta[key] = [item.strip() for item in value.split(',') if item.strip()] if many else value - write_doc(doc) - return f'{doc.id}: {key} = {value}' + return records.save_doc(_ROOT, ident, key, value) # ---------- Lean ---------- @@ -258,12 +83,12 @@ def lake() -> str: def run(command: list[str], timeout: int = 3600) -> tuple[int, str]: # stdin закрыт: под MCP-сервером дочерний процесс иначе наследует его канал и на Windows зависает - done = subprocess.run(command, cwd=ROOT, capture_output=True, timeout=timeout, stdin=subprocess.DEVNULL) + done = subprocess.run(command, cwd=_ROOT, capture_output=True, timeout=timeout, stdin=subprocess.DEVNULL) return done.returncode, (done.stdout + done.stderr).decode('utf-8', 'replace') def lean_files() -> list[Path]: - return sorted((ROOT / LIB).rglob('*.lean')) + [ROOT / f'{LIB}.lean'] + return sorted((_ROOT / LIB).rglob('*.lean')) + [_ROOT / f'{LIB}.lean'] def hygiene() -> tuple[list[str], list[str]]: @@ -292,7 +117,7 @@ def audit(names: list[str]) -> list[str]: """Проверяет в Lean, что объявления существуют и зависят только от разрешённых аксиом.""" if not names: return [] - target = ROOT / 'output' / 'Audit.lean' + target = _ROOT / 'output' / 'Audit.lean' target.parent.mkdir(exist_ok=True) target.write_text(f'import {LIB}\n' + ''.join(f'#print axioms {name}\n' for name in names), encoding='utf-8', newline='\n') @@ -390,9 +215,9 @@ def check_ideas(ideas: list[Doc], records: set[str]) -> tuple[list, list]: def registry() -> tuple[set[str], set[str], set[str]]: """Коды источников реестра; коды с карточкой; коды с карточкой, сверенной по PDF.""" import json - path = ROOT / 'sources' / 'papers.json' + path = _ROOT / 'sources' / 'papers.json' codes = {row['code'] for row in json.loads(path.read_text(encoding='utf-8'))} if path.exists() else set() - cards = [read_doc(card) for card in (ROOT / 'sources' / 'cards').glob('S*.md')] + cards = [records.read_doc(card) for card in (_ROOT / 'sources' / 'cards').glob('S*.md')] return (codes, {card.path.stem for card in cards}, {card.path.stem for card in cards if card.meta.get('verified')}) @@ -401,13 +226,13 @@ def check(fast: bool) -> tuple[int, list[str]]: errors, warnings, passed = [], [], [] for required in ('AGENTS.md', 'PROJECT.md', 'question.md', 'project.toml', 'lakefile.toml', 'lean-toolchain', f'{LIB}.lean', 'sources/papers.json', '.gitignore'): - if not (ROOT / required).exists(): + if not (_ROOT / required).exists(): errors.append(f'нет файла {required}') - lakefile = (ROOT / 'lakefile.toml').read_text(encoding='utf-8') if (ROOT / 'lakefile.toml').exists() else '' + lakefile = (_ROOT / 'lakefile.toml').read_text(encoding='utf-8') if (_ROOT / 'lakefile.toml').exists() else '' if f'name = "{LIB}"' not in lakefile: errors.append(f'lakefile.toml не объявляет библиотеку {LIB} из project.toml') - index = leandecl.library(ROOT, LIB) + index = leandecl.library(_ROOT, LIB) records, ideas = docs('results', 'R'), docs('ideas', 'I') sources, carded, verified = registry() for found_errors, found_warnings in (check_records(records, sources, carded, index, verified), @@ -419,11 +244,11 @@ def check(fast: bool) -> tuple[int, list[str]]: f'объявлений Lean: {len(index)}') for name, text in views(records, ideas, index).items(): - current = (ROOT / name).read_text(encoding='utf-8').replace('\r\n', '\n') if (ROOT / name).exists() else '' + current = (_ROOT / name).read_text(encoding='utf-8').replace('\r\n', '\n') if (_ROOT / name).exists() else '' if current != text: errors.append(f'{name} устарел: python scripts/proj.py sync') - if not (ROOT / '.git').exists(): + if not (_ROOT / '.git').exists(): warnings.append('каталог не под Git: git init') else: code, output = run(['git', 'check-ignore', 'output/probe']) @@ -484,7 +309,7 @@ def views(records: list[Doc], ideas: list[Doc], index: dict) -> dict[str, str]: edges += [f' {dep} --> {doc.id}' for dep in doc.many('depends')] modules = [] for path in lean_files(): - if path.exists() and path.parent != ROOT: + if path.exists() and path.parent != _ROOT: found = re.search(r'/-!\s*#*\s*([^\n]*)', path.read_text(encoding='utf-8')) modules.append(f"| `{rel(path)}` | {cell(found.group(1).strip() if found else '')} |") blueprint = '\n'.join([ @@ -512,14 +337,17 @@ def views(records: list[Doc], ideas: list[Doc], index: dict) -> dict[str, str]: def sync() -> list[str]: - index = leandecl.library(ROOT, LIB) + """Собирает сводки записей и каталог источников; каталог строит lit, а не этот файл.""" + index = leandecl.library(_ROOT, LIB) written = [] for name, text in views(docs('results', 'R'), docs('ideas', 'I'), index).items(): - (ROOT / name).parent.mkdir(parents=True, exist_ok=True) - (ROOT / name).write_text(text, encoding='utf-8', newline='\n') + (_ROOT / name).parent.mkdir(parents=True, exist_ok=True) + (_ROOT / name).write_text(text, encoding='utf-8', newline='\n') written.append(name) - if (ROOT / 'sources' / 'papers.json').exists(): - code, output = run([sys.executable, 'scripts/lit.py', 'catalog']) + if (_ROOT / 'sources' / 'papers.json').exists(): + # sys.executable и путь рядом с этим файлом: то же окружение, что у proj.py. + catalog = Path(__file__).resolve().parent / 'lit.py' + code, output = run([sys.executable, str(catalog), 'catalog', '--root', str(_ROOT)]) written.append('sources/catalog.md' if not code else 'sources/catalog.md не собран: ' + output[-200:]) return written @@ -528,11 +356,11 @@ def sync() -> list[str]: def tex(source: str) -> int: """Два прохода pdflatex в output/ и предупреждения из журнала.""" - path = ROOT / source + path = _ROOT / source if not shutil.which('pdflatex'): print('pdflatex не найден.') return 1 - (ROOT / 'output').mkdir(exist_ok=True) + (_ROOT / 'output').mkdir(exist_ok=True) for attempt in (1, 2): code, output = run(['pdflatex', '-interaction=nonstopmode', '-halt-on-error', '-file-line-error', '-output-directory=output', source]) @@ -540,7 +368,7 @@ def tex(source: str) -> int: print(f'pdflatex не прошёл (проход {attempt}):') print('\n'.join(line for line in output.split('\n') if re.search(r':\d+: |^! ', line))[:1500]) return 1 - log = (ROOT / 'output' / (path.stem + '.log')).read_text(encoding='utf-8', errors='replace') + log = (_ROOT / 'output' / (path.stem + '.log')).read_text(encoding='utf-8', errors='replace') found = [line for line in log.split('\n') if re.search(r'undefined|Overfull|LaTeX Warning|Package .* Warning', line)] for line in found: print('замечание:', line.strip()) @@ -566,9 +394,9 @@ def doctor() -> int: __import__(module) except ImportError: lines.append(f'модуль {module}: нет — нужен scripts/lit.py; `uv run scripts/lit.py …` поставит сам') - toolchain = (ROOT / 'lean-toolchain').read_text(encoding='utf-8').strip() + toolchain = (_ROOT / 'lean-toolchain').read_text(encoding='utf-8').strip() lines.append(f'lean-toolchain: {toolchain}; библиотека: {LIB}') - if not (ROOT / '.lake' / 'packages' / 'mathlib').exists(): + if not (_ROOT / '.lake' / 'packages' / 'mathlib').exists(): lines.append('Mathlib не загружен: lake exe cache get') print('\n'.join(lines)) return 1 if bad else 0 @@ -579,14 +407,14 @@ def doctor() -> int: def aristotle_pack(name: str, skeleton: str) -> list[str]: """Пакет для Aristotle: библиотека, закреплённые версии и заготовка с sorry как новый модуль.""" source = Path(skeleton) - source = source if source.is_absolute() else ROOT / source - package = ROOT / 'output' / 'aristotle' / name + source = source if source.is_absolute() else _ROOT / source + package = _ROOT / 'output' / 'aristotle' / name if package.exists(): raise SystemExit(f'{rel(package)} уже есть: выберите другое имя.') (package / LIB).mkdir(parents=True) for item in ('lakefile.toml', 'lean-toolchain', 'lake-manifest.json', f'{LIB}.lean'): - shutil.copy2(ROOT / item, package / item) - shutil.copytree(ROOT / LIB, package / LIB, dirs_exist_ok=True) + shutil.copy2(_ROOT / item, package / item) + shutil.copytree(_ROOT / LIB, package / LIB, dirs_exist_ok=True) shutil.copy2(source, package / LIB / source.name) shutil.copy2(source, package / 'skeleton.lean') with (package / f'{LIB}.lean').open('a', encoding='utf-8', newline='\n') as root_file: @@ -604,8 +432,8 @@ def aristotle_pack(name: str, skeleton: str) -> list[str]: def aristotle_accept(name: str, result: str) -> int: """Сверяет ответ с заготовкой: формулировки, sorry, axiom, изменённые файлы. Ничего не переносит.""" - package = ROOT / 'output' / 'aristotle' / name - answer = Path(result) if Path(result).is_absolute() else ROOT / result + package = _ROOT / 'output' / 'aristotle' / name + answer = Path(result) if Path(result).is_absolute() else _ROOT / result if answer.is_file(): folder = package.parent / (name + '-result') with tarfile.open(answer) as archive: @@ -649,7 +477,7 @@ def create(kind: str, title: str, depends: str = '', target: str = '', idea: str if kind != 'card': return rel(new(kind, title, depends=depends, target=target, idea=idea)) import json - rows = json.loads((ROOT / 'sources' / 'papers.json').read_text(encoding='utf-8')) + rows = json.loads((_ROOT / 'sources' / 'papers.json').read_text(encoding='utf-8')) row = next((row for row in rows if row['code'] == title.upper()), None) if row is None: raise SystemExit(f'Источника {title} нет в реестре.') @@ -659,7 +487,7 @@ def create(kind: str, title: str, depends: str = '', target: str = '', idea: str def declarations(items: list[str]) -> tuple[dict, list]: """Объявления по полным именам или номерам записей; пустой список — все записи.""" - index = leandecl.library(ROOT, LIB) + index = leandecl.library(_ROOT, LIB) names = [] for item in items or [doc.id for doc in docs('results', 'R')]: names += find_doc(item).many('lean') if re.fullmatch(r'[Rr]\d+', item) else [item] @@ -705,8 +533,9 @@ def overview() -> str: def main() -> int: sys.stdout.reconfigure(encoding='utf-8', errors='replace') - configure(ROOT) parser = argparse.ArgumentParser(description=__doc__.split('\n')[0]) + parser.add_argument('--root', type=Path, default=_ROOT, + help='корень проекта, по умолчанию каталог над scripts/') commands = parser.add_subparsers(dest='command', required=True) p = commands.add_parser('new', help='создать запись со следующим номером') p.add_argument('kind', choices=['result', 'idea', 'card', 'experiment']) @@ -735,6 +564,7 @@ def main() -> int: p.add_argument('name') p.add_argument('file', help='pack: заготовка .lean с sorry; accept: архив или папка ответа') args = parser.parse_args() + configure(args.root) if args.command == 'new': print(create(args.kind, args.title, args.depends, args.target, args.idea)) diff --git a/template/scripts/records.py b/template/scripts/records.py new file mode 100644 index 0000000..3dc3f7a --- /dev/null +++ b/template/scripts/records.py @@ -0,0 +1,232 @@ +"""Записи проекта с шапкой: разбор, запись, заготовки. + +Один вид документа на весь проект: запись результата `results/R*.md`, идея `ideas/I*.md`, +карточка теоремы `sources/cards/S*.md`, опыт `experiments/E*/README.md`. Шапка — плоское +YAML-подмножество `ключ: значение`, списки в квадратных скобках. Здесь же словари статусов +и заготовки новых файлов, поэтому `proj.py` и `lit.py` видят записи одинаково. + +Пути записей выводятся из корня проекта: `proj.py` и `lit.py` передают свой, тесты — +временный каталог. +""" +from __future__ import annotations + +import re +from dataclasses import dataclass +from datetime import date +from pathlib import Path + +RESULT_STATUS = ['цель', 'набросок', 'доказано', 'опровергнуто'] +IDEA_STATUS = ['новая', 'выдержала критику', 'в работе', 'отвергнута', 'перенесена'] +# Вид записи: папка и префикс номера. +FOLDERS = {'result': ('results', 'R'), 'idea': ('ideas', 'I'), 'card': ('sources/cards', 'S')} +# Поля шапки, которые всегда списки, даже когда в записи стоит одно значение. +MANY = ('depends', 'sources', 'lean') + + +@dataclass +class Doc: + path: Path + meta: dict + body: str + + @property + def id(self) -> str | None: + """Номер записи из имени файла; None, если имя не подходит под схему.""" + found = re.match(r'[A-Z]+\d+', self.path.stem) + return found.group(0) if found else None + + def many(self, key: str) -> list[str]: + value = self.meta.get(key) or [] + return value if isinstance(value, list) else [value] + + +def read_doc(path: Path) -> Doc: + text = path.read_text(encoding='utf-8').replace('\r\n', '\n') + if not text.startswith('---\n'): + return Doc(path, {}, text) + head, _, body = text[4:].partition('\n---\n') + meta: dict = {} + for line in head.split('\n'): + key, colon, value = line.partition(':') + if not colon or not key.strip() or key.lstrip().startswith('#'): + continue + value = value.strip() + meta[key.strip()] = [item.strip() for item in value[1:-1].split(',') if item.strip()] \ + if value.startswith('[') and value.endswith(']') else value + return Doc(path, meta, body) + + +def write_doc(doc: Doc) -> None: + lines = [f"{key}: [{', '.join(value)}]" if isinstance(value, list) else f'{key}: {value}'.rstrip() + for key, value in doc.meta.items()] + doc.path.write_text('---\n' + '\n'.join(lines) + '\n---\n' + doc.body, encoding='utf-8', newline='\n') + + +def rel(root: Path, path: Path) -> str: + return path.relative_to(root).as_posix() + + +def docs(root: Path, folder: str, prefix: str) -> list[Doc]: + paths = [path for path in (root / folder).glob(f'{prefix}*.md') if re.fullmatch(rf'{prefix}\d+', path.stem)] + return [read_doc(path) for path in sorted(paths, key=lambda path: int(path.stem[len(prefix):]))] + + +def find_doc(root: Path, ident: str) -> Doc: + """Запись по номеру: R07 — результат, I12 — идея, S31 — карточка источника.""" + folder = {prefix: name for name, prefix in FOLDERS.values()}.get(ident[:1].upper()) + path = root / (folder or '') / f'{ident.upper()}.md' + if not folder or not path.is_file(): + raise SystemExit(f'Нет записи {ident}.') + return read_doc(path) + + +def save_doc(root: Path, ident: str, key: str, value: str) -> str: + """Меняет поле шапки; списком становится поле, которое уже список или перечислено в MANY.""" + doc = find_doc(root, ident) + many = isinstance(doc.meta.get(key), list) or key in MANY + doc.meta[key] = [item.strip() for item in value.split(',') if item.strip()] if many else value + write_doc(doc) + return f'{doc.id}: {key} = {value}' + + +# ---------- заготовки ---------- + +RESULT = '''--- +id: {id} +title: {title} +status: цель +depends: [{depends}] +sources: [] +lean: [] +review: +fidelity: +--- + +## Утверждение + +Точная формулировка: объекты, гипотезы, вывод, область определения. + +## Доказательство + +Пока нет. + +## Границы + +Что утверждение не покрывает; какие гипотезы существенны и почему. +''' + +IDEA = '''--- +id: {id} +title: {title} +target: {target} +status: новая +created: {today} +critic: +--- + +## Формулировка + +Гипотезы, вывод, область определения. + +## Набросок + +Шаги по одному. У каждого шага опора: запись R…, карточка источника S…, стандартный факт +с названием или «пробел». + +## Чем убить + +Самая дешёвая проверка, которая опровергла бы идею: частный случай, расчёт, известный пример. + +## Следующий шаг +''' + +CARD = '''--- +source: {source} +verified: +--- + +# {title} + +## Теорема N, с. P + +**Гипотезы.** Все, включая соглашения раздела и статьи («всюду далее …»). + +**Вывод.** + +**Определения, от которых зависит формулировка.** Как они даны в этой работе. + +**Применимость.** Где используется (R…) и как там проверена каждая гипотеза. +''' + +EXPERIMENT = '''--- +id: {id} +title: {title} +idea: {idea} +status: начат +--- + +## Вопрос + +Что проверяем и какой исход опроверг бы гипотезу. + +## Запуск + +`uv run experiments/{id}/run.py` + +## Проверка метода + +Случай с известным ответом и расхождение с ним. + +## Результат + +Таблица чисел с оценкой погрешности. Вывод — «согласуется» или «не согласуется», не «доказано». +''' + +RUN_PY = '''# /// script +# requires-python = ">=3.11" +# dependencies = ["numpy", "scipy", "mpmath", "sympy"] +# /// +"""{title}""" +''' + + +def create(root: Path, kind: str, title: str, **fields) -> Path: + """Создаёт запись со следующим свободным номером; номер занимается созданием файла.""" + if kind == 'experiment': + folder, prefix = root / 'experiments', 'E' + taken = [int(path.name[1:]) for path in folder.glob('E*') if re.fullmatch(r'E\d+', path.name)] + else: + subfolder, prefix = FOLDERS[kind] + folder = root / subfolder + taken = [int(path.stem[len(prefix):]) for path in folder.glob(f'{prefix}*.md') + if re.fullmatch(rf'{prefix}\d+', path.stem)] + folder.mkdir(parents=True, exist_ok=True) + if kind == 'card': + path = folder / f"{fields['source']}.md" + with path.open('x', encoding='utf-8', newline='\n') as handle: + handle.write(CARD.format(source=fields['source'], title=title)) + return path + number = max(taken, default=0) + 1 + while True: + ident = f'{prefix}{number:02d}' + try: + if kind == 'experiment': + (folder / ident).mkdir() + (folder / ident / 'README.md').write_text( + EXPERIMENT.format(id=ident, title=title, idea=fields.get('idea', '')), + encoding='utf-8', newline='\n') + (folder / ident / 'run.py').write_text(RUN_PY.format(title=title), encoding='utf-8', newline='\n') + return folder / ident / 'README.md' + stub = RESULT if kind == 'result' else IDEA + path = folder / f'{ident}.md' + with path.open('x', encoding='utf-8', newline='\n') as handle: + handle.write(stub.format(id=ident, title=title, today=f'{date.today():%Y-%m-%d}', + depends=fields.get('depends', ''), target=fields.get('target', ''))) + return path + except FileExistsError: + number += 1 + + +def card_for(root: Path, code: str, title: str) -> Path: + """Карточка теоремы источника; `title` — строка шапки, собранная из реестра.""" + return create(root, 'card', title, source=code.upper()) diff --git a/tests/test_create.py b/tests/kit/test_create.py similarity index 96% rename from tests/test_create.py rename to tests/kit/test_create.py index 00a5048..651edd3 100644 --- a/tests/test_create.py +++ b/tests/kit/test_create.py @@ -1,4 +1,7 @@ -"""Generator and upgrade regression tests; no network, Git initialization or Lean.""" +"""Generator and upgrade regression tests; no network, Git initialization or Lean. + + python -m unittest discover -s tests/kit +""" import contextlib import importlib.util import io @@ -7,8 +10,8 @@ import unittest from pathlib import Path -REPO = Path(__file__).resolve().parent.parent -spec = importlib.util.spec_from_file_location('create_project', REPO / 'create.py') +REPO = Path(__file__).resolve().parents[2] +spec = importlib.util.spec_from_file_location('create_project', REPO / 'tools/create.py') create_project = importlib.util.module_from_spec(spec) spec.loader.exec_module(create_project) diff --git a/template/tests/harness_runtime.mjs b/tests/template/harness_runtime.mjs similarity index 95% rename from template/tests/harness_runtime.mjs rename to tests/template/harness_runtime.mjs index 06d58b6..c521725 100644 --- a/template/tests/harness_runtime.mjs +++ b/tests/template/harness_runtime.mjs @@ -1,12 +1,13 @@ // Contract check against the real, pinned Harness packages. No LLM calls. -// node tests/harness_runtime.mjs /path/to/node_modules [--mcp] +// node tests/template/harness_runtime.mjs /path/to/node_modules [--mcp] import assert from 'node:assert/strict'; import { readFile } from 'node:fs/promises'; import { createRequire } from 'node:module'; import { dirname, resolve } from 'node:path'; import { fileURLToPath, pathToFileURL } from 'node:url'; -const root = resolve(dirname(fileURLToPath(import.meta.url)), '..'); +// tests/template/ -> repository root, where template/scripts/harness.py writes output/. +const root = resolve(dirname(fileURLToPath(import.meta.url)), '..', '..'); if (!process.argv[2]) throw new Error('Pass the node_modules directory containing @deepseek-ai/dsh'); const modules = resolve(process.argv[2]); const requireDsh = createRequire(resolve(modules, '@deepseek-ai/dsh/package.json')); diff --git a/tests/template/test_docs.py b/tests/template/test_docs.py new file mode 100644 index 0000000..7b71846 --- /dev/null +++ b/tests/template/test_docs.py @@ -0,0 +1,88 @@ +"""Согласованность документации с составом воркфлоу. + +Документация называет команды, роли и пути словами. Тест читает её и сверяет с +фактическим составом `.claude/`: упомянутая команда должна существовать, каждый навык +должен быть назван, названный путь — существовать. Новых сущностей тест не закрепляет. + +Инструкции проекта (`AGENTS.md`, `DEEPSEEK.md`, `README.md` шаблона) читаются в раскладке +созданного проекта: имена команд и ролей от неё не зависят, а пути к производным файлам +в наборе и в проекте лежат в разных местах. + + python -m unittest discover -s tests/template +""" +import re +import sys +import tempfile +import unittest +from pathlib import Path + +TEMPLATE = Path(__file__).resolve().parents[2] / 'template' +REPO = TEMPLATE.parent +sys.path.insert(0, str(TEMPLATE / 'scripts')) +import harness # noqa: E402 + +# Инструкции набора: адресованы тому, кто создаёт проект, поэтому лежат вне заготовки. +KIT_DOCS = (REPO / 'README.md', REPO / 'docs/guide.md') +# Инструкции проекта: создание копирует их в корень нового проекта. +PROJECT_DOCS = (TEMPLATE / 'README.md', TEMPLATE / 'AGENTS.md', TEMPLATE / 'DEEPSEEK.md') +# Появляются при работе: сводки собирает proj.py sync, каталог — lit.py, записи и опыты +# создают команды. Их в заготовке нет по замыслу. +GENERATED = {'blueprint.md', 'ideas/README.md', 'sources/catalog.md', 'results/R01.md', + 'experiments/E01/run.py'} +# Названы в собственной раскладке: у навыка свои scripts/ и reference/, а `harness_runtime.mjs` +# в наборе лежит вне заготовки. +OWN_LAYOUT = {'scripts/check_fragment.py', 'tests/template/harness_runtime.mjs'} + + +class DocumentationMatchesWorkflow(unittest.TestCase): + def setUp(self): + self.folder = tempfile.TemporaryDirectory() + self.addCleanup(self.folder.cleanup) + self.project = Path(self.folder.name) / 'project' + self.project.mkdir() + self.docs = {} + for path in KIT_DOCS: + self.docs[path.name] = path.read_text(encoding='utf-8') + for path in PROJECT_DOCS: + self.docs[path.name] = path.read_text(encoding='utf-8') + self.instructed = '\n'.join(self.docs.values()) + self.agents, self.skills = harness.sources(TEMPLATE) + self.bodies = [body for _, _, body in list(self.agents.values()) + list(self.skills.values())] + self.bodies += list(self.docs.values()) + + def test_mentioned_commands_exist(self): + """`/имя` в документации — команда, которая есть в составе воркфлоу.""" + for name, text in self.docs.items(): + for command in set(re.findall(r'`/([a-z][\w-]+)', text)): + self.assertIn(command, self.skills, f'{name}: команды /{command} нет') + + def test_every_skill_is_named_somewhere(self): + for name in self.skills: + self.assertIn(name, self.instructed, f'навык `{name}` не упомянут в документации') + + def test_documented_paths_exist(self): + """Путь, названный в инструкции, есть в заготовке; схемы имён вроде `ideas/I…` не в счёт.""" + pattern = re.compile(r'(? Path: + """Настраивает proj и lit на каталог шаблона.""" + proj.configure(TEMPLATE) + lit.configure(TEMPLATE) + return TEMPLATE LEAN = '''module @@ -106,14 +121,15 @@ def setUp(self): def tearDown(self): self.folder.cleanup() + _as_template() def test_new_numbers_and_front_matter(self): first = proj.new('result', 'Первая: с двоеточием') second = proj.new('result', 'Вторая', depends='R01') self.assertEqual((first.name, second.name), ('R01.md', 'R02.md')) - doc = proj.read_doc(second) + doc = records.read_doc(second) self.assertEqual((doc.meta['id'], doc.meta['status'], doc.meta['depends']), ('R02', 'цель', ['R01'])) - self.assertEqual(proj.read_doc(first).meta['title'], 'Первая: с двоеточием') + self.assertEqual(records.read_doc(first).meta['title'], 'Первая: с двоеточием') proj.set_field('R02', 'lean', 'Demo.const_even, Demo.scaled_even') self.assertEqual(proj.find_doc('R02').meta['lean'], ['Demo.const_even', 'Demo.scaled_even']) with self.assertRaises(SystemExit): @@ -165,6 +181,24 @@ def test_hygiene_ignores_comments(self): class Sources(unittest.TestCase): + def test_configure_points_paths_at_the_project(self): + """Пути источников выводятся из корня, а не из места установки скрипта.""" + with tempfile.TemporaryDirectory() as folder: + root = Path(folder) + (root / 'project.toml').write_text('[project]\nlib = "Demo"\n[sources]\ndirect_hosts = ["example.org"]\n', + encoding='utf-8') + (root / 'sources' / 'cards').mkdir(parents=True) + (root / 'sources' / 'papers.json').write_text('[]', encoding='utf-8') + records.card_for(root, 'S7', 'Теорема о базисах') + try: + lit.configure(root) + self.assertEqual(lit.REGISTRY, root / 'sources' / 'papers.json') + self.assertEqual(lit.DB, root / 'output' / 'literature' / 'index' / 'lit.sqlite') + self.assertEqual(lit.DIRECT_HOSTS, ['example.org']) + self.assertEqual(lit.cards(), {'S7'}) + finally: + _as_template() + def test_identifiers(self): cases = { '2107.12209v2': ('arxiv', '2107.12209v2'), diff --git a/create.py b/tools/create.py similarity index 94% rename from create.py rename to tools/create.py index fa0f3ed..fee0ebd 100644 --- a/create.py +++ b/tools/create.py @@ -1,11 +1,14 @@ """Новый исследовательский проект из template/ или обновление инструментов в существующем. - python create.py ПАПКА --lib Spectra --title "Название темы" [--pins-from ПРОЕКТ] [--no-git] - python create.py --update ПРОЕКТ [--dry-run] + python tools/create.py ПАПКА --lib Spectra --title "Название темы" [--pins-from ПРОЕКТ] [--no-git] + python tools/create.py --update ПРОЕКТ [--dry-run] Создание копирует весь шаблон и подставляет имя библиотеки и название. Обновление переписывает только инструменты (правила, скрипты, агентов, команды, тесты); постановка, записи, идеи, источники, библиотека Lean и статья не трогаются. + +Команды ниже в подсказках выполняются уже в папке созданного проекта, где этот файл +лежит как scripts/proj.py. """ from __future__ import annotations @@ -19,7 +22,7 @@ import tomllib from pathlib import Path -TEMPLATE = Path(__file__).resolve().parent / 'template' +TEMPLATE = Path(__file__).resolve().parent.parent / 'template' # Файлы, которыми владеет шаблон: обновление переписывает их в проекте TOOLING = ['AGENTS.md', 'CLAUDE.md', 'DEEPSEEK.md', 'scripts/*', 'tests/*', '.claude/agents/*', '.claude/commands/*', '.claude/skills/*', 'sources/README.md', 'experiments/README.md', '.github/workflows/ci.yml']