libisabelle mit vorhandener Isabelle-Installation

Question

Ich möchte libisabelle verwenden, um Isabelle von Scala aufzurufen. In der Standardeinstellung (d. H. Unter Verwendung des Aufrufs wie in tutorial beschrieben) wird libisabelle eine neue Isabelle-Installation herunterladen.

Ich möchte stattdessen eine vorhandene (schreibgeschützte) Isabelle-Konfiguration verwenden. Ich habe versucht, die folgenden:

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) 

Ich bin nicht sicher, ob dies ist, wie ich soll alles einzurichten, aber auf jeden Fall funktioniert es nicht:

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

So libisabelle schreiben will zur Isabelle-Installation. Ich möchte, dass der Code auch mit einer schreibgeschützten Installation funktioniert.

Wie kann ich libisabelle in der oben genannten Situation arbeiten?

Answer 1

Setup.detect versuchen, die Installation so zu sperren, dass keine zwei Prozesse gleichzeitig in sie schreiben können.

ein genericPlatform wahrscheinlich nicht verwenden nicht das tun, was Sie denken, weil der Weg, den Sie dort passieren wird für alles verwendet werden, die von libisabelle erhält oder auf die Festplatte schreibt, Ressourcen, einschließlich.

Zum Glück Instanziierung ein Setup manuell ist ganz einfach:

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

Mit dieser Beschwörung, werden Sie die globale Installation in /opt/Isabelle2016-1 verwenden, aber nichts wird geschrieben. $ISABELLE_HOME_USER usw. wird unter Linux auf ~/.local/share/libisabelle zeigen.