Подготовка документа Изабель

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

Я перешел в каталог Hales.thy и выполнил isabelle mkroot, а затем isabelle build -D ., который сгенерировал файл с именем document и файл *.pdf, который был подозрительно (почти) пуст. Модификации этой команды путем добавления Hales.thy в качестве параметра не увенчались успехом.

Буду признателен, если кто-нибудь сможет кратко описать необходимые команды.


latex isabelle
person Rodrigo    schedule 10.08.2019    source источник

Ответы (1)


arrow_upward
6
arrow_downward

  1. В качестве меры предосторожности скопируйте файл Hales.thy в новый каталог, не содержащий других файлов, и снова запустите isabelle mkroot.
  2. Если я правильно понял, ваша теория содержит sorry. В этом случае для успешной сборки необходимо включить режим quick_and_dirty. Для этого перед первым появлением sorry в вашем файле теории необходимо вставить declare [[quick_and_dirty=true]].
  3. Ваша теория содержит необработанный текст, который неправильно отформатирован. Попробуйте заменить соответствующие строки следующими: text‹The case \<^text>‹t^2 = 1› corresponds to a product of intersecting lines which cannot be a group› и text‹The case \<^text>‹t = 0› corresponds to a circle which has been treated before›.
  4. Как только это будет сделано, вы сможете использовать файл ROOT в приложении ниже. Как видите, я явно указал файл теории, а также добавил соответствующие импортированные сеансы.

Приложение

session Hales = HOL +
  options [document = pdf, document_output = "output"]
sessions
  "HOL-Library"
  "HOL-Algebra"
theories
  "Hales"
document_files
  "root.tex"
person user9716869    schedule 10.08.2019
comment
Спецификации команд LaTeX, представленные Изабель в процессе сборки, должны быть разбросаны по соответствующим автоматически сгенерированным файлам * .sty. Вы видите такие файлы, как isabelle.sty и isabellesym.sty в одном каталоге с Hales.tex? Если это так, то при условии, что они включены с использованием \usepackage, LaTeX должен их распознать. Мне любопытно, что именно вы пытаетесь сделать ... Сталкивались ли вы с какими-либо проблемами в процессе сборки после выполнения пунктов 1-4? - person user9716869; 11.08.2019
comment
Кстати, если это имеет для вас смысл, я хотел бы поблагодарить вас за помощь в разделе, который я пишу о доказательстве, но мне понадобится настоящее имя ... - person Rodrigo; 25.11.2019
comment
Спасибо. Как я упоминал ранее, я не ищу какой-либо ссылки. Вы можете предоставить ссылки на соответствующие сообщения в SO в комментариях в коде, если хотите. Однако, на мой взгляд, они не должны появляться в официальных подтверждающих документах (т.е. в сгенерированных файлах * .pdf). Что касается моей личности, то я не скрываю ее ни от кого конкретно, только от широкой публики. Если вам интересно, не стесняйтесь, напишите мне электронное письмо и спросите явно, и я предоставлю его (мне приходилось делать это несколько раз, так что, я думаю, к настоящему времени довольно много людей все равно это знают. ). - person user9716869; 25.11.2019