how do I build with scalac using Leon's library?

Question

I am trying to compile my Leon code using scalac directly. Unfortunately, I was not able to properly build the Leon library on which the code depends.

For instance, I have run

scalac $(find ~/my-path/leon/library/ -name "*.scala" | xargs) Queue.scala

But this actually returns errors:

.../leon/library/collection/List.scala:81: error: missing parameter type for expanded function ((x$2) => x$2.size.$eq$eq(if (i.$less$eq(0))
  BigInt(0)
else
  if (i.$greater$eq(this.size))
    this.size
  else
    i))
  }} ensuring { _.size == (
                ^

What should be passed to scalac to avoid those errors in the library and ultimately compile my own source file?

Thank you!

This looks like a type error (or type inference error), rather than a missing library problem. What happens if you explicitly type the parameter of the `ensuring` closure? I.e. `ensuring { (x : Queue) => x.size == ...`. — Philippe, May 02 '15 at 02:29
See answer below: note that this is from the Leon library, not my code. — mdemarne, May 03 '15 at 14:11

score 3 · Answer 1 · answered May 03 '15 at 19:26

First of all, I suspect that the attempt here was to execute Leon programs, if so, there is a new option called --eval which will evaluate all ground functions (you can filter it further through --functions as usual). This should prevent issues with skeleton implementations being non-executable.

About the compilation issue: it should now be fixed in https://github.com/epfl-lara/leon/commit/3d73c6447916516d0ad56806fe0febf7b30a71ad

This was due to type-inference not being able to track types from the declared return type, through the untyped ensuring, to the body of the function. This causes Nil() to be imprecisely typed in the body, which in turn causes the type-less closure to be rejected.

Why did this work within Leon? Leon inserts a phase in the Scala compiler pipeline before type-checking to inject hints that make this inference possible (and convenient), since the pattern

def foo(a: A): B = { a match {
   case ..
   case ..
}} ensuring { .. }

is so frequent in Leon programs.

score 1 · Answer 2 · answered May 03 '15 at 14:11

Oddly enough, writing something like:

def take(i: BigInt): List[T] = { val res: List[T] = (this, i) match {
    case (Nil(), _) => Nil()
    case (Cons(h, t), i) =>
      if (i <= BigInt(0)) {
        Nil()
      } else {
        Cons(h, t.take(i-1))
      }
  }; res} ensuring { _.size == (
    if      (i <= 0)         BigInt(0)
    else if (i >= this.size) this.size 
    else                     i
  )}

...makes it clearly explicit. Scalac was not able to infer the proper parameter type, but this makes the return type of the first block explicit enough. Note however that this is not a problem using Leon directly, and that is a common syntax used throughout the Leon library, not my code.

By changing all functions as explained above I was able to compile the Leon Library - but not to run the project using normal scala syntax, since the set implementation in https://github.com/epfl-lara/leon/blob/master/library/lang/Set.scala, which is somehow not used by Leon, is missing.

score 0 · Answer 3 · answered May 04 '15 at 10:10

Following Etienne post:

That works, but we still need to implement sets in https://github.com/epfl-lara/leon/blob/master/library/lang/Set.scala. I did it that way:

package leon.lang
import leon.annotation._
import scala.collection.{ immutable => imm }

object Set {
  @library
  def empty[T] = Set[T]()
  protected[Set] def apply[T](elems: imm.Set[T]): Set[T] = Set(elems.toSeq :_*)
}

@ignore
case class Set[T](elems: T*) {
  def +(a: T): Set[T] = Set(elems.toSet + a)
  def ++(a: Set[T]): Set[T] = Set(elems.toSet ++ a.elems.toSet) //Set.trim(elems ++ a.elems) //Set((elems.toSeq ++ a.elems.toSeq).toSet.toSeq :_*)
  def -(a: T): Set[T] = Set(elems.toSet - a)
  def --(a: Set[T]): Set[T] = Set(elems.toSet -- a.elems.toSet)
  def contains(a: T): Boolean = elems.toSet.contains(a)
  def isEmpty: Boolean = this == Set.empty
  def subsetOf(b: Set[T]): Boolean = elems.toSet.forall(e => b.elems.toSet.contains(e))
  def &(a: Set[T]): Set[T] = Set(elems.toSet & a.elems.toSet)
}

Unfortunately this cannot be used directly as is in Leon:

[ Error  ] 8:31: Scala's Set API is no longer extracted. Make sure you import leon.lang.Set that defines supported Set operations.
         protected[Set] def apply[T](elems: imm.Set[T]): Set[T] = Set(elems.toSeq :_*)
                                     ^^^^^^^^^^^^^^^^^

But it works fine for compiling with scalac and running with scala using:

scalac $(find ~/my-path/leon/library/ -name "*.scala" | xargs) Queue.scala

Anyway, if --eval does the trick, let's just use it!

Thank you!

Note that https://github.com/epfl-lara/leon/commit/48c1d6d3a6e67a5f7ddb6cd14085781a1eab5578 now implements skeleton APIs of Set/Map by falling back to Scala sets and maps. This should allow you to compile and execute Leon programs using Scalac. — Etienne Kneuss, May 05 '15 at 12:38

how do I build with scalac using Leon's library?

3 Answers3