Merge pull request #67 from larsrh/issue/66

clean up `etc/components` after failure
larsrh · Apr 30, 2018 · 9c5d580 · 9c5d580
2 parents c27eedf + ec8e782
commit 9c5d580
Show file tree

Hide file tree

Showing 5 changed files with 64 additions and 30 deletions.
diff --git a/modules/pide-interface/src/main/scala/Environment.scala b/modules/pide-interface/src/main/scala/Environment.scala
@@ -71,6 +71,13 @@ object Environment {
   /** Bundles all requirements to instantiate an [[Environment environment]]. */
   case class Context(home: Path, user: Path, components: List[Path], options: List[OptionKey.Update])(implicit val scheduler: Scheduler) {
     def executorService = scheduler.toExecutorService
+
+    // FIXME move to different location?
+    def etc(version: Version) = version match {
+      case Version.Devel(_) => user.resolve(".isabelle").resolve("etc")
+      case Version.Stable(identifier) => user.resolve(".isabelle").resolve(s"Isabelle$identifier").resolve("etc")
+    }
+    def etcComponents(version: Version) = etc(version).resolve("components")
   }
 
 }
@@ -141,11 +148,8 @@ abstract class Environment protected(val context: Environment.Context, versionOv
     case Version.Stable(identifier) => Map("ISABELLE_VERSION" -> identifier)
   })
 
-  final val etc = version match {
-    case Version.Devel(_) => user.resolve(".isabelle").resolve("etc")
-    case Version.Stable(identifier) => user.resolve(".isabelle").resolve(s"Isabelle$identifier").resolve("etc")
-  }
-  final val etcComponents = etc.resolve("components")
+  final val etc = context.etc(version)
+  final val etcComponents = context.etcComponents(version)
 
   protected final def setEtcComponents(): Unit =
     if (!context.components.isEmpty) {

diff --git a/modules/pide/2016-1/src/main/scala/impl/Environment.scala b/modules/pide/2016-1/src/main/scala/impl/Environment.scala
@@ -13,14 +13,18 @@ import shapeless.tag._
 final class Environment private(context: api.Environment.Context) extends api.Environment(context) {
 
   isabelle.Standard_Thread.pool = context.executorService
-  isabelle.Isabelle_System.init(
-    isabelle_root = home.toString,
-    cygwin_root = home.resolve("contrib/cygwin").toString,
-    user = user.toString,
-    init_env = variables,
-    hook = setEtcComponents _
-  )
-  cleanEtcComponents()
+  try {
+    isabelle.Isabelle_System.init(
+      isabelle_root = home.toString,
+      cygwin_root = home.resolve("contrib/cygwin").toString,
+      user = user.toString,
+      init_env = variables,
+      hook = setEtcComponents _
+    )
+  }
+  finally {
+    cleanEtcComponents()
+  }
 
   private def destMarkup(markup: isabelle.Markup) =
     (markup.name, markup.properties)

diff --git a/modules/pide/2016/src/main/scala/impl/Environment.scala b/modules/pide/2016/src/main/scala/impl/Environment.scala
@@ -13,14 +13,18 @@ import shapeless.tag._
 final class Environment private(context: api.Environment.Context) extends api.Environment(context) {
 
   isabelle.Standard_Thread.pool = context.executorService
-  isabelle.Isabelle_System.init(
-    isabelle_root = home.toString,
-    cygwin_root = home.resolve("contrib/cygwin").toString,
-    user = user.toString,
-    init_env = variables,
-    hook = setEtcComponents _
-  )
-  cleanEtcComponents()
+  try {
+    isabelle.Isabelle_System.init(
+      isabelle_root = home.toString,
+      cygwin_root = home.resolve("contrib/cygwin").toString,
+      user = user.toString,
+      init_env = variables,
+      hook = setEtcComponents _
+    )
+  }
+  finally {
+    cleanEtcComponents()
+  }
 
   private def destMarkup(markup: isabelle.Markup) =
     (markup.name, markup.properties)

diff --git a/modules/pide/2017/src/main/scala/impl/Environment.scala b/modules/pide/2017/src/main/scala/impl/Environment.scala
@@ -13,14 +13,18 @@ import shapeless.tag._
 final class Environment private(context: api.Environment.Context) extends api.Environment(context) {
 
   isabelle.Standard_Thread.pool = context.executorService
-  isabelle.Isabelle_System.init(
-    isabelle_root = home.toString,
-    cygwin_root = home.resolve("contrib/cygwin").toString,
-    user = user.toString,
-    init_env = variables,
-    hook = setEtcComponents _
-  )
-  cleanEtcComponents()
+  try {
+    isabelle.Isabelle_System.init(
+      isabelle_root = home.toString,
+      cygwin_root = home.resolve("contrib/cygwin").toString,
+      user = user.toString,
+      init_env = variables,
+      hook = setEtcComponents _
+    )
+  }
+  finally {
+    cleanEtcComponents()
+  }
 
   private def destMarkup(markup: isabelle.Markup) =
     (markup.name, markup.properties)

diff --git a/tests/offline/src/test/scala/EnvironmentSpec.scala b/tests/offline/src/test/scala/EnvironmentSpec.scala
@@ -2,6 +2,8 @@ package info.hupel.isabelle.tests
 
 import java.nio.file.Files
 
+import scala.util.control.NonFatal
+
 import org.specs2.Specification
 import org.specs2.specification.core.Env
 
@@ -13,7 +15,8 @@ class EnvironmentSpec(val specs2Env: Env) extends Specification with BasicSetup
   Environment handling
 
   A low-level environment
-    respects the USER_HOME setting                        ${settingsPrefix must beTrue.awaitFor(duration)}"""
+    respects the USER_HOME setting                        ${settingsPrefix must beTrue.awaitFor(duration)}
+    cleans up etc/components after failure                ${cleanedUp must beTrue.awaitFor(duration)}"""
 
   val classpath = Resolver.Default.resolve(platform, version)
   val user = Files.createTempDirectory("libisabelle_user")
@@ -27,4 +30,19 @@ class EnvironmentSpec(val specs2Env: Env) extends Specification with BasicSetup
     }
   }
 
+  val cleanedUp = classpath.map { paths =>
+    try {
+      val testContext = context.copy(
+        home = Files.createTempDirectory("nonexistent_home"),
+        components = List(Files.createTempDirectory("dummy_component"))
+      )
+      Environment.instantiate(version, paths, testContext)
+    }
+    catch {
+      case NonFatal(ex) =>
+    }
+
+    !Files.exists(context.etcComponents(version))
+  }
+
 }