我想获得与相关的 LaTeX 代码这个理论 https://github.com/rjraya/Isabelle/blob/master/curves/Hales.thy。以前的答案仅提供文档的链接。让我描述一下我做了什么。
我去了目录Hales.thy并被处决isabelle mkroot， 其次是isabelle build -D .，它生成了一个名为 document 的文件和一个*.pdf文件可疑（几乎）为空。修改此命令，添加Hales.thy作为参数没有成功。
如果有人能简要描述所需的命令，我将不胜感激。
- 作为预防措施，将文件 Hales.thy 复制到不包含任何其他文件的新目录中并运行
isabelle mkroot again.
- 如果我理解正确的话，你的理论包含
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› and text‹The case \<^text>‹t = 0› corresponds to a circle which has been treated before›.
- 完成此操作后，您应该能够使用
ROOT文件在下面的附录中。如您所见，我已明确指定理论文件，并添加了相关的导入会话。
Appendix
session Hales = HOL +
options [document = pdf, document_output = "output"]
sessions
"HOL-Library"
"HOL-Algebra"
theories
"Hales"
document_files
"root.tex"
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
