伊莎贝尔的文件准备

Question

我想获得与该理论相关的 LaTeX 代码。以前的答案仅提供指向文档的链接。让我描述一下我做了什么。

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

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

Answer 1

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"