Как генерировать html-версию теории Изабеллы

Question

У меня есть файл теории Изабеллы, называемый John.thy. Я хотел бы показать это моему другу, но у моего друга нет Изабеллы, а сырые файлы .thy не так-то просто читать. Я видел некоторые веб-страницы в библиотеке Isabelle (например, этот: http://isabelle.in.tum.de/library/HOL/Finite_Set.html), которые имеют довольно синтаксическую подсветку, и я хотел бы, чтобы моя теория выглядела так.

Так как я могу сделать John.html? Я просмотрел документацию, и все это выглядит довольно страшно и сложно, что со всеми файлами сборки и файлами и т. П. Может ли какая-то душа объяснить самый простой способ сделать это?

Answer 1

Первый ответ на ваш вопрос (см также Isabelle System Manual, раздел 3.2 - параметры системы сборки):

Для генерации HTML для John.thy, создайте файл с именем ROOT, в том же каталоге, John.thy, со следующим содержанием

session John = "HOL" + 
    theories 
    John 

, а затем, оставаясь в том же каталоге, вызовите

isabelle build -d . -o browser_info -v John 

где

• -d . указывает, что текущий каталог следует искать сессий (которые указаны в файле ROOT)
• -o browser_info является существенным флаг для генерации HTML (А.К.А. информации браузер) и
• -v (многословные флаг) полезно, чтобы увидеть, в каком каталог результат помещается

выше вызов будет что-то подобное

Started at Thu Jul 25 09:38:20 JST 2013 [...] 
[...] 
Session Pure 
Session HOL (main) 
Session John 
Running John ... 
John: theory John 
[...] 
Browser info at /home/username/.isabelle/Isabelle2013/browser_info/HOL/John 
[...] 

(где [...] указывает пропущенный вывод). Итак, вы видите, в какой директории вы должны проконсультироваться, чтобы получить файлы HTML.

Сказав это, по крайней мере, по следующим причинам я лично предпочитаю PDF над HTML:

• с -o browser_info вы получите кучу файлов в директории (а не только один автономный файл при использовании -o document=pdf)
• не все символы Изабель красиво отображаются в HTML (в то время как вы имеете полный контроль над символами при генерации PDF)

Примечание: Если вы используете приложение Isabelle Isabelle для Mac OS, вам может потребоваться заменить isabelle выше на /Applications/Isabelle2013.app/Isabelle/bin/isabelle или добавить /Applications/Isabelle2013.app/Isabelle/bin/ на ваш PATH.