Updated manually

_sources/coq.rst.txt

@@ -44,7 +44,7 @@ file:
   def test(a: BigInt, b: BigInt, c: BigInt): BigInt = {
     require(a > b && c > BigInt(0))
     c + a
-  } ensuring( _ > c + b )
+ }.ensuring( _ > c + b )
 
 Running ``stainless-scalac --coq frontends/benchmarks/coq/Arith.scala``
 generates the file ``tmp/test.v`` which contains the following Coq definition.

_sources/faq.rst.txt

@@ -75,7 +75,7 @@ I have defined a size function on my algebraic data type.
   def size(l: List) : Int = (l match {
     case Nil => 0
     case Cons(_, t) => 1 + size(t)
-  }) ensuring(_ >= 0)
+  }).ensuring(_ >= 0)
 
 Stainless neither proves nor gives a counterexample. Why?
 

_sources/genc.rst.txt

@@ -319,7 +319,7 @@ example:
     state.data(state.y) = 1
     state.stable = true
     if (state.y > 0) move()
-  }.ensuring(_ => state.stable)
+ }.ensuring(_ => state.stable)
 
 After compilation to C, we get the following function, with global declarations
 ``stable``, ``x``, ``y``, and ``data``.

_sources/ghost.rst.txt

@@ -25,7 +25,7 @@ and prove that some properties are satisfied by the program.
 
   def sort(list: List[BigInt]): List[BigInt] = {
     /* ... */
-  } ensuring { res =>
+ }.ensuring { res =>
     res.contents == list.contents &&
     isSorted(res) &&
     res.size == l.size
@@ -104,21 +104,21 @@ Case study
         val result = _take()
         msgs = msgs.tailOption.getOrElse(Nil())
         result
-      } ensuring { res =>
+     }.ensuring { res =>
         res == old(this).msgs.headOption
       }
 
       @extern @pure
       private def _take(): Option[A] = {
         Option(queue.pollFirst())
-      } ensuring { res =>
+     }.ensuring { res =>
         res == msgs.headOption
       }
 
       @extern @pure
       def isEmpty: Boolean = {
         queue.size() == 0
-      } ensuring { res =>
+     }.ensuring { res =>
         res == msgs.isEmpty
       }
     }
@@ -127,7 +127,7 @@ Case study
       @extern @pure
       def empty[A]: MsgQueue[A] = {
         MsgQueue(new ArrayDeque(), Nil())
-      } ensuring { res =>
+     }.ensuring { res =>
         res.isEmpty && res.msgs.isEmpty
       }
     }

_sources/imperative.rst.txt

@@ -212,7 +212,7 @@ properties:
   case class A(var x: Int)
   def inc(a: A): Unit = {
     a.x = a.x + 1
-  } ensuring(_ => a.x == old(a).x + 1)
+ }.ensuring(_ => a.x == old(a).x + 1)
 
 ``old`` can be wrapped around any identifier that is affected by the body. You can also use
 ``old`` for variables in scope, in the case of nested functions:
@@ -223,7 +223,7 @@ properties:
     var x = 0
     def inc(): Unit = {
       x = x + 1
-    } ensuring(_ => x == old(x) + 1)
+   }.ensuring(_ => x == old(x) + 1)
 
     inc(); inc();
     assert(x == 2)
@@ -472,7 +472,7 @@ the ``ReturnElimination`` phase. Here is a function taken from `ReturnInWhile.sc
 
       assert(false, "unreachable code")
       0
-    }.ensuring((res: Int) => res == n)
+   }.ensuring((res: Int) => res == n)
 
 After transformation, we get a recursive (local) function named ``returnWhile``
 that returns a control flow element to indicate whether the loop terminated
@@ -515,7 +515,7 @@ the postcondition of the top-level holds (see comment).
                 Proceed[Int, Unit](())
               }
           }
-        } ensuring {
+       }.ensuring {
           (cfWhile: ControlFlow[Int, Unit]) => cfWhile match {
             case Return(retValue) =>
               // we check the postcondition `retValue == n` of the top-level function
@@ -537,7 +537,7 @@ the postcondition of the top-level holds (see comment).
           assert(false, "unreachable code")
           0
       }
-    } ensuring {
+   }.ensuring {
       (res: Int) => res == n
     }
 

_sources/installation.rst.txt

@@ -12,7 +12,7 @@ General Requirement
   It suffices to have headless OpenJDK JRE 17 (e.g. one that one gets with ``apt install openjdk-17-jre-headless`` on Debian/Ubuntu).
   Make sure that ``java -version`` reports a version starting with 1.17, such as ``openjdk version "1.17`` or ``java version "1.17``.
 
-Stainless bundles Scala compiler front-end and runs it before it starts compilation. We recommend using the Scala 3 front end (originally named dotty), though Scala 2 is also available.
+Stainless bundles Scala 3 compiler front-end and runs it before it starts compilation.
 
 .. _standalone-release:
 
@@ -158,19 +158,13 @@ Note that the dependencies specified in ``stainlessExtraDeps`` must be available
 Running Code with Stainless dependencies
 ----------------------------------------
 
-Using sources:
-
-1. Clone the sources from https://github.com/epfl-lara/stainless
+If you are debugging your scala code before running stainless on it (e.g. using a simple editor with `scala-cli --watch`), you can use this workflow with stainless as well; you just need to make sure that Stainless libraries are visible to the Scala compiler.
 
-2. Create a folder to put compiled Scala objects: ``mkdir -p ~/.scala_objects``
+The simplest way is to use the release package, which contains `stainless-cli` script, a simple wrapper around `scala-cli` that adds the jar dependency on the compiled and source version of stainless library.
 
-3. Compile your code (here in ``MyFile.scala``, though you can have more than one file) while referring to the Stainless library sources: ``scalac -d ~/.scala_objects $(find /path/to/stainless/frontends/library/stainless/ -name "*.scala") MyFile.scala``
+Building a jar:
 
-4. Run your code (replace ``MyMainClass`` with the name of your main object): ``scala -cp ~/.scala_objects MyMainClass``
-
-Using jar:
-
-You can package the Stainless library into a jar to avoid the need to compile it every time:
+You can package the Stainless library into a jar like this:
 
 .. code-block:: bash
 
@@ -182,11 +176,22 @@ Add the generated Stainless library jar file when invoking the compiler with ``s
 .. code-block:: bash
 
     $ mkdir -p ~/.scala_objects
-    $ scalac -d ~/.scala_objects -cp /path/to/stainless/frontends/library/target/scala-2.13/stainless-library_2.13-X.Y.Z-A-BCDEFGHI.jar MyFile1.scala MyFile2.scala # and so on
-    $ scala -cp ~/.scala_objects:/path/to/stainless/frontends/library/target/scala-2.13/stainless-library_2.13-X.Y.Z-A-BCDEFGHI.jar MyMainClass
+    $ scalac -d ~/.scala_objects -cp /path/to/stainless/frontends/library/target/scala-3.3.3/stainless-library_3-X.Y.Z-A-BCDEFGHI.jar MyFile1.scala MyFile2.scala # and so on
+    $ scala -cp ~/.scala_objects:/path/to/stainless/frontends/library/target/scala-3.3.3/stainless-library_3-X.Y.Z-A-BCDEFGHI.jar MyMainClass
 
 where ``X.Y.Z`` is the Stainless version and ``A-BCDEFGHI`` is some hash (which can be autocompleted by the terminal).
 
+Using sources:
+
+1. Clone the sources from https://github.com/epfl-lara/stainless
+
+2. Create a folder to put compiled Scala objects: ``mkdir -p ~/.scala_objects``
+
+3. Compile your code (here in ``MyFile.scala``, though you can have more than one file) while referring to the Stainless library sources: ``scalac -d ~/.scala_objects $(find /path/to/stainless/frontends/library/stainless/ -name "*.scala") MyFile.scala``
+
+4. Run your code (replace ``MyMainClass`` with the name of your main object): ``scala -cp ~/.scala_objects MyMainClass``
+
+
 .. _smt-solvers:
 
 External Solver Binaries
@@ -264,56 +269,55 @@ Get the sources of Stainless by cloning the official Stainless repository:
 
 .. code-block:: bash
 
-  $ git clone https://github.com/epfl-lara/stainless.git
+  $ git clone --recursive https://github.com/epfl-lara/stainless.git
   Cloning into 'stainless'...
+  $ cd stainless
+  $ git submodule update --init --recursive
 
 **Run SBT**
 
 The following instructions will invoke SBT while using a stainless sub-directory to download files.
 
 .. code-block:: bash
 
-  $ cd stainless
   $ sbt universal:stage
 
 **Where to find generated files**
 
-The compilation will automatically generate the bash script ``stainless-dotty`` (and the Scala2 one ``stainless-scalac``).
+The compilation will automatically generate the bash script ``stainless-dotty``.
 
 You may want to introduce a soft-link from to a file called ``stainless``:
 
 .. code-block:: bash
 
   $ ln -s frontends/dotty/target/universal/stage/bin/stainless-dotty stainless
 
-and, for the Scala2 version of the front end,
-
-  $ ln -s frontends/scalac/target/universal/stage/bin/stainless-scalac stainless-scalac-old
 
 Analogous scripts work for various platforms and allow additional control over the execution, such as passing JVM arguments or system properties:
 
 .. code-block:: bash
 
   $ stainless -Dscalaz3.debug.load=true -J-Xmx6G --help
 
-Note that Stainless is organized as a structure of several projects. The main project lives in ``core`` while the two available frontends can be found in ``frontends/dotty`` (and ``frontends/scalac``).  From a user point of view, this should most of the time be transparent and the build command should take care of everything.
+Note that Stainless is organized as a structure of several projects. The main project lives in ``core`` while the Scala 3 frontend can be found in ``frontends/dotty``.  From a user point of view, this should most of the time be transparent and the build command should take care of everything.
 
 Build from Source on Windows 10
 -------------------------------
 
-Before following the infrequently updated instructions in this section, considering running Ubuntu on Windows 10 (through e.g. WSL) and following the instructions for Linux.
+Before following the infrequently updated instructions in this section, considering running Ubuntu on Windows 10 (through e.g. WSL2) and following the instructions for Linux.
 
 Get the sources of Stainless by cloning the official Stainless repository. You will need a Git shell for windows, e.g.  `Git for Windows <https://git-for-windows.github.io/>`_.
 On Windows, please do not use ``sbt universal:stage`` as this generates a Windows batch file which is unusable, because it contains commands that are too long for Windows.
-Instead, please use ``sbt stainless-scalac-standalone/assembly`` as follows:
+Instead, please use ``sbt stainless-dotty-standalone/assembly`` as follows:
 
 .. code-block:: bash
 
-  $ git clone https://github.com/epfl-lara/stainless.git
+  $ git clone --recursive https://github.com/epfl-lara/stainless.git
   Cloning into 'stainless'...
   // ...
   $ cd stainless
-  $ sbt stainless-scalac-standalone/assembly
+  $ git submodule update --init --recursive
+  $ sbt stainless-dotty-standalone/assembly
   // takes about 1 minutes
 
 Running Stainless can then be done with the command: ``java -jar frontends\stainless-dotty-standalone\target\scala-3.3.3\stainless-dotty-standalone-{VERSION}.jar``, where ``VERSION`` denotes Stainless version.

_sources/intro.rst.txt

@@ -70,7 +70,7 @@ precondition does hold. A simple example:
     } else {
       n * factorial(n - 1)
     }
-  } ensuring(res => res >= 0)
+ }.ensuring(res => res >= 0)
 
 Stainless generates a ``postcondition`` verification condition for the above
 function, corresponding to the predicate parameter to the ``ensuring``
@@ -128,7 +128,7 @@ can be shown terminating as follows:
   def M(n: BigInt): BigInt = {
     decreases(stainless.math.max(101 - n, 0))
     if (n > 100) n - 10 else M(M(n + 11))
-  } ensuring (_ == (if (n > 100) n - 10 else BigInt(91)))
+ }.ensuring(_ == (if (n > 100) n - 10 else BigInt(91)))
 
 
 It is also possible to add a pre-condition (``require(...)``) *before* ``decreases``.

_sources/laws.rst.txt

@@ -429,7 +429,7 @@ into methods with explicit postconditions.
      @abstract
      def law_associativity$0(x$109: A$85, y$25: A$85, z$11: A$85): Boolean = {
        <empty tree>[Boolean]
-     } ensuring {
+    }.ensuring {
        (res$82: Boolean) => res$82 && this.law_associativity$2(x$109, y$25, z$11)
      }
    }
@@ -448,7 +448,7 @@ into methods with explicit postconditions.
      @abstract
      def law_leftIdentity$0(x$110: A$86): Boolean = {
        <empty tree>[Boolean]
-     } ensuring {
+    }.ensuring {
        (res$77: Boolean) => res$77 && this.law_leftIdentity$1(x$110)
      }
 
@@ -461,14 +461,14 @@ into methods with explicit postconditions.
      @abstract
      def law_rightIdentity$0(x$111: A$86): Boolean = {
        <empty tree>[Boolean]
-     } ensuring {
+    }.ensuring {
        (res$80: Boolean) => res$80 && this.law_rightIdentity$2(x$111)
      }
 
      @law
      def law_associativity$1(x$112: A$86, y$26: A$86, z$12: A$86): Boolean = {
        this.law_associativity$2(x$112, y$26, z$12) && refineLaw$0[A$86](x$112, y$26, z$12)
-     } ensuring {
+    }.ensuring {
        (res$84: Boolean) => res$84 && this.law_associativity$2(x$112, y$26, z$12)
      }
    }
@@ -483,22 +483,22 @@ into methods with explicit postconditions.
      @derived(law_leftIdentity$0)
      def law_leftIdentity$2(x$119: BigInt): Boolean = {
        true
-     } ensuring {
+    }.ensuring {
        (res$84: Boolean) => this.law_leftIdentity$1(x$119)
      }
 
      @law
      def law_rightIdentity$1(x$115: BigInt): Boolean = {
        someProof$0
-     } ensuring {
+    }.ensuring {
        (res$79: Boolean) => res$79 && this.law_rightIdentity$2(x$115)
      }
 
      @law
      @derived(law_associativity$0)
      def law_associativity$2(x$120: BigInt, y$29: BigInt, z$13: BigInt): Boolean = {
        true
-     } ensuring {
+    }.ensuring {
        (res$85: Boolean) => this.law_associativity$1(x$120, y$29, z$13)
      }
    }
@@ -539,7 +539,7 @@ There are a few things going on here:
      @abstract
      def law_associativity$0(x$109: A$85, y$25: A$85, z$11: A$85): Boolean = {
        <empty tree>[Boolean]
-     } ensuring {
+    }.ensuring {
        (res$82: Boolean) => res$82 && this.law_associativity$2(x$109, y$25, z$11)
      }
 
@@ -556,7 +556,7 @@ There are a few things going on here:
      @law
      def law_associativity$1(x$112: A$86, y$26: A$86, z$12: A$86): Boolean = {
        this.law_associativity$2(x$112, y$26, z$12) && refineLaw$0[A$86](x$112, y$26, z$12)
-     } ensuring {
+    }.ensuring {
        (res$84: Boolean) => res$84 && this.law_associativity$2(x$112, y$26, z$12)
      }
 
@@ -572,7 +572,7 @@ There are a few things going on here:
      @law
      def law_rightIdentity$1(x$115: BigInt): Boolean = {
        someProof$0
-     } ensuring {
+    }.ensuring {
        (res$79: Boolean) => res$79 && this.law_rightIdentity$2(x$115)
      }
 
@@ -590,7 +590,7 @@ There are a few things going on here:
      @derived(law_leftIdentity$0)
      def law_leftIdentity$2(x$119: BigInt): Boolean = {
        true
-     } ensuring {
+    }.ensuring {
        (res$84: Boolean) => this.law_leftIdentity$1(x$119)
      }
 

_sources/neon.rst.txt

@@ -87,7 +87,7 @@ answer this question, we need to have a look at the definition of the
   def ++(that: List[T]): List[T] = (this match {
     case Nil()       => that
     case Cons(x, xs) => Cons(x, xs ++ that)
-  }) ensuring { res => /* ... */ }
+  }).ensuring { res => /* ... */ }
 
 Note that the implementation of ``++`` is recursive in its first
 argument ``this`` but *not* in its second argument ``that``.  This is
@@ -292,7 +292,7 @@ verification conditions for postconditions, while ``check``'s are.
     def foo(): Unit = {
       assert(b1) // verification condition: b1
       check(b2)  // verification condition: b1 ==> b2
-    }.ensuring(_ => b3) // verification condition b2 ==> b3 (b1 might not be visible to the solver)
+   }.ensuring(_ => b3) // verification condition b2 ==> b3 (b1 might not be visible to the solver)
 
 
 .. _induction:
@@ -831,7 +831,7 @@ the rationality and positiveness properties are correctly preserved:
     def +(that: Rational): Rational = {
       require(isRational && that.isRational)
       Rational(n * that.d + that.n * d, d * that.d)
-    } ensuring { res =>
+   }.ensuring { res =>
       res.isRational &&
       (this.isPositive == that.isPositive ==> res.isPositive == this.isPositive)
     }
@@ -844,7 +844,7 @@ multiplication in a similar fashion:
     def *(that: Rational): Rational = {
       require(isRational && that.isRational)
       Rational(n * that.n, d * that.d)
-    } ensuring { res =>
+   }.ensuring { res =>
       res.isRational &&
       (res.isNonZero  == (this.isNonZero && that.isNonZero)) &&
       (res.isPositive == (!res.isNonZero || this.isPositive == that.isPositive))
@@ -916,7 +916,7 @@ induction on ``this`` inside the postcondition as follows:
         case Empty()       => Rational(0, 1)
         case Cons(x, w, m) => if (xs contains x) w + m(xs) else m(xs)
       }
-    } ensuring { res =>
+   }.ensuring { res =>
       res.isPositive because {
         this match {
           case Empty()       => trivial