1

我最近开始使用 Isabelle/jEdit。我为 Simpl AFP 条目创建了一个堆映像。我使用命令行isabelle build工具来创建新图像。我可以通过 ProofGeneral 和Isabelle/Eclipse查看和使用该图像。不幸的是，我无法通过 jEdit 看到它。

如果使用：

isabelle jedit -d isabelle_afp/Simpl -l Simpl

我可以看到 Simpl，但我相信它只是即时重建 Simpl 图像。

有任何想法吗？

这是位于预期位置的堆：

~ > 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
4

2 回答 2

2

请参阅http://afp.sourceforge.net/using.shtml，了解如何将 AFP 注册为 Isabelle 中的组件。

这告诉 Isabelle AFP ROOT 会话文件在哪里。您可以将其视为将 AFP 添加到搜索路径中。

于 2014-03-12T21:38:35.830 回答
0

在类似于 UNIX 的 Isabelle 用户主目录（不是 Isabelle 系统本身的主目录）中~/.isabelle（对于 Windows 不知道），ROOTS如果文件不存在，您可以创建一个文件。如果还没有这样的行，那么在ROOTS添加$AFP一行（字面意思是不要扩展变量）。如果该Simpl理论仍未出现在 jEdit 的 Isabelle 理论列表中，则可能是 AFP 设置不正确。如果是，请检查该文件~/.isabelle/etc/components并查看该文件是否包含您为 AFP 的本地副本选择的位置所在的行。

于 2014-04-20T02:28:14.967 回答