libisabelle与现有的Isabelle安装

Question

我想使用利比沙贝尔从Scala调用Isabelle。但是，在默认情况下(即使用教程中描述的调用)，libisabelle将下载一个新的Isabelle安装。

我希望使用现有的(只读) Isabelle配置。我尝试了以下几点：

val path = "/opt/Isabelle2016-1"
val setup = Setup.detect(Platform.genericPlatform(new File(path).toPath), Version.Stable("2016-1")).right.get
val resources = Resources.dumpIsabelleResources().right.get
val environment = Await.result(setup.makeEnvironment(resources), Duration.Inf)
val config = Configuration.simple("Example")
System.build(environment,config)
val system = System.create(environment,config)

我不知道这是否是我应该做的，但无论如何，它是行不通的：

java.nio.file.AccessDeniedException: /opt/Isabelle2016-1/.lock

所以libisabelle想给伊莎贝尔的装置写信。我希望代码即使在只读安装中也能工作。

在上述情况下，我怎样才能让libisabelle工作呢？

Answer 1

Setup.detect将试图锁定安装，使任何两个进程都不能同时写入它们。

使用genericPlatform可能不像您想的那样，因为您所经过的路径将用于libisabelle从磁盘获取或写入磁盘的所有内容，包括资源。

幸运的是，手动实例化Setup非常简单：

val setup = Setup(
  Paths.get("/opt/Isabelle2016-1"),
  Platform.guess.get,
  Version.Stable("2016-1")
)

有了这个咒语，您将在/opt/Isabelle2016-1中使用全局安装，但是这里没有写任何东西。$ISABELLE_HOME_USER等将指向Linux上的~/.local/share/libisabelle。