Avoiding several concurrent initializations of Isabelle in tests.

In CtermTest, CtypTest, MLExceptionTest, class member `ctxt` was initialized before the corresponding test runs. This leads to a concurrent initialization of Isabelle with the Isabelle from, e.g., `Test.README example`. This can lead to conflicts if Isabelle needs to build the heaps first (Pure or HOL).
dominique-unruh · Dec 29, 2023 · e131a0a · e131a0a
1 parent 9a487d0
commit e131a0a
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 4 deletions.
diff --git a/src/main/scala/de/unruh/isabelle/control/Isabelle.scala b/src/main/scala/de/unruh/isabelle/control/Isabelle.scala
@@ -102,6 +102,8 @@ class Isabelle(val setup: SetupGeneral) extends FutureValue {
   private val cleanupFiles = !Utils.checkEnvironmentFlag("SCALA_ISABELLE_NO_CLEANUP")
   private val logQueries = Utils.checkEnvironmentFlag("SCALA_ISABELLE_LOG_QUERIES")
 
+//  logger.debug(new RuntimeException(s"${hashCode()}"))(s"${hashCode()}")
+
   /** This promise will be completed when initializing the Isabelle process finished (first successful communication).
    * Contains an exception if initilization fails. */
   private val initializedPromise : Promise[Unit] = Promise()
@@ -735,7 +737,7 @@ class Isabelle(val setup: SetupGeneral) extends FutureValue {
   private val lastMessages = new mutable.Queue[String]()
   private def logStream(stream: InputStream, level: LogLevel) : Unit = {
     val log = logger(level)
-    val thread = new Thread(s"Isabelle output logger, $level") {
+    val thread = new Thread(s"Isabelle output logger (instance ${this.hashCode()}), $level") {
       override def run(): Unit = {
         try
           new BufferedReader(new InputStreamReader(stream)).lines().forEach { line =>

diff --git a/src/test/scala/de/unruh/isabelle/pure/CtermTest.scala b/src/test/scala/de/unruh/isabelle/pure/CtermTest.scala
@@ -4,7 +4,7 @@ import de.unruh.isabelle.control.IsabelleTest.isabelle
 import org.scalatest.funsuite.AnyFunSuite
 
 class CtermTest extends AnyFunSuite {
-  val ctxt: Context = Context("Main")
+  lazy val ctxt: Context = Context("Main")
 
   test ("Create Cterm from term") {
     val term = Term(ctxt, "1+1::nat")

diff --git a/src/test/scala/de/unruh/isabelle/pure/CtypTest.scala b/src/test/scala/de/unruh/isabelle/pure/CtypTest.scala
@@ -4,7 +4,7 @@ import de.unruh.isabelle.control.IsabelleTest.isabelle
 import org.scalatest.funsuite.AnyFunSuite
 
 class CtypTest extends AnyFunSuite {
-  val ctxt: Context = Context("Main")
+  lazy val ctxt: Context = Context("Main")
 
   test ("Create Ctyp from term") {
     val term = Typ(ctxt, "nat => nat")

diff --git a/src/test/scala/de/unruh/isabelle/pure/exceptions/MLExceptionTest.scala b/src/test/scala/de/unruh/isabelle/pure/exceptions/MLExceptionTest.scala
@@ -15,7 +15,7 @@ import de.unruh.isabelle.pure.Implicits._
 
 class MLExceptionTest extends AnyFunSuite {
   implicit lazy val isabelle: Isabelle = IsabelleTest.isabelle
-  val ctxt: Context = Context("Pure")
+  lazy val ctxt: Context = Context("Pure")
 
   def recognizeExceptionTest[T <: IsabelleMLException](code: String)(implicit classTag: ClassTag[T]) : T = {
     val id = Await.result(isabelle.storeValue(code), Duration.Inf)