伊莎贝尔的文件准备 [英] Isabelle's document preparation

问题描述

我想获得与此理论相关的LaTeX代码.先前的答案仅提供指向文档的链接.让我描述一下我的所作所为.

I would like to obtain the LaTeX code associated with this theory. Previous answers only provide links to the documentation. Let me describe what I did.

我进入了 Hales.thy 目录，执行了 isabelle mkroot ，然后执行了 isabelle build -D.，生成了一个文件命名文档和一个 *.pdf 文件，该文件可疑(几乎)为空.通过添加 Hales.thy 作为参数来修改此命令没有成功.

I went to the directory of Hales.thy and executed isabelle mkroot, followed by isabelle build -D ., which generated a file named document and a *.pdf file which was suspiciously (nearly) empty. Modifications of this command by adding Hales.thy as a parameter didn't succeed.

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

I would appreciate if someone could describe briefly the commands needed.

推荐答案

1. 为预防起见，请将文件Hales.thy复制到一个不包含任何其他文件的新目录中，然后再次运行 isabelle mkroot .
2. 如果我的理解正确，您的理论包含 sorry .在这种情况下，要使构建成功，您需要启用 quick_and_dirty 模式.为此，在理论文件中第一次出现 sorry 之前，您需要插入 declare [[quick_and_dirty = true]] .
3. 您的理论包含的原始文本格式不正确.尝试用以下内容替换相关行: text ‹情况\< ^ text> t ^ 2 = 1›对应于不能是组的相交线的产物› 和文本‹案例\< ^ text> t = 0›对应于在›之前被处理过的圆.
4. 完成此操作后，您应该可以使用下面的附录中的 ROOT 文件.如您所见，我已经明确指定了理论文件，还添加了相关的导入会话.

1. As a precaution, copy the file Hales.thy into a new directory that does not contain any other files and run isabelle mkroot again.
2. If I understand correctly, your theory contains sorry. In this case, for the build to succeed you need to enable the quick_and_dirty mode. For this, before the first occurrence of sorry in your theory file, you need to insert declare [[quick_and_dirty=true]].
3. Your theory contains raw text that is not suitably formatted. Try replacing the relevant lines with the following: 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›.
4. Once this is done, you should be able to use the ROOT file in the appendix below. As you can see, I have specified the theory file explicitly and also added the relevant imported sessions.

---

附录

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

这篇关于伊莎贝尔的文件准备的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！