如何在根中指定非文档理论文件？
如何在根中指定非文档理论文件？
提问于 2014-07-25 13:41:11
我将Nominal2导入到我的主要理论文件中，而在Isabelle/jEdit中，我可以使用atom_decl来工作。在根用户中，我尝试了各种尝试来指定Nominal2，如
session "techreport" = "HOL" +
options [document = pdf, document_output = "output"]
theories [document = false]
Nominal2
theories
IsarIntroduction
files "document/root.tex" 但我得到了bad input或No such file: "Nominal2.thy"。我试图从IsarIntroduction的dir和root.tex的dir指定一个相对路径，但都是徒劳的。
如何为Nominal2理论指定路径？
更新:我使用了一个专门为Isabelle/JEdit构建的Nominal2映像
回答 2
Stack Overflow用户
回答已采纳
发布于 2014-08-02 11:57:34
您还应该能够构建会话(图像) Nominal2，就像在Isabelle/jEdit中所做的那样。例如：
session "techreport" = "Nominal2" +
options [document = pdf, document_output = "output"]
theories
IsarIntroduction
files "document/root.tex" Stack Overflow用户
发布于 2014-07-25 18:24:12
有人摆弄我找到了解决办法。
No such file: "Nominal2.thy"消息来自于isabelle build进程，它没有看到伊莎贝尔/jEdit使用的带有Nominal2的预构建映像。因此，给出了Nominal2在主理论文件IsarIntroduction.thy和ROOT文件中的完整路径，解决了该问题。
但是有一个警告:我得到了一个超过200页的文档，其中包含了Infinite_Set.thy的所有开发。原木
Loading theory "Infinite_Set" (required by "IsarIntroduction"
via "Nominal2" via "Nominal2_Base")所以我不得不包括
theories [document = false]
"Nominal2-Isabelle2013-1/Nominal/Nominal2"
"~~/src/HOL/Library/Infinite_Set"在ROOT中防止这种情况发生。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/24957145
复制相关文章
相似问题
腾讯云开发者
