diff --git a/build.sbt b/build.sbt index 0273bf8cb3211a0b3372d538e34558eed9c7ac59..ca2702c1d5018b3f793f1d6f2fad267ba20b4d80 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 0000000000000000000000000000000000000000..4dda6f88ac85b4d0e91df3611ea0d2b043515316 --- /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 8f762612fd91b062a99d95d799e948da45747c36..8623bd014a7d8f06d41b4859e4d95210f1a03289 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 0000000000000000000000000000000000000000..078659c9c138fce536196c7642d5496dd85d9311 --- /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 +}