libisabelle與現有的Isabelle安裝

Question

我想使用libisabelle從Scala調用Isabelle。但是，默認情況下（即使用tutorial中描述的調用），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。