1

这是一个后续行动

在 Isabelle 中加载预编译的堆映像

现在我在 Windows 上。我在标准位置创建了一个 Nominal2 堆映像：

$HOME/.isabelle/Isabelle2015/heaps/polyml-5.5.2_x86-cygwin

我无法在“理论”面板中选择它来加载。

我尝试isabelle jedit -d ... -l ...从 cygwin bash 脚本开始，但没有奏效。脚本包含

#!/bin/bash

isabelle jedit -d /cygdrive/d/phd/thy/Nominal2-Isabelle2015/Nominal  -l Nominal2

但 id 什么也没做，jEdit 没有出现。

如何创建一个可执行文件来自动加载我预构建的 Nominal2 映像？或者，让 Isabelle/jEdit 知道标准堆位置中有一个 Nominal2 图像？

更新：我将图像从用户的主目录复制到主堆目录：

in /cygdrive/d/isabelle/Isabelle2015/heaps/polyml-5.5.2_x86-cygwin 

$ cp ~/.isabelle/Isabelle2015/heaps/polyml-5.5.2_x86-cygwin/Nominal2 .

并重新启动 Isabelle/jEdit 但我在菜单中找不到Nominal2会话图像。

4

1 回答 1

1

与其尝试手动组装堆图像并移动它们，不如让系统来做。isabelle jedit -d DIR您只需要通过某个 ROOTS 文件（在某个已知的会话目录中）或永久地告诉它在哪里找到会话源树。

一个好地方是$ISABELLE_HOME_USER/ROOTS：只需在单独的行上添加目录位置（以 Isabelle/POSIX 表示法），并且 Isabelle/jEdit 逻辑选择器应该知道重新启动后的新会话。

然后你可以选择一个新的会话，它的堆将在应用程序下一次重启后建立。

于 2015-10-07T19:20:53.853 回答