From f3db3bd3c0c87a3dda5d7ccfc4b59b6d2f35dc76 Mon Sep 17 00:00:00 2001
From: Lars Hupel <lars.hupel@mytum.de>
Date: Sun, 20 Mar 2016 22:04:38 +0100
Subject: [PATCH] update to libisabelle 0.3

Notable changes:
* sbt-libisabelle plugin which takes care of Isabelle source management
  - no more submodules; Isabelle sources are now packaged in JAR files
  - no weird ROOTS file in the repository root
* less isabelle: flags, everybody would want to use the defaults anyway
* updating to Isabelle2016 becomes possible (future work)
---
 .gitmodules                                   |  3 --
 ROOTS                                         |  2 -
 build.sbt                                     |  6 +--
 project/plugins.sbt                           |  2 +
 src/main/isabelle/ROOT                        |  2 +-
 .../leon/solvers/isabelle/Component.scala     | 23 +---------
 .../leon/solvers/isabelle/Functions.scala     |  1 +
 .../isabelle/IsabelleEnvironment.scala        | 43 ++++++-------------
 .../solvers/isabelle/IsabelleSolver.scala     |  5 ++-
 .../leon/solvers/isabelle/Translator.scala    |  1 +
 .../scala/leon/solvers/isabelle/Types.scala   |  1 +
 .../scala/leon/solvers/isabelle/package.scala | 11 +++--
 .../leon/isabelle/IsabelleLibrarySuite.scala  |  2 +-
 .../isabelle/IsabelleVerificationSuite.scala  |  2 +-
 unmanaged/isabelle/protocol                   |  1 -
 15 files changed, 38 insertions(+), 67 deletions(-)
 delete mode 100644 .gitmodules
 delete mode 100644 ROOTS
 delete mode 160000 unmanaged/isabelle/protocol

diff --git a/.gitmodules b/.gitmodules
deleted file mode 100644
index 58bbf387e..000000000
--- a/.gitmodules
+++ /dev/null
@@ -1,3 +0,0 @@
-[submodule "unmanaged/isabelle/protocol"]
-	path = unmanaged/isabelle/protocol
-	url = https://github.com/larsrh/libisabelle-protocol.git
diff --git a/ROOTS b/ROOTS
deleted file mode 100644
index 011708995..000000000
--- a/ROOTS
+++ /dev/null
@@ -1,2 +0,0 @@
-unmanaged/isabelle/protocol
-src/main/isabelle
diff --git a/build.sbt b/build.sbt
index cafc0af35..601d0234f 100644
--- a/build.sbt
+++ b/build.sbt
@@ -28,10 +28,11 @@ if(System.getProperty("sun.arch.data.model") == "64") {
 
 resolvers ++= Seq(
   "Typesafe Repository" at "http://repo.typesafe.com/typesafe/releases/",
-  "Sonatype OSS Snapshots" at "https://oss.sonatype.org/content/repositories/snapshots"
+  "Sonatype OSS Snapshots" at "https://oss.sonatype.org/content/repositories/snapshots",
+  "Sonatype OSS Releases" at "https://oss.sonatype.org/content/repositories/releases"
 )
 
-val libisabelleVersion = "0.2"
+val libisabelleVersion = "0.3"
 
 libraryDependencies ++= Seq(
   "org.scala-lang" % "scala-compiler" % "2.11.7",
@@ -39,7 +40,6 @@ libraryDependencies ++= Seq(
   "com.typesafe.akka" %% "akka-actor" % "2.3.4",
   "info.hupel" %% "libisabelle" % libisabelleVersion,
   "info.hupel" %% "libisabelle-setup" % libisabelleVersion,
-  "info.hupel" %% "pide-2015" % libisabelleVersion,
   "org.slf4j" % "slf4j-nop" % "1.7.13",
   "org.ow2.asm" % "asm-all" % "5.0.4",
   "com.fasterxml.jackson.module" %% "jackson-module-scala" % "2.6.0-rc2",
diff --git a/project/plugins.sbt b/project/plugins.sbt
index 9a94578c3..fe9172392 100644
--- a/project/plugins.sbt
+++ b/project/plugins.sbt
@@ -1 +1,3 @@
 addSbtPlugin("com.typesafe.sbt" % "sbt-site" % "0.8.1")
+
+addSbtPlugin("info.hupel" % "sbt-libisabelle" % "0.1")
diff --git a/src/main/isabelle/ROOT b/src/main/isabelle/ROOT
index 5c659007c..d95bef0c4 100644
--- a/src/main/isabelle/ROOT
+++ b/src/main/isabelle/ROOT
@@ -1,4 +1,4 @@
-session Leon_Deps = "HOL-Protocol2015" +
+session Leon_Deps = "HOL-Protocol" +
   theories
     "~~/src/HOL/Word/Word"
     "~~/src/HOL/Library/Simps_Case_Conv"
diff --git a/src/main/scala/leon/solvers/isabelle/Component.scala b/src/main/scala/leon/solvers/isabelle/Component.scala
index 55e2eef1e..ad73857cb 100644
--- a/src/main/scala/leon/solvers/isabelle/Component.scala
+++ b/src/main/scala/leon/solvers/isabelle/Component.scala
@@ -21,26 +21,7 @@ object Component extends LeonComponent {
     Paths.get(Option(System.getProperty("leon.base")).getOrElse(".")).toAbsolutePath()
 
   val platform =
-    Platform.guess.getOrElse(Platform.genericPlatform("generic", leonBase.resolve("contrib").toAbsolutePath()))
-
-  val optBase = LeonStringOptionDef(
-    name = "isabelle:base",
-    description = "Base directory of the Isabelle installation",
-    default = platform.setupStorage.toString,
-    usageRhs = "path"
-  )
-
-  val optDownload = LeonFlagOptionDef(
-    name = "isabelle:download",
-    description = "Automatic download of Isabelle",
-    default = false
-  )
-
-  val optBuild = LeonFlagOptionDef(
-    name = "isabelle:build",
-    description = "Automatic build of Isabelle/Leon",
-    default = true
-  )
+    Platform.guess.getOrElse(Platform.genericPlatform(leonBase.resolve("contrib").toAbsolutePath()))
 
   val optMapping = LeonFlagOptionDef(
     name = "isabelle:mapping",
@@ -62,6 +43,6 @@ object Component extends LeonComponent {
   )
 
   override val definedOptions: Set[LeonOptionDef[Any]] =
-    Set(optBase, optDownload, optBuild, optMapping, optDump, optStrict)
+    Set(optMapping, optDump, optStrict)
 
 }
diff --git a/src/main/scala/leon/solvers/isabelle/Functions.scala b/src/main/scala/leon/solvers/isabelle/Functions.scala
index 9e221e988..a258fd1cd 100644
--- a/src/main/scala/leon/solvers/isabelle/Functions.scala
+++ b/src/main/scala/leon/solvers/isabelle/Functions.scala
@@ -14,6 +14,7 @@ import leon.purescala.Types._
 import leon.utils._
 
 import edu.tum.cs.isabelle._
+import edu.tum.cs.isabelle.pure.{Expr => _, _}
 
 final class Functions(context: LeonContext, program: Program, types: Types, funs: List[FunDef], system: System)(implicit ec: ExecutionContext) {
 
diff --git a/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala b/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala
index 944a2e249..8f762612f 100644
--- a/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala
+++ b/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala
@@ -28,9 +28,6 @@ object IsabelleEnvironment {
 
   def apply(context: LeonContext, program: Program): Future[IsabelleEnvironment] = {
     val version = Version(isabelleVersion)
-    val base = Paths.get(context.findOptionOrDefault(Component.optBase))
-    val download = context.findOptionOrDefault(Component.optDownload)
-    val build = context.findOptionOrDefault(Component.optBuild)
     val dump = context.findOptionOrDefault(Component.optDump)
     val strict = context.findOptionOrDefault(Component.optStrict)
 
@@ -53,35 +50,21 @@ object IsabelleEnvironment {
       }
     }.toList
 
-    val home = base.resolve(s"Isabelle${version.identifier}")
-
-    val setup =
-      if (Files.isDirectory(home))
-        Future.successful { Setup(home, Component.platform, version) }
-      else if (!download)
-        context.reporter.fatalError(s"No $version found at $base. Please install manually or set '${Component.optDownload.name}' flag to true.")
-      else
-        Component.platform match {
-          case o: OfficialPlatform =>
-            context.reporter.info(s"No $version found at $base")
-            context.reporter.info(s"Preparing $version environment ...")
-            Setup.install(o, version)
-          case _ =>
-            context.reporter.fatalError(s"No $version found at $base. Platform unsupported, please install manually.")
-        }
+    context.reporter.info(s"Preparing Isabelle setup (this might take a while) ...")
+    val setup = Setup.defaultSetup(version)
 
     val system = setup.flatMap { setup =>
-      val env = Implementations.makeEnvironment(setup.home, classOf[edu.tum.cs.isabelle.impl.Environment])
-      val config = Configuration.fromPath(Component.leonBase, "Leon")
+      val resources = Resources.dumpIsabelleResources()
+      val config = resources.makeConfiguration(Nil, "Leon")
 
-      if (build) {
+      setup.makeEnvironment.flatMap { env =>
         context.reporter.info(s"Building session ...")
         if (!System.build(env, config))
           context.reporter.internalError("Build failed")
-      }
 
-      context.reporter.info(s"Starting $version instance ...")
-      System.create(env, config)
+        context.reporter.info(s"Starting $version instance ...")
+        System.create(env, config)
+      }
     }
 
     val thy = system.flatMap { system =>
@@ -126,10 +109,12 @@ object IsabelleEnvironment {
 
     functions.flatMap(_.data).foreach { _ =>
       if (dump.isEmpty)
-        system.flatMap(_.invoke(Report)(())).assertSuccess(context).foreach { report =>
-          context.reporter.debug(s"Report for $theory ...")
-          report.foreach { case (key, value) =>
-            context.reporter.debug(s"$key: ${canonicalizeOutput(value)}")
+        system.foreach { sys =>
+          sys.invoke(Report)(()).assertSuccess(context).foreach { report =>
+            context.reporter.debug(s"Report for $theory ...")
+            report.foreach { case (key, value) =>
+              context.reporter.debug(s"$key: ${canonicalizeOutput(sys, value)}")
+            }
           }
         }
       else
diff --git a/src/main/scala/leon/solvers/isabelle/IsabelleSolver.scala b/src/main/scala/leon/solvers/isabelle/IsabelleSolver.scala
index 9bf81247d..a6b52a321 100644
--- a/src/main/scala/leon/solvers/isabelle/IsabelleSolver.scala
+++ b/src/main/scala/leon/solvers/isabelle/IsabelleSolver.scala
@@ -16,6 +16,7 @@ import leon.utils.Interruptible
 import leon.verification.VC
 
 import edu.tum.cs.isabelle._
+import edu.tum.cs.isabelle.pure.{Expr => _, _}
 
 class IsabelleSolver(val context: LeonContext, program: Program, types: Types, functions: Functions, system: System) extends Solver with Interruptible { self: TimeoutSolver =>
 
@@ -49,7 +50,7 @@ class IsabelleSolver(val context: LeonContext, program: Program, types: Types, f
   def check: Option[Boolean] = {
     val verdict = sequencePending().flatMapC { ts =>
       Future.traverse(ts)(system.invoke(Pretty)(_).assertSuccess(context)).foreach { strs =>
-        context.reporter.debug(s"Attempting to prove disjunction of ${canonicalizeOutput(strs.mkString(", "))}")
+        context.reporter.debug(s"Attempting to prove disjunction of ${canonicalizeOutput(system, strs.mkString(", "))}")
       }
 
       system.cancellableInvoke(Prove)((ts, method))
@@ -59,7 +60,7 @@ class IsabelleSolver(val context: LeonContext, program: Program, types: Types, f
     try {
       Await.result(verdict.future.assertSuccess(context), timeout) match {
         case Some(thm) =>
-          context.reporter.debug(s"Proved theorem: ${canonicalizeOutput(thm)}")
+          context.reporter.debug(s"Proved theorem: ${canonicalizeOutput(system, thm)}")
           Some(false)
         case None =>
           None
diff --git a/src/main/scala/leon/solvers/isabelle/Translator.scala b/src/main/scala/leon/solvers/isabelle/Translator.scala
index 79c4cfea7..3a0734726 100644
--- a/src/main/scala/leon/solvers/isabelle/Translator.scala
+++ b/src/main/scala/leon/solvers/isabelle/Translator.scala
@@ -14,6 +14,7 @@ import leon.purescala.Types._
 import leon.utils._
 
 import edu.tum.cs.isabelle._
+import edu.tum.cs.isabelle.pure.{Expr => _, _}
 
 final class Translator(context: LeonContext, program: Program, types: Types, system: System)(implicit ec: ExecutionContext) {
 
diff --git a/src/main/scala/leon/solvers/isabelle/Types.scala b/src/main/scala/leon/solvers/isabelle/Types.scala
index 268a1b788..3847d80c5 100644
--- a/src/main/scala/leon/solvers/isabelle/Types.scala
+++ b/src/main/scala/leon/solvers/isabelle/Types.scala
@@ -12,6 +12,7 @@ import leon.purescala.Expressions._
 import leon.purescala.Types._
 
 import edu.tum.cs.isabelle._
+import edu.tum.cs.isabelle.pure._
 
 case class Constructor(term: Term, disc: Term, sels: Map[ValDef, Term])
 case class Datatype(typ: String, constructors: Map[CaseClassDef, Constructor])
diff --git a/src/main/scala/leon/solvers/isabelle/package.scala b/src/main/scala/leon/solvers/isabelle/package.scala
index 490469653..c06f4f59b 100644
--- a/src/main/scala/leon/solvers/isabelle/package.scala
+++ b/src/main/scala/leon/solvers/isabelle/package.scala
@@ -14,6 +14,10 @@ import leon.purescala.Expressions._
 import leon.verification.VC
 
 import edu.tum.cs.isabelle._
+import edu.tum.cs.isabelle.api.Environment
+import edu.tum.cs.isabelle.pure.{Expr => _, _}
+
+import shapeless.tag
 
 object `package` {
 
@@ -108,10 +112,11 @@ object `package` {
     }
   }
 
-  def canonicalizeOutput(str: String) =
-    // FIXME expose this via libisabelle
+  def canonicalizeOutput(system: System, str: String) = {
     // FIXME use this everywhere
-    isabelle.Symbol.decode("""\s+""".r.replaceAllIn(str, " "))
+    val raw = """\s+""".r.replaceAllIn(str, " ")
+    system.env.decode(tag[Environment.Raw].apply(raw))
+  }
 
   val Prove = Operation.implicitly[(List[Term], Option[String]), Option[String]]("prove")
   val Pretty = Operation.implicitly[Term, String]("pretty")
diff --git a/src/test/scala/leon/isabelle/IsabelleLibrarySuite.scala b/src/test/scala/leon/isabelle/IsabelleLibrarySuite.scala
index bf4acc202..ba2ce427d 100644
--- a/src/test/scala/leon/isabelle/IsabelleLibrarySuite.scala
+++ b/src/test/scala/leon/isabelle/IsabelleLibrarySuite.scala
@@ -29,7 +29,7 @@ class IsabelleLibrarySuite extends LeonRegressionSuite {
   test("Define the library") {
     val pipeline = ExtractionPhase andThen new PreprocessingPhase andThen IsabelleNoopPhase
 
-    val ctx = Main.processOptions(Seq("--isabelle:download=true", "--functions=_")).copy(reporter = new TestSilentReporter())
+    val ctx = Main.processOptions(Seq("--functions=_")).copy(reporter = new TestSilentReporter())
 
     pipeline.run(ctx, Nil)
   }
diff --git a/src/test/scala/leon/isabelle/IsabelleVerificationSuite.scala b/src/test/scala/leon/isabelle/IsabelleVerificationSuite.scala
index d8a5ba46f..7540c296d 100644
--- a/src/test/scala/leon/isabelle/IsabelleVerificationSuite.scala
+++ b/src/test/scala/leon/isabelle/IsabelleVerificationSuite.scala
@@ -9,6 +9,6 @@ class IsabelleVerificationSuite extends VerificationSuite {
   val testDir = "regression/verification/isabelle/"
   override val isabelle = true
 
-  val optionVariants: List[List[String]] = List(List("--isabelle:download=true", "--solvers=isabelle"))
+  val optionVariants: List[List[String]] = List(List("--solvers=isabelle"))
 
 }
diff --git a/unmanaged/isabelle/protocol b/unmanaged/isabelle/protocol
deleted file mode 160000
index c33db5fef..000000000
--- a/unmanaged/isabelle/protocol
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit c33db5fef8af6548c494705e55e6b56e976a10a9
-- 
GitLab