Add Rosette 4.0 release notes.

jamestiotio · Mar 4, 2021 · dcdc60c · dcdc60c
1 parent 723cd8a
commit dcdc60c
Show file tree

Hide file tree

Showing 2 changed files with 24 additions and 3 deletions.
diff --git a/NOTES.md b/NOTES.md
@@ -1,5 +1,26 @@
 # Release Notes
 
+## Version 4.0
+
+This is a major release with significant changes to the language and the runtime.  Rosette 4.0 is *not backward compatible* with Rosette 3.x. But porting Rosette 3.x code to Rosette 4.0 should be straightforward for most applications.
+
+This release includes the following features:
+
+- Support for assumptions (see `assume`). 
+- New symbolic evaluation core that tracks verification conditions (VCs) rather than path conditions and assertions. 
+- New symbolic reflection constructs for working with VCs, including `vc`, `with-vc`, and `clear-vc!`.
+- New symbolic reflection facilities for managing symbolic `terms`, including the option of using a garbage-collected data structure.
+- Updated `verify`, `synthesize`, `solve`, and `optimize` queries.
+- New synthesis library with efficient support for grammar holes (see `define-grammar`).
+- New list and vector operators that use bitvectors instead of integers.
+- Updates to The Rosette Guide to document the new language in detail.
+
+The following features have been removed:
+
+- The `debug` query.
+- Reflection facilities for working with path conditions and assertions: `pc`, `with-asserts`, `with-asserts-only`, `clear-asserts!`, and `asserts`.  
+- Support for CPLEX.
+
 ## Version 3.2
 
 This release includes minor updates and a new [value destructuring library].

diff --git a/README.md b/README.md
@@ -9,7 +9,7 @@ The Rosette Language
 
 The easiest way to install Rosette is from Racket's package manager:
 
-* Download and install Racket 7.0 or later from http://racket-lang.org
+* Download and install Racket 8.0 or later from http://racket-lang.org
 
 * Use Racket's `raco` tool to install Rosette:
 
@@ -19,7 +19,7 @@ The easiest way to install Rosette is from Racket's package manager:
 
 Alternatively, you can install Rosette from source:
 
-* Download and install Racket 7.0 or later from http://racket-lang.org
+* Download and install Racket 8.0 or later from http://racket-lang.org
 
 * Clone the rosette repository:
 
@@ -63,7 +63,7 @@ Alternatively, you can install Rosette from source:
 
 * The `rosette` language includes all of Racket.  This places the burden
   on the programmer to decide whether a given Racket construct (which
-  is not overriden by Rosette) is safe to use in a given context.
+  is not overridden by Rosette) is safe to use in a given context.
   Rosette provides no guarantees or checks for programs that use
   unsafe constructs.  In the best case, such a program will fail with
   an exception if a symbolic value flows to a construct that does not