From e131a0ae195c487c5f85189b280875ceeced624a Mon Sep 17 00:00:00 2001
From: Dominique Unruh <9913676+dominique-unruh@users.noreply.github.com>
Date: Fri, 29 Dec 2023 16:53:01 +0100
Subject: [PATCH] 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).
---
 src/main/scala/de/unruh/isabelle/control/Isabelle.scala       | 4 +++-
 src/test/scala/de/unruh/isabelle/pure/CtermTest.scala         | 2 +-
 src/test/scala/de/unruh/isabelle/pure/CtypTest.scala          | 2 +-
 .../de/unruh/isabelle/pure/exceptions/MLExceptionTest.scala   | 2 +-
 4 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/main/scala/de/unruh/isabelle/control/Isabelle.scala b/src/main/scala/de/unruh/isabelle/control/Isabelle.scala
index a57ec0c..ced6cf2 100644
--- 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
index 5adb2c3..a06469f 100644
--- 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
index 04e6871..5e538c0 100644
--- 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
index d3cc1bd..80ced71 100644
--- 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)