Создание документации по Изабелле HTML * без доказательств *

Question

Я хочу создать документацию HTML для теорий Изабель (например, сеанс HOL), но без включения доказательств.

То есть, я хотел бы производить страницы, как http://isabelle.in.tum.de/library/HOL/Nat.html , но вместо того, чтобы, например,

lemma diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==> 
    (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n" 
    apply (rule_tac x = m in spec) 
    apply (induct n) 
    prefer 2 
    apply (rule allI) 
    apply (induct_tac x, iprover+) 
    done 

Я хочу видеть только

lemma diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==> 
    (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n" 

Причина заключается в том, что я использую HTML страницы чтобы посмотреть, какие теоремы доступны, но доказательства только отвлекают в этом случае. (Я знаю, что исключение доказательств возможно при создании PDF-документа, но меня особенно интересует документация HTML.)

Answer 1

К сожалению, в настоящее время в Isabelle нет встроенного способа сделать это (генерирование HTML используется для добавления дайджеста несколько лет назад, но это больше не предоставляется).

Вы можете думать о постобработке сгенерированных HTML-файлов, но это сложнее, чем может показаться.

Ваши лучшие ставки в настоящее время очертание PDF и, как говорит Крис, используя команду

find_theorems name: "MyThy." 

, чтобы получить список всех теорем в теории MyThy. Вы можете увеличить команду find_theorems с помощью выражений терминов или просто константных имен, чтобы сузить область поиска до конкретных констант. Это обычно более эффективно, чем просмотр длинных списков теорем. Аналогичным образом вы можете использовать команду find_consts, чтобы найти константы по типу, имени константы или имени теории, например. для получения списка всех констант, определенных в одной теории.

Answer 2

Я недавно наткнулся на вывод coqdoc и могу понять этот вопрос с этой точки зрения, хотя страницы Coq HTML теперь также показывают их возраст.

В Isabelle презентация HTML была когда-то очень важной, тогда другие инструменты, такие как онлайн find_theorems или автономные документы PDF, стали более мощными и полезными, и теперь есть также Isabelle/jEdit с качествами отображения, которые приближают браузеры HTML с того времени, когда Исходный вывод Isabelle был впервые реализован.

Я не знаю, как легко получить то, что вы просите в современной Isabelle2013, но это не невозможно, в основном требуется некоторое обновление старых вещей, соответствующих новым концепциям. Поскольку HTML-просмотр со статическими веб-страницами в наши дни немного старомоден, он пока не получил главного приоритета.

В любом случае Isabelle/Scala (являющийся официальным программным интерфейсом системы Isabelle) уже предоставляет некоторые общедоступные операции API, чтобы получить деревья XML из разметки документа PIDE, которые вы видите в Интернете в Isabelle/jEdit, например. Оттуда это не очень далеко от HTML + CSS, для людей, которые понимают этот бизнес. Однако, возможно, было бы более быстро и полезно использовать некоторую презентацию в Isabelle/jEdit, минуя множество веб-браузеров и их причуды.