伊莎贝尔的文件准备

Question

我想获取与 this theory 关联的 LaTeX 代码。以前的答案仅提供指向文档的链接。让我描述一下我做了什么。

我进入Hales.thy的目录执行isabelle mkroot，然后isabelle build -D .，生成了一个名为document的文件和一个可疑的*.pdf文件（几乎）是空的。通过添加 Hales.thy 作为参数修改此命令未成功。

如果有人能简要描述所需的命令，我将不胜感激。

Answer 1

作为预防措施，将文件 Hales.thy 复制到一个不包含任何其他文件的新目录中，然后再次运行 isabelle mkroot。
如果我没理解错的话，你的理论包含sorry。在这种情况下，要使构建成功，您需要启用 quick_and_dirty 模式。为此，在您的理论文件中第一次出现 sorry 之前，您需要插入 declare [[quick_and_dirty=true]].
您的理论包含格式不正确的原始文本。尝试用以下内容替换相关行：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›.
完成后，您应该可以使用下面附录中的 ROOT 文件。如您所见，我已经明确指定了理论文件，还添加了相关的导入会话。

附录

session Hales = HOL +
  options [document = pdf, document_output = "output"]
sessions
  "HOL-Library"
  "HOL-Algebra"
theories
  "Hales"
document_files
  "root.tex"

伊莎贝尔的文件准备

Isabelle's document preparation

latex

isabelle