Merge branch 'codespaces_doc' of github.com:samuelchassot/stainless i…

…nto codespaces_doc

.gitignore

@@ -1,5 +1,4 @@
 # Stainless
-/bin/stainless-*
 .stainless-cache/
 .stainless.conf
 stainless.conf

.larabot.conf

@@ -1,15 +1,14 @@
 commands = [
-    "sbt -batch -Dtest-parallelism=5 test"
-    "sbt -batch -Dtest-parallelism=5 \"it:testOnly stainless.GhostRewriteSuite stainless.GenCSuite stainless.ScalacExtractionSuite stainless.LibrarySuite stainless.verification.SMTZ3VerificationSuite stainless.verification.SMTZ3UncheckedSuite stainless.verification.TerminationVerificationSuite stainless.verification.ImperativeSuite stainless.verification.FullImperativeSuite stainless.verification.StrictArithmeticSuite stainless.verification.CodeGenVerificationSuite stainless.verification.SMTCVC4VerificationSuite stainless.verification.SMTCVC4UncheckedSuite stainless.verification.PrincessVerificationSuite stainless.termination.TerminationSuite stainless.evaluators.EvaluatorComponentTest\""
+    "sbt -batch -Dtestsuite-parallelism=5 test"
+    "sbt -batch -Dtestsuite-parallelism=3 -Dtestcase-parallelism=5 \"stainless-dotty / IntegrationTest / testOnly stainless.DottyExtractionSuite stainless.GhostRewriteSuite stainless.GenCSuite stainless.LibrarySuite stainless.verification.VerificationSuite stainless.verification.UncheckedSuite stainless.verification.TerminationVerificationSuite stainless.verification.ImperativeSuite stainless.verification.FullImperativeSuite stainless.verification.StrictArithmeticSuite stainless.termination.TerminationSuite stainless.evaluators.EvaluatorComponentTest\""
 ]
 
 nightly {
   commands = [
     "sbt universal:stage"
-    "sbt -batch -Dtest-parallelism=5 test"
-    "sbt -batch -Dtest-parallelism=5 it:test"
-    "bash bin/external-tests.sh --only-scalac"
-    "bash bin/external-tests.sh --only-dotty"
+    "sbt -batch -Dtestsuite-parallelism=5 test"
+    "sbt -batch -Dtestsuite-parallelism=3 -Dtestcase-parallelism=5 it:test"
+    "bash bin/external-tests.sh"
     "sbt -batch scripted"
     "bash bin/build-slc-lib.sh"
   ]

README.md

@@ -1,14 +1,18 @@
 # Stainless [![Release][release-img]][latest-release] [![Nightly Build Status][nightly-larabot-img]][nightly-larabot-ref] [![Build Status][larabot-img]][larabot-ref] [![Gitter chat][gitter-img]][gitter-ref] [![Apache 2.0 License][license-img]][license-ref]
 
+Hosted at https://github.com/epfl-lara/stainless ; mirrored at https://gitlab.epfl.ch/lara/stainless
+
 Verification framework for a subset of the [Scala](http://scala-lang.org) programming language. See the [tutorial](https://epfl-lara.github.io/asplos2022tutorial/).
 
+Please note that Stainless does not support Scala 2 frontend anymore but only Scala 3.3. The latest release that does support Scala 2.13 frontend is the [v0.9.8.7](https://github.com/epfl-lara/stainless/releases/tag/v0.9.8.7).
+
 ## Quick start
 
 We test mostly on [Ubuntu](https://ubuntu.com/download); on [Windows](https://www.microsoft.com/eb-gb/software-download/windows10), you can get sufficient text-based Ubuntu environment by installing [Windows Subsystem for Linux](https://learn.microsoft.com/en-us/windows/wsl/install) (e.g. `wsl --install`, then `wsl --install -d ubuntu`). Ensure you have a [Java](https://openjdk.org/projects/jdk/17/) version ready (it can be headless); on Ubuntu `sudo apt install openjdk-17-jdk-headless` suffices.
 
-Once ready, [Download the latest `stainless-dotty-standalone` release](https://github.com/epfl-lara/stainless/releases) for your platform. Unzip the archive, and run Stainless through the `stainless.sh` script. Stainless expects a list of space-separated Scala files to verify but also has other [Command-line Options](https://epfl-lara.github.io/stainless/options.html).
+Once ready, [Download the latest `stainless-dotty-standalone` release](https://github.com/epfl-lara/stainless/releases) for your platform. Unzip the archive, and run Stainless through the `stainless` script. Stainless expects a list of space-separated Scala files to verify but also has other [Command-line Options](https://epfl-lara.github.io/stainless/options.html).
 
-To check if everything works, you may create a file named `HelloStainless.scala` next to the `stainless.sh` script with the following content:
+To check if everything works, you may create a file named `HelloStainless.scala` next to the `stainless` script with the following content:
 ```scala
 import stainless.collection._
 object HelloStainless {
@@ -21,7 +25,7 @@ object HelloStainless {
   }
 }
 ```
-and run `stainless.sh HelloStainless.scala`.
+and run `stainless HelloStainless.scala`.
 If all goes well, Stainless should report something along the lines:
 ```
 [  Info  ]   ┌───────────────────┐
@@ -36,11 +40,11 @@ If all goes well, Stainless should report something along the lines:
 If you see funny symbols instead of the beautiful ASCII art, run Stainless with `--no-colors` option for clean ASCII output with standardized error message format. 
 
 The release archive of Stainless only requires JDK17. In particular, it needs neither a Scala compiler nor SBT.
-It is shipped with Z3 4.8.14 and Princess. If z3 API is not found, use option `--solvers=smt-z3` to rely on the executable.
+It is shipped with Z3 4.12.2, cvc5 1.0.8 and Princess. If Z3 API is not found, use option `--solvers=smt-z3` to rely on the executable.
 
 ## SBT Stainless plugin
 
-Alternatively, one may integrate Stainless with SBT. The supported Scala versions are `3.2.0` and `2.13.6`
+Alternatively, one may integrate Stainless with SBT. The supported Scala versions is `3.3.3`.
 To do so, download [sbt-stainless](https://github.com/epfl-lara/stainless/releases), and move it to the directory of the project.
 Assuming the project's structure is:
 ```
@@ -70,10 +74,11 @@ these should be moved according to the above structure.
 
 Finally, the plugin must be explicitly enabled for projects in `build.sbt` desiring Stainless with `.enablePlugins(StainlessPlugin)`.
 For instance:
+
 ```scala
 ThisBuild / version := "0.1.0"
 
-ThisBuild / scalaVersion := "3.2.0"
+ThisBuild / scalaVersion := "3.3.3"
 
 lazy val myTestProject = (project in file("."))
   .enablePlugins(StainlessPlugin) // <--------
@@ -84,16 +89,15 @@ lazy val myTestProject = (project in file("."))
 
 Verification occurs with the usual `compile` command.
 
-Note that this method only ships the Princess SMT solver. Z3 and CVC4 can still be used if their executable can be found in the `$PATH`.
+Note that this method only ships the Princess SMT solver. Z3 and cvc5 can still be used if their executable can be found in the `$PATH`.
 
 ## Build and Use
 
-To start quickly, install a JVM and use a [recent release](https://github.com/epfl-lara/stainless/releases). To build the project, run `sbt universal:stage`. If all goes well, scripts are generated for Scala 3 and Scala 2 versions of the front end:
-  * `frontends/scalac/target/universal/stage/bin/stainless-scalac`
+To start quickly, install a JVM and use a [recent release](https://github.com/epfl-lara/stainless/releases). To build the project, run `sbt universal:stage`. If all goes well, scripts are generated for the front end:
   * `frontends/dotty/target/universal/stage/bin/stainless-dotty`
 
 Use one of these scripts as you would use `scalac` to compile Scala files.
-The default behavior of Stainless is to formally verify files, instead of generating JVM class files. 
+The default behavior of Stainless is to formally verify files, instead of generating JVM class files.
 See [frontends/benchmarks/verification/valid/](frontends/benchmarks/verification/valid/) and related directories for some benchmarks and
 [bolts repository](https://github.com/epfl-lara/bolts/) for a larger collection.
 More information is available in the documentation links.
@@ -136,7 +140,7 @@ Stainless is released under the Apache 2.0 license. See the [LICENSE]() file for
 
 Stainless relies on Inox to solve the various queries stemming from program verification.
 Inox supports model-complete queries in a feature-rich fragment that lets Stainless focus
-on program transformations and soundness of both contract and termination checking and uses its own reasoning steps, as well as invocations to solvers (theorem provers) [z3](https://github.com/Z3Prover/z3), [CVC4](https://cvc4.github.io/), and [Princess](http://www.philipp.ruemmer.org/princess.shtml).
+on program transformations and soundness of both contract and termination checking and uses its own reasoning steps, as well as invocations to solvers (theorem provers) [z3](https://github.com/Z3Prover/z3), [cvc5](https://cvc5.github.io/), and [Princess](http://www.philipp.ruemmer.org/princess.shtml).
 
 [latest-release]: https://github.com/epfl-lara/stainless/releases/latest
 [license-img]: https://img.shields.io/badge/license-Apache_2.0-blue.svg?color=134EA2

bin/bolts-tests.sh

@@ -3,7 +3,6 @@
 set -e
 
 TEST_DIR=$1
-FRONTEND=$2
 echo "Moving to $TEST_DIR"
 mkdir -p "$TEST_DIR"
 cd "$TEST_DIR" || exit 1
@@ -16,6 +15,6 @@ else
   cd bolts || exit 1
 fi
 
-bash ./run-tests.sh "$FRONTEND"
+bash ./run-tests.sh stainless-dotty
 
 cd ../.. || true

bin/external-tests.sh

@@ -84,14 +84,10 @@ Usage: external-tests.sh [options]
 
   -h | -help         Print this message
   --skip-build       Do not build Stainless (saves time if the build is already up-to-date).
-  --only-scalac      Run the tests for the Scalac frontend only.
-  --only-dotty       Run the tests for the Dotty frontend only.
 EOM
 }
 
 SKIP_BUILD=false
-ONLY_SCALAC=false
-ONLY_DOTTY=false
 while [[ $# -gt 0 ]]; do
   key="$1"
 
@@ -104,14 +100,6 @@ while [[ $# -gt 0 ]]; do
       SKIP_BUILD=true
       shift # past argument
       ;;
-    --only-scalac)
-      ONLY_SCALAC=true
-      shift # past argument
-      ;;
-    --only-dotty)
-      ONLY_DOTTY=true
-      shift # past argument
-      ;;
     *)    # unknown option
       usage
       exit 1
@@ -141,7 +129,7 @@ if [[ "$SKIP_BUILD" = false ]]; then
 
   echo "Publishing Stainless..."
 
-  STAINLESS_VERSION=$(sbt publishLocal | $SED -n -r 's#^.*stainless-scalac-plugin_2.12.13/([^/]+)/poms.*$#\1#p' | head -n1)
+  STAINLESS_VERSION=$(sbt publishLocal | $SED -n -r 's#^.*stainless-dotty-plugin_3.3.3/([^/]+)/poms.*$#\1#p' | head -n1)
 
   echo "Published Stainless version is: $STAINLESS_VERSION"
 else
@@ -158,11 +146,5 @@ mkdir -p "$TEST_DIR"
 
 # Stainless Actors are currently disabled: https://github.com/epfl-lara/stainless/issues/970
 # "$BIN_DIR/stainless-actors-tests.sh" "$TEST_DIR" "$STAINLESS_VERSION"
-if [[ "$ONLY_DOTTY" = false ]]; then
-  echo "Running bolts test for scalac"
-  "$BIN_DIR/bolts-tests.sh" "$TEST_DIR" "stainless-scalac"
-fi
-if [[ "$ONLY_SCALAC" = false ]]; then
-  echo "Running bolts test for dotty"
-  "$BIN_DIR/bolts-tests.sh" "$TEST_DIR" "stainless-dotty"
-fi
+echo "Running bolts test"
+"$BIN_DIR/bolts-tests.sh" "$TEST_DIR" "stainless-dotty"

bin/launcher-cygwin-noscalaz3.tmpl.sh

@@ -78,6 +78,7 @@ _canonicalize_file_path() {
 
 BASE_DIR="$( dirname "$( realpath "${BASH_SOURCE[0]}" )" )"
 Z3_DIR="$BASE_DIR/z3"
+CVC5_DIR="$BASE_DIR/cvc5"
 STAINLESS_JAR="$BASE_DIR/lib/{STAINLESS_JAR_BASENAME}"
 
 if ! [[ -r "$STAINLESS_JAR" ]]; then
@@ -87,4 +88,4 @@ fi
 
 # NOTE: $JAVA_OPTS not quoted, as it may be empty!
 # Cygpath necessary, see https://stackoverflow.com/a/16640483
-exec env PATH="$Z3_DIR:$PATH" java -cp $(cygpath -w $STAINLESS_JAR) $JAVA_OPTS stainless.Main "$@"
+exec env PATH="$CVC5_DIR:$Z3_DIR:$PATH" java -cp $(cygpath -w $STAINLESS_JAR) $JAVA_OPTS stainless.Main "$@"

bin/launcher-noscalaz3.tmpl.bat

@@ -6,5 +6,6 @@ set script_dir=%CD%
 popd
 
 set PATH=%PATH%;%script_dir%\z3
+set PATH=%PATH%;%script_dir%\cvc5
 
 java -jar %script_dir%\lib\{STAINLESS_JAR_BASENAME} %*

bin/launcher-noscalaz3.tmpl.sh

@@ -78,6 +78,7 @@ _canonicalize_file_path() {
 
 BASE_DIR="$( dirname "$( realpath "${BASH_SOURCE[0]}" )" )"
 Z3_DIR="$BASE_DIR/z3"
+CVC5_DIR="$BASE_DIR/cvc5"
 STAINLESS_JAR="$BASE_DIR/lib/{STAINLESS_JAR_BASENAME}"
 
 if ! [[ -r "$STAINLESS_JAR" ]]; then
@@ -86,4 +87,4 @@ if ! [[ -r "$STAINLESS_JAR" ]]; then
 fi
 
 # NOTE: $JAVA_OPTS not quoted, as it may be empty!
-exec env PATH="$Z3_DIR:$PATH" java -cp "$STAINLESS_JAR" $JAVA_OPTS stainless.Main "$@"
+exec env PATH="$CVC5_DIR:$Z3_DIR:$PATH" java -cp "$STAINLESS_JAR" $JAVA_OPTS stainless.Main "$@"

bin/launcher.tmpl.sh

@@ -78,6 +78,7 @@ _canonicalize_file_path() {
 
 BASE_DIR="$( dirname "$( realpath "${BASH_SOURCE[0]}" )" )"
 Z3_DIR="$BASE_DIR/z3"
+CVC5_DIR="$BASE_DIR/cvc5"
 STAINLESS_JAR="$BASE_DIR/lib/{STAINLESS_JAR_BASENAME}"
 SCALAZ3_JAR="$BASE_DIR/lib/{SCALAZ3_JAR_BASENAME}"
 JARS="$STAINLESS_JAR:$SCALAZ3_JAR"
@@ -90,4 +91,4 @@ for JAR in "$STAINLESS_JAR" "$SCALAZ3_JAR"; do
 done
 
 # NOTE: $JAVA_OPTS not quoted, as it may be empty!
-exec env PATH="$Z3_DIR:$PATH" java -cp "$JARS" $JAVA_OPTS stainless.Main "$@"
+exec env PATH="$CVC5_DIR:$Z3_DIR:$PATH" java -cp "$JARS" $JAVA_OPTS stainless.Main "$@"

bin/package-sbt-plugin.sh

@@ -6,10 +6,12 @@ if [[ $(git diff --stat) != '' ]]; then
   STAINLESS_VERSION="$STAINLESS_VERSION-SNAPSHOT"
 fi
 
+SCALA_VERSION="3.3.3"
+SCALA_LIB_VERSION="3.3.3"
 PUBLISHED_SBT_PLUGIN_DIR="$HOME/.ivy2/local/ch.epfl.lara/sbt-stainless/scala_2.12/sbt_1.0/$STAINLESS_VERSION"
-PUBLISHED_LIB_DIR="$HOME/.ivy2/local/ch.epfl.lara/stainless-library_2.13/$STAINLESS_VERSION"
-PUBLISHED_DOTTY_DIR="$HOME/.ivy2/local/ch.epfl.lara/stainless-dotty-plugin_3.2.0/$STAINLESS_VERSION"
-PUBLISHED_SCALAC_DIR="$HOME/.ivy2/local/ch.epfl.lara/stainless-scalac-plugin_3.2.0/$STAINLESS_VERSION"
+LIB_SCALA_VERSION_JAR_NAME_PART=$(echo $SCALA_LIB_VERSION | cut -d '.' -f 1)
+PUBLISHED_LIB_DIR="$HOME/.ivy2/local/ch.epfl.lara/stainless-library_$LIB_SCALA_VERSION_JAR_NAME_PART/$STAINLESS_VERSION"
+PUBLISHED_DOTTY_DIR="$HOME/.ivy2/local/ch.epfl.lara/stainless-dotty-plugin_$SCALA_VERSION/$STAINLESS_VERSION"
 
 OUTPUT="./.stainless-package-sbt-plugin"
 rm -rf "$OUTPUT" || true
@@ -41,24 +43,16 @@ info "$(tput bold)[] Preparing SBT plugin jar..."
 OUT_SBT_JAR_DIR="$OUTPUT/project/lib"
 mkdir -p "$OUT_SBT_JAR_DIR"
 cp "$PUBLISHED_SBT_PLUGIN_DIR/jars/sbt-stainless.jar" "$OUT_SBT_JAR_DIR/sbt-stainless.jar"
+OUT_DOTTY_DIR="$OUTPUT/stainless/ch/epfl/lara/stainless-dotty-plugin_$SCALA_VERSION/$STAINLESS_VERSION"
+mkdir -p "$OUT_DOTTY_DIR"
+cp "$PUBLISHED_DOTTY_DIR/jars/stainless-dotty-plugin_$SCALA_VERSION.jar" "$OUT_DOTTY_DIR/stainless-dotty-plugin_$SCALA_VERSION-$STAINLESS_VERSION.jar"
+cp "$PUBLISHED_DOTTY_DIR/poms/stainless-dotty-plugin_$SCALA_VERSION.pom" "$OUT_DOTTY_DIR/stainless-dotty-plugin_$SCALA_VERSION-$STAINLESS_VERSION.pom"
 
 info "$(tput bold)[] Preparing Stainless library jar..."
-OUT_LIB_DIR="$OUTPUT/stainless/ch/epfl/lara/stainless-library_2.13/$STAINLESS_VERSION"
+OUT_LIB_DIR="$OUTPUT/stainless/ch/epfl/lara/stainless-library_$LIB_SCALA_VERSION_JAR_NAME_PART/$STAINLESS_VERSION"
 mkdir -p "$OUT_LIB_DIR"
-cp "$PUBLISHED_LIB_DIR/srcs/stainless-library_2.13-sources.jar" "$OUT_LIB_DIR/stainless-library_2.13-$STAINLESS_VERSION-sources.jar"
-cp "$PUBLISHED_LIB_DIR/poms/stainless-library_2.13.pom" "$OUT_LIB_DIR/stainless-library_2.13-$STAINLESS_VERSION.pom"
-
-info "$(tput bold)[] Preparing Dotty plugin jar..."
-OUT_DOTTY_DIR="$OUTPUT/stainless/ch/epfl/lara/stainless-dotty-plugin_3.2.0/$STAINLESS_VERSION"
-mkdir -p "$OUT_DOTTY_DIR"
-cp "$PUBLISHED_DOTTY_DIR/jars/stainless-dotty-plugin_3.2.0.jar" "$OUT_DOTTY_DIR/stainless-dotty-plugin_3.2.0-$STAINLESS_VERSION.jar"
-cp "$PUBLISHED_DOTTY_DIR/poms/stainless-dotty-plugin_3.2.0.pom" "$OUT_DOTTY_DIR/stainless-dotty-plugin_3.2.0-$STAINLESS_VERSION.pom"
-
-info "$(tput bold)[] Preparing Scalac plugin jar..."
-OUT_SCALAC_DIR="$OUTPUT/stainless/ch/epfl/lara/stainless-scalac-plugin_3.2.0/$STAINLESS_VERSION"
-mkdir -p "$OUT_SCALAC_DIR"
-cp "$PUBLISHED_SCALAC_DIR/jars/stainless-scalac-plugin_3.2.0.jar" "$OUT_SCALAC_DIR/stainless-scalac-plugin_3.2.0-$STAINLESS_VERSION.jar"
-cp "$PUBLISHED_SCALAC_DIR/poms/stainless-scalac-plugin_3.2.0.pom" "$OUT_SCALAC_DIR/stainless-scalac-plugin_3.2.0-$STAINLESS_VERSION.pom"
+cp "$PUBLISHED_LIB_DIR/srcs/stainless-library_$LIB_SCALA_VERSION_JAR_NAME_PART-sources.jar" "$OUT_LIB_DIR/stainless-library_$LIB_SCALA_VERSION_JAR_NAME_PART-$STAINLESS_VERSION-sources.jar"
+cp "$PUBLISHED_LIB_DIR/poms/stainless-library_$LIB_SCALA_VERSION_JAR_NAME_PART.pom" "$OUT_LIB_DIR/stainless-library_$LIB_SCALA_VERSION_JAR_NAME_PART-$STAINLESS_VERSION.pom"
 
 info "$(tput bold)[] Creating archive..."
 ARCHIVE="sbt-stainless"