如何在 ROOT 中指定非文档理论文件

Question

我将Nominal2导入到我的主理论文件中，在Isabelle/jEdit中，我可以使用atom_decl使其正常工作。在 ROOT 中，我尝试了各种尝试来指定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的目录和root.tex的目录指定一个相对路径，但徒劳无功。

如何指定Nominal2理论的路径？

更新：我为伊莎贝尔/JEdit 使用特意构建的 Nominal2 图像

Answer 1

您还应该能够像在Isabelle/jEdit中那样在会话(图像(Nominal2上进行构建。例如：

session "techreport" = "Nominal2" + 
   options [document = pdf, document_output = "output"] 
   theories 
     IsarIntroduction 
   files "document/root.tex" 

Answer 2

一些摆弄使我找到了解决方案。

No such file: "Nominal2.thy"消息来自isabelle build进程，该进程看不到Isabelle/jEdit使用的带有Nominal2的预构建映像。因此，在主理论文件IsarIntroduction.thy和ROOT文件中给出Nominal2的完整路径解决了这个问题。

不过有一个警告：我得到了一份两百多页长的文档，其中包括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防止这种情况发生。