Merge pull request #189 from larsrh/topic/libisabelle-0.3

update to libisabelle 0.3

.gitmodules

-[submodule "unmanaged/isabelle/protocol"]
-	path = unmanaged/isabelle/protocol
-	url = https://github.com/larsrh/libisabelle-protocol.git

ROOTS

-unmanaged/isabelle/protocol
-src/main/isabelle

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",
@@ -88,13 +88,11 @@ script := {
       s.log.info("Generating '"+f.getName+"' script ("+(if(is64) "64b" else "32b")+")...")
     }
     val paths = (res.getAbsolutePath +: out.getAbsolutePath +: cps.map(_.data.absolutePath)).mkString(System.getProperty("path.separator"))
-    val base = baseDirectory.value.getAbsolutePath
     IO.write(f, s"""|#!/bin/bash --posix
                     |
                     |SCALACLASSPATH="$paths"
-                    |BASEDIRECTORY="$base"
                     |
-                    |java -Xmx2G -Xms512M -Xss64M -classpath "$${SCALACLASSPATH}" -Dleon.base="$${BASEDIRECTORY}" -Dscala.usejavacp=false scala.tools.nsc.MainGenericRunner -classpath "$${SCALACLASSPATH}" leon.Main $$@ 2>&1 | tee -i last.log
+                    |java -Xmx2G -Xms512M -Xss64M -classpath "$${SCALACLASSPATH}" -Dscala.usejavacp=false scala.tools.nsc.MainGenericRunner -classpath "$${SCALACLASSPATH}" leon.Main $$@ 2>&1 | tee -i last.log
                     |""".stripMargin)
     f.setExecutable(true)
   } catch {

project/plugins.sbt

 addSbtPlugin("com.typesafe.sbt" % "sbt-site" % "0.8.1")
+
+addSbtPlugin("info.hupel" % "sbt-libisabelle" % "0.1")

src/main/isabelle/ROOT

-session Leon_Deps = "HOL-Protocol2015" +
+session Leon_Deps = "HOL-Protocol" +
   theories
     "~~/src/HOL/Word/Word"
     "~~/src/HOL/Library/Simps_Case_Conv"

src/main/scala/leon/solvers/isabelle/Component.scala

@@ -17,30 +17,8 @@ object Component extends LeonComponent {
   val name = "Isabelle"
   val description = "Isabelle solver"
 
-  val leonBase =
-    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
-  )
+  def platform =
+    Platform.guess.getOrElse(sys.error("Unknown platform; can't run Isabelle here"))
 
   val optMapping = LeonFlagOptionDef(
     name = "isabelle:mapping",
@@ -62,6 +40,6 @@ object Component extends LeonComponent {
   )
 
   override val definedOptions: Set[LeonOptionDef[Any]] =
-    Set(optBase, optDownload, optBuild, optMapping, optDump, optStrict)
+    Set(optMapping, optDump, optStrict)
 
 }

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) {
 

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

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

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) {
 

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])

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")

src/sphinx/isabelle.rst

@@ -28,20 +28,10 @@ verification.
 Installation
 ------------
 
-You can obtain a copy of Isabelle for your operating system at `its website
-<https://isabelle.in.tum.de/>`_, then follow the `installation instructions
-<https://isabelle.in.tum.de/installation.html>`_. The installation path needs
-to be passed to Leon via the ``--isabelle:base`` command line option. (The path
-will end in ``Isabelle2015``. Depending on your operating system, this folder
-might be some levels into the installation tree.)
-
-On Linux, you can skip this step. Leon is able to download and install Isabelle
-itself. During the first start, you just need to pass the command line option
-``--isabelle:download=true``. You may specify ``--isabelle:base``, but don't
-have to.
-
-Additionally, you need to instruct Git to fetch all the referenced repositories
-via ``git submodule update --init --recursive``.
+You don't have to obtain a copy of Isabelle. Leon is able to download and
+install Isabelle itself. The installation happens in the appropriate folder for
+your operating system, e.g. ``%APPDATA%`` under Windows or ``$HOME/.local``
+under Linux.
 
 
 Basic usage

src/sphinx/options.rst

@@ -313,27 +313,6 @@ CVC4 Solver
 Isabelle
 ********
 
-* ``--isabelle:base=<path>``
-
-  Specify the installation directory of Isabelle. In Isabelle-parlance, this is
-  called ``$ISABELLE_HOME``. It will have the form ``/path/to/Isabelle2015``.
-  When no Isabelle installation can be found there, the system suggests to
-  enable the ``download`` option.
-
-* ``--isabelle:build``
-
-  Flag to indicate that during the start-up of Leon, Isabelle should
-  automatically build all required library sources. This is on by default, and
-  should usually be left on. Building only happens when some dependencies
-  changed and subsequent runs of Leon don't rebuild the library. However, even
-  if nothing is build, it still requires the system a couple of seconds to
-  figure that out.
-
-* ``--isabelle:download``
-
-  If necessary, perform a full system bootstrap by downloading and unpacking a
-  copy of Isabelle. Off by default. Only supported under Linux.
-
 * ``--isabelle:dump=<path>``
 
   Makes the system write theory files containing the translated definitions

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)
   }

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"))
 
 }

protocol @ c33db5fe

-Subproject commit c33db5fef8af6548c494705e55e6b56e976a10a9