SKILLEMALL.ai

AC openmath-rocq-theorem

Настраивает среды Rocq, выполняет предварительные проверки и руководит процессом проверки теорем OpenMath Rocq. Используйте, когда пользователь хочет настроить инструменты Rocq, доказать загруженную теорему OpenMath в Rocq/Coq или проверить и отправить доказательство Rocq.

машинный переводПоказать оригиналСкрыть оригинал«Configures Rocq environments, runs preflight checks, and guides the pr…»

Configures Rocq environments, runs preflight checks, and guides the proving workflow for OpenMath Rocq theorems. Use when the user wants to set up Rocq tooling, prove a downloaded OpenMath theorem in Rocq/Coq, or verify and submit a Rocq proof.

ClawHub Agent Skills автор: shentu v1.0.3 MIT-0 5 файлов тело ≈ 1 048 токенов Открыть источникclawhub.ai проанализирован 2 дн назад

Настраивает среды Rocq, выполняет предварительные проверки и руководит процессом проверки теорем OpenMath Rocq.

Как процесс C 58/100 · Есть пробелы — слабые места: результат и критерий готовности, входы и предусловия, согласованность

ПроцедураИнфраструктуратип и темы размечены автоматически по тексту скилла
JSON
Технический рейтинг
A
94/100
безопасность, качество, тесты
Безопасность 60%
100
Качество 40%
86
Прогон на моделях
не было
Процессный рейтинг
C
58/100
Есть пробелы
Результат и критерий готовности вес 14
0
Входы и предусловия вес 11
0
Отчётность по ходу вес 2
0
три самых слабых из десяти параметров · все десять

Такой же скилл встречается ещё в 1 месте: ClawHub

Как улучшить

    Для прогона на моделях — необязательно
    • Свои кейсы (evals/evals.json, 4–6 реальных запросов с ожидаемыми ответами): тогда полная проверка прогонит именно их, а не черновик от модели.
    • spec.yaml с триггерными фразами и утверждениями — контракт поведения для CI; `skilltest init` создаст шаблон.

    Находки guard · 0

    ✓ Критических и высоких находок нет

    Просканировано файлов: 5. Улики замаскированы. Пометки в серых чипах объясняют, почему серьёзность понижена.

    По спецификации Agent Skills

    • заметка frontmatter-key неизвестное поле фронтматтера "requirements"
    • заметка frontmatter-key неизвестное поле фронтматтера "side_effects"

    Процессный рейтинг: все десять параметров 58/100

    • 0Результат и критерий готовности. Не сказано, что считать результатом
    • 0Входы и предусловия. Не сказано, что нужно иметь на входе
    • 0Отчётность по ходу. Скилл ничего не сообщает по ходу работы
    • 30Повторный запуск. Изменяющих операций: 1, без проверки текущего состояния
    • 40Согласованность. Имя во frontmatter (openmath-rocq-theorem) не совпадает с папкой (openmath-rocq-theorems)
    • 60Ошибки и развилки. Развилок: 2
    • 70Когда включается. Сказано, когда применять, но не сказано, когда не стоит
    • 100Инструменты и файлы. Внешние инструменты не нужны
    • 100Шаги. Шагов: 14
    • 100Стоимость исполнения. Тело инструкции 1048 токенов

    Всё перечисленное измерено по тексту скилла, а не оценено моделью: цифры проверяемы. Вес параметра тем больше, чем чаще из-за него процесс встаёт.

    Сигналы качества

    • +5В description нет примеров фраз, по которым скилл должен срабатывать
    • +4Описание не говорит, когда скилл НЕ применять (ложные срабатывания)
    • +3Формат ответа не описан: модель каждый раз решает сама
    • +1Лицензия не указана
    • +2Инструкции на одном языке
    • +3Длина description 244 символов: достаточно сигнала, не съедает бюджет
    • +4Структура: 6 заголовков
    • +3Пошаговые инструкции: 14 пунктов
    • +4Есть примеры (2 блоков кода)
    • +4Справочные файлы упоминаются в инструкциях (3 из 3)

    База качества 70; замечания lint вычитаются, сигналы прибавляют до 100. Итог: 86.

    Внешние проверки

    ClawHub: clean
    This Rocq theorem helper is a markdown-only skill that transparently uses local proof, build, and dependency commands without hidden code or credential access.
    LLM: benign (high) · VirusTotal: · 29 мая 2026 г.