我最近开始使用伊莎贝尔/绝地。我已经为simlpafp条目创建了一个堆映像。我使用命令行isabelle build工具创建新图像。我可以看到并使用ProofGeneral和Isabelle/Eclipse的图像。不幸的是，我无法通过绝地武士看到它。
如果使用：
isabelle jedit -d isabelle_afp/Simpl -l Simpl
我可以看到simp，但我相信它只是在飞行中重建一个simp图像。
有什么想法吗？
这是位于预期位置的堆：
~ > ls -l .isabelle/Isabelle2013-2/heaps/polyml-5.5.1_x86_64-linux/
total 425424
-r--r--r-- 1 george users 435622904 Feb 24 11:32 Simpl
drwxr-xr-x 2 george users 4096 Feb 24 11:32 log
我的系统是这样的：
~ > uname -a
Linux athina 3.11.1 #4 SMP Wed Jan 22 16:45:25 EST 2014 x86_64 Intel(R) Core(TM) i5 CPU M 560 @ 2.67GHz GenuineIntel GNU/Linux
最佳答案
有关如何在Isabelle中将AFP注册为组件的信息，请参见http://afp.sourceforge.net/using.shtml。
这会告诉Isabelle AFP根会话文件在哪里。可以将其视为将AFP添加到搜索路径中。