diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala index 9aa0c57ac2371bdaa01df63543a6947312c23a75..43b595df6d1e461c3e3c1e0c1c3a57f1e364573a 100644 --- a/src/main/scala/leon/Settings.scala +++ b/src/main/scala/leon/Settings.scala @@ -12,5 +12,10 @@ object Settings { case class Settings( val synthesis: Boolean = false, val xlang: Boolean = false, - val verify: Boolean = true + val verify: Boolean = true, + val classPath: String = + List( + "/home/ekneuss/scala/scala-2.9.2/lib/", + "/home/ekneuss/git/leon-2.0/library/target/scala-2.9.2/" + ).mkString(":") ) diff --git a/src/main/scala/leon/plugin/ExtractionPhase.scala b/src/main/scala/leon/plugin/ExtractionPhase.scala index fdc271d53cc641d587dde3fbef7b1520579f28e4..72064330bcce1597a5662457383ca90700a3e54e 100644 --- a/src/main/scala/leon/plugin/ExtractionPhase.scala +++ b/src/main/scala/leon/plugin/ExtractionPhase.scala @@ -12,7 +12,7 @@ object ExtractionPhase extends LeonPhase[List[String], Program] { def run(ctx: LeonContext)(args: List[String]): Program = { val settings = new NSCSettings - settings.usejavacp.value = true + settings.extdirs.value = ctx.settings.classPath val compilerOpts = args.filterNot(_.startsWith("--")) @@ -21,6 +21,12 @@ object ExtractionPhase extends LeonPhase[List[String], Program] { } if(command.ok) { + // Debugging code for classpath crap + //new scala.tools.util.PathResolver(settings).Calculated.basis.foreach { cp => + // cp.foreach( p => + // ctx.reporter.info(" => "+p.toString) + // ) + //} val runner = new PluginRunner(settings, ctx, None) val run = new runner.Run run.compile(command.files) diff --git a/web/app/examples/VerificationExamples.scala b/web/app/examples/VerificationExamples.scala index e2027c62a4a74235546900e4132970253b2ca3da..60a053b84d608a5230d67ec1b918d2883e93d09d 100644 --- a/web/app/examples/VerificationExamples.scala +++ b/web/app/examples/VerificationExamples.scala @@ -9,8 +9,8 @@ object VerificationExamples { val default = Example("Default", """ import scala.collection.immutable.Set -import funcheck.Annotations._ -import funcheck.Utils._ +import leon.Annotations._ +import leon.Utils._ object Example { sealed abstract class List @@ -34,8 +34,8 @@ object Example { newExample("Amortized Queue", """ import scala.collection.immutable.Set -import funcheck.Utils._ -import funcheck.Annotations._ +import leon.Utils._ +import leon.Annotations._ object AmortizedQueue { sealed abstract class List @@ -139,8 +139,8 @@ object AmortizedQueue { newExample("Associative List", """ import scala.collection.immutable.Set -import funcheck.Utils._ -import funcheck.Annotations._ +import leon.Utils._ +import leon.Annotations._ object AssociativeList { sealed abstract class KeyValuePairAbs @@ -192,8 +192,8 @@ object AssociativeList { newExample("Insertion Sort", """ import scala.collection.immutable.Set -import funcheck.Annotations._ -import funcheck.Utils._ +import leon.Annotations._ +import leon.Utils._ object InsertionSort { sealed abstract class List @@ -274,8 +274,8 @@ object InsertionSort { newExample("List Operations", """ import scala.collection.immutable.Set -import funcheck.Annotations._ -import funcheck.Utils._ +import leon.Annotations._ +import leon.Utils._ object ListOperations { sealed abstract class List @@ -384,8 +384,8 @@ object ListOperations { newExample("Propositional Logic", """ import scala.collection.immutable.Set -import funcheck.Utils._ -import funcheck.Annotations._ +import leon.Utils._ +import leon.Annotations._ object PropositionalLogic { @@ -488,8 +488,8 @@ object PropositionalLogic { newExample("Red-Black Tree", """ import scala.collection.immutable.Set -import funcheck.Annotations._ -import funcheck.Utils._ +import leon.Annotations._ +import leon.Utils._ object RedBlackTree { sealed abstract class Color @@ -607,8 +607,8 @@ object RedBlackTree { newExample("Search Linked-List", """ import scala.collection.immutable.Set -import funcheck.Utils._ -import funcheck.Annotations._ +import leon.Utils._ +import leon.Annotations._ object SearchLinkedList { sealed abstract class List @@ -657,8 +657,8 @@ object SearchLinkedList { """.trim) newExample("Sum and Max", """ -import funcheck.Utils._ -import funcheck.Annotations._ +import leon.Utils._ +import leon.Annotations._ object SumAndMax { sealed abstract class List diff --git a/web/app/models/LeonConsole.scala b/web/app/models/LeonConsole.scala index 76ef94140165f917db1a37c4320acb8f5bf64f0e..eac20b8c5af077994d337200ed66eb5b7c0318af 100644 --- a/web/app/models/LeonConsole.scala +++ b/web/app/models/LeonConsole.scala @@ -20,6 +20,8 @@ import leon.{LeonContext, Settings, Reporter} import leon.plugin.{TemporaryInputPhase, ExtractionPhase} import leon.verification.AnalysisPhase +import scala.tools.util.PathResolver + object LeonConsole { def open: Promise[(Iteratee[JsValue,_],Enumerator[JsValue])] = { diff --git a/web/lib/cafebabe_2.9.2-1.2.jar b/web/lib/cafebabe_2.9.2-1.2.jar new file mode 120000 index 0000000000000000000000000000000000000000..57d96b33e6c9a29cbab7d616b007d4f2121f6e66 --- /dev/null +++ b/web/lib/cafebabe_2.9.2-1.2.jar @@ -0,0 +1 @@ +../../unmanaged/64/cafebabe_2.9.2-1.2.jar \ No newline at end of file diff --git a/web/lib/scalaz3.jar b/web/lib/scalaz3.jar new file mode 120000 index 0000000000000000000000000000000000000000..ee09a7a2d62e155c2dcfa2b86795309ff5d7b7a1 --- /dev/null +++ b/web/lib/scalaz3.jar @@ -0,0 +1 @@ +../../unmanaged/64/scalaz3.jar \ No newline at end of file diff --git a/web/public/stylesheets/leon.css b/web/public/stylesheets/leon.css index b480006d208144b2d02704625f4aa24427d28181..c60ac99045f25878587d85706faf7a3ad7ac0e32 100644 --- a/web/public/stylesheets/leon.css +++ b/web/public/stylesheets/leon.css @@ -143,7 +143,7 @@ td.date { div#codebox { border-style: none; - background-color: rgba(255,255,255,0.5); + background-color: rgba(255,255,255,0.8); border: 1px dashed #333; width: 700px; height: 450px;