From 202352d966104dc1579da939b6665a2f137dfea4 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 11 Dec 2012 15:49:09 +0100
Subject: [PATCH] Works on web with hardcoded classPath **TO FIX**
---
src/main/scala/leon/Settings.scala | 7 +++-
.../scala/leon/plugin/ExtractionPhase.scala | 8 ++++-
web/app/examples/VerificationExamples.scala | 36 +++++++++----------
web/app/models/LeonConsole.scala | 2 ++
web/lib/cafebabe_2.9.2-1.2.jar | 1 +
web/lib/scalaz3.jar | 1 +
web/public/stylesheets/leon.css | 2 +-
7 files changed, 36 insertions(+), 21 deletions(-)
create mode 120000 web/lib/cafebabe_2.9.2-1.2.jar
create mode 120000 web/lib/scalaz3.jar
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 9aa0c57ac..43b595df6 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 fdc271d53..72064330b 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 e2027c62a..60a053b84 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 76ef94140..eac20b8c5 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 000000000..57d96b33e
--- /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 000000000..ee09a7a2d
--- /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 b480006d2..c60ac9904 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;
--
GitLab