From 8ee11c234e525f3a813fee4e413b960e986eb86c Mon Sep 17 00:00:00 2001
From: Lars Hupel <lars.hupel@mytum.de>
Date: Sun, 27 Mar 2016 16:11:54 +0200
Subject: [PATCH] Leon/slf4j log bridge
---
build.sbt | 4 +-
src/main/resources/slf4j-impl-helper | 1 +
.../isabelle/IsabelleEnvironment.scala | 2 +
.../solvers/isabelle/LeonLoggerFactory.scala | 48 +++++++++++++++++++
4 files changed, 53 insertions(+), 2 deletions(-)
create mode 100644 src/main/resources/slf4j-impl-helper
create mode 100644 src/main/scala/leon/solvers/isabelle/LeonLoggerFactory.scala
diff --git a/build.sbt b/build.sbt
index 0273bf8cb..ca2702c1d 100644
--- a/build.sbt
+++ b/build.sbt
@@ -34,15 +34,15 @@ resolvers ++= Seq(
"Sonatype OSS Releases" at "https://oss.sonatype.org/content/repositories/releases"
)
-val libisabelleVersion = "0.3"
+val libisabelleVer = "0.3.1"
libraryDependencies ++= Seq(
"org.scala-lang" % "scala-compiler" % scalaVer,
"org.scalatest" %% "scalatest" % "2.2.4" % "test",
"com.typesafe.akka" %% "akka-actor" % "2.3.4",
- "org.slf4j" % "slf4j-nop" % "1.7.13",
"info.hupel" %% "libisabelle" % libisabelleVer,
"info.hupel" %% "libisabelle-setup" % libisabelleVer,
+ "info.hupel" %% "slf4j-impl-helper" % "0.1",
"org.ow2.asm" % "asm-all" % "5.0.4",
"com.fasterxml.jackson.module" %% "jackson-module-scala" % "2.6.0-rc2",
"com.regblanc" %% "scala-smtlib" % "0.2"
diff --git a/src/main/resources/slf4j-impl-helper b/src/main/resources/slf4j-impl-helper
new file mode 100644
index 000000000..4dda6f88a
--- /dev/null
+++ b/src/main/resources/slf4j-impl-helper
@@ -0,0 +1 @@
+leon.solvers.isabelle.LeonLoggerFactory
diff --git a/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala b/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala
index 8f762612f..8623bd014 100644
--- a/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala
+++ b/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala
@@ -27,6 +27,8 @@ object IsabelleEnvironment {
private implicit val debugSection = DebugSectionIsabelle
def apply(context: LeonContext, program: Program): Future[IsabelleEnvironment] = {
+ LeonLoggerFactory.reporter = context.reporter
+
val version = Version(isabelleVersion)
val dump = context.findOptionOrDefault(Component.optDump)
val strict = context.findOptionOrDefault(Component.optStrict)
diff --git a/src/main/scala/leon/solvers/isabelle/LeonLoggerFactory.scala b/src/main/scala/leon/solvers/isabelle/LeonLoggerFactory.scala
new file mode 100644
index 000000000..078659c9c
--- /dev/null
+++ b/src/main/scala/leon/solvers/isabelle/LeonLoggerFactory.scala
@@ -0,0 +1,48 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon.solvers.isabelle
+
+import org.slf4j.{Logger, ILoggerFactory}
+import org.slf4j.helpers.NOPLogger
+
+import info.hupel.slf4j.DefaultLogger
+
+import leon.Reporter
+import leon.utils._
+
+object LeonLoggerFactory {
+
+ private implicit val debugSection = DebugSectionIsabelle
+
+ private var _reporter: Option[Reporter] = None
+
+ private[isabelle] def reporter_=(r: Reporter): Unit = _reporter = Some(r)
+
+ private[isabelle] def reporter: Reporter = _reporter.getOrElse(sys.error("No reporter set"))
+
+ private class LeonLogger extends DefaultLogger {
+ import DefaultLogger._
+ protected def writeLogMessage(level: LogLevel, message: Option[String], t: Option[Throwable] = None) {
+ message.foreach { m =>
+ level match {
+ case TRACE => reporter.debug(m)
+ case DEBUG => reporter.debug(m)
+ case INFO => reporter.info(m)
+ case WARN => reporter.warning(m)
+ case ERROR => reporter.error(m)
+ }
+ }
+ t.foreach(t => reporter.debug(t))
+ }
+
+ }
+
+}
+
+class LeonLoggerFactory extends ILoggerFactory {
+ override def getLogger(name: String): Logger =
+ if (name startsWith "edu.tum.cs.isabelle")
+ new LeonLoggerFactory.LeonLogger
+ else
+ NOPLogger.NOP_LOGGER
+}
--
GitLab