Docs for exceptions. Release notes

core/src/sphinx/imperative.rst

@@ -1,7 +1,7 @@
 .. _imperative:
 
-Imperative
-==========
+Imperative and Other Effects
+============================
 
 To complement the core :doc:`Pure Scala <purescala>` language, Stainless
 proposes a few extensions to that core language.
@@ -143,6 +143,7 @@ Stainless also has a ``swap`` operation in ``stainless.lang``, which is equivale
 
   def swap[@mutable T](a1: Array[T], i1: Int, a2: Array[T], i2: Int): Unit
 
+We recommend avoiding the use of arrays of mutable structures.
 
 Mutable Objects
 ---------------
@@ -163,6 +164,9 @@ Mutable case classes are behaving similarly to ``Array``, and are handled with a
 rewriting, where each field updates becomes essentially a copy of the object with
 the modified parameter changed.
 
+First class functions may accept mutable classes as declared
+type parameters, but they may not capture mutable objects.
+
 Aliasing
 --------
 
@@ -543,3 +547,21 @@ the postcondition of the top-level holds (see comment).
 
 Finally, ``return`` is also supported for local function definitions, with the same transformation.
 It is however not supported for anonymous functions.
+
+Exceptions
+----------
+
+
+As an alternative to exceptions, we recommend specifying
+appropriate preconditions for functions using `require` or
+using richer return types (e.g. `Option`, `Either`, or a
+class such as `Try`).
+
+It is possible to use `throw` to document reasons why
+certain situation would not be desirable.  However,
+stainless currently requires the `throw` to be provably
+unreachable, given the `require` specifications, so it will
+never be executed. There is no support for `try`. To use
+`throw` for such documentation purposes, it is necessary to
+use a simple exception class that extends
+`stainless.lang.Exception`.

core/src/sphinx/internals.rst

@@ -3,10 +3,6 @@
 Stainless' Internals
 ====================
 
-The main component of Stainless and the dataflow in its pipeline:
-
-.. image:: static/images/pipeline.svg
-   :width: 90%
-
-
-
+For deeper understanding of Stainless and Inox, please
+consult the code on GitHub or GitLab, as well as papers and
+PhD dissertations.

docs/RELEASE_NOTES.md

@@ -1,5 +1,14 @@
 # Release Notes
 
+## Version 0.9.8.8.7 (2024-09-15)
+
+- Scala version is now 3.5.0
+- Inox now has a solver for ground assertions based on internal evaluator (Inox #218), called `eval`
+- Opaque Forall and ensures: help higher order contracts (#1567)
+- Option `--compact` also reduces progress messages (#1573)
+- Changed CI to use GitHub actions
+- Documented a limited use of `throw`
+
 ## Version 0.9.8.8 (2024-08-22)
 
 ### Stainless frontend, library and internals