как мне построить с помощью scalac, используя библиотеку Леона?

Во-первых, я подозреваю, что здесь была попытка выполнить программы Леона, если это так, то есть новая опция, называемая --eval, которая будет оценивать все наземные функции (вы можете фильтровать ее дальше через --functions, как обычно). Это должно предотвратить проблемы с неисполняемыми реализациями скелета.

О проблеме компиляции: теперь она должна быть исправлена ​​в https://github.com/epfl-lara/leon/commit/3d73c6447916516d0ad56806fe0febf7b30a71ad

Это произошло из-за того, что вывод типа не мог отслеживать типы от объявленного возвращаемого типа через нетипизированный ensuring до тела функции. Это приводит к тому, что Nil() неточно печатается в теле, что, в свою очередь, приводит к отклонению закрытия без типа.

Почему это сработало в Леоне? Леон вставляет фазу в конвейер компилятора Scala перед проверкой типов, чтобы ввести подсказки, которые делают этот вывод возможным (и удобным), поскольку шаблон

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

так часто встречается в программах Леона.

Как ни странно, пишет что-то вроде:

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
  )}

... делает это явно явным. Scalac не смог вывести правильный тип параметра, но это делает возвращаемый тип первого блока достаточно явным. Обратите внимание, однако, что это не проблема при использовании Leon напрямую, и это общий синтаксис, используемый во всей библиотеке Leon, а не в моем коде.

Изменив все функции, как описано выше, я смог скомпилировать библиотеку Leon, но не запустить проект с использованием обычного синтаксиса scala, поскольку реализация set в https://github.com/epfl-lara/leon/blob/master/library/lang/Set.scala, который как-то не используется Леоном, отсутствует.

Следующий пост Этьена:

Это работает, но нам все еще нужно реализовать наборы в https://github.com/epfl-lara/leon/blob/master/library/lang/Set.scala. Я сделал это так:

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)
}

К сожалению, это нельзя использовать напрямую, как в Леоне:

[ 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 :_*)
                                     ^^^^^^^^^^^^^^^^^

Но он отлично работает для компиляции с scalac и запуска с scala с использованием:

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

В любом случае, если --eval поможет, давайте просто воспользуемся им!

Благодарю вас!