Added release notes. Minor tweads to README.md.

[ci skip]
ROS-ROBOT-SERIES · Mar 24, 2016 · 22131b0 · 22131b0
1 parent 8ed0759
commit 22131b0
Show file tree

Hide file tree

Showing 2 changed files with 87 additions and 7 deletions.
diff --git a/NOTES.md b/NOTES.md
@@ -0,0 +1,78 @@
+# Release Notes
+
+## Version 2.0
+
+This is a major release with significant features to the language and
+the symbolic evaluator.  Rosette 2.0 is *not backward compatible* with
+Rosette 1.x.
+
+This release includes the following features:
+
+- New symbolic datatypes.
+
+  - Replaced the `number?` type with `integer?` and `real?` types.
+    These datatypes are translated to the theories of integers and
+    reals if `current-bitwidth` is set to `#f`.  Otherwise, they are
+    translated to bitvectors of length `(current-bitwidth)`.
+
+   - Added the `bitvector?` datatype, which embeds the SMT theory of
+     bitvectors into Rosette.
+
+   - Added the `function?` datatype, which embeds uninterpreted
+   functions into Rosette.
+
+- New solver-aided queries.
+
+  - Changed the behavior of solver-aided queries to no longer throw
+  exceptions when a model is not found.  Instead they return an
+  `unsat?` solution.
+
+  - Changed the `solve` and `verify` queries to ensure that any
+  solution obtained with finite-precision reasoning is correct under
+  the aribitrary-precision semantics of integers and reals.
+
+  - Added the `optimize` query, which exposes Z3's optimization
+   features.
+
+- Improved implementation for the `define-synthax` form and other
+  high-level synthesis constructs.
+
+- Ported sample SDSLs to Rosette 2.0.
+
+- Updated The Rosette Guide to document the new language in detail.
+
+The following features have been removed:
+
+- Support for Kodkod and CVC4 solvers.
+
+- Support for the `enum` datatype.
+
+- Support for internal logging via `current-log-handler`.
+
+## Version 1.1
+
+- This release includes a new reader for `rosette` and `rosette/safe`
+  implemented by [bmastenbrook](https://github.com/bmastenbrook).
+
+- It also includes a fix for a bug in the evaluation of symbolic
+  boxes.  Thanks to Alan Borning for reporting it.
+
+## Version 1.0
+
+- This is the initial release of the Rosette language and Symbolic
+  Virtual Machine, as described in [PLDI'14][1] and [Onward13][2].
+
+- It includes two symbolic datatypes: `boolean?` and `number?`.
+  Assertions over numbers are translated to the theory of bitvectors.
+
+- Rosette 1.0 supports the Kodkod, Z3, and CVC4 solvers.
+
+- This release also includes the source code for three solver-aided
+  DSLs: WebSynth (web scraping by demonstration), IFC (verification
+  for secure stack machine semantics), and SynthCL (synthesis and
+  verification for an Open-CL imperative language).
+
+
+[1]: http://dl.acm.org/citation.cfm?id=2594340
+[2]: http://dl.acm.org/citation.cfm?id=2509586
+
diff --git a/README.md b/README.md
@@ -1,12 +1,12 @@
-rosette
-=======
+The Rosette Language
+====================
 
 [![Build Status](https://travis-ci.org/emina/rosette.svg?branch=refactor-ops)](https://travis-ci.org/emina/rosette)
 
 This repository includes the source code for the Rosette solver-aided host language, as well as several example
 solver-aided DSLs.
 
-### Installing Rosette
+## Installing Rosette
 
 * Download and install Racket 6.4 from http://racket-lang.org
 
@@ -30,7 +30,7 @@ solver-aided DSLs.
 
 * Copy the `z3` executable (with no filename extension) to the `rosette/bin` directory.
 
-### Executing Rosette programs
+## Executing Rosette programs
 
 * Open the target program in DrRacket (e.g., [`rosette/sdsl/fsm/demo.rkt`](https://github.com/emina/rosette/blob/master/sdsl/fsm/demo.rkt))
   and hit run!
@@ -41,7 +41,7 @@ solver-aided DSLs.
   `$ raco make <your program>`  
   `$ racket <your program>`  
 
-### Available languages
+## Available languages
 
 * Rosette ships with two languages: `#lang rosette/safe` and  `#lang rosette`.
 
@@ -67,5 +67,7 @@ solver-aided DSLs.
   incorrect semantics or cause more serious problems (e.g., data loss if 
   it writes to a file).
 
-* For more on using Rosette, see [_The Rosette Guide_](http://homes.cs.washington.edu/~emina/rosette/guide/index.html).  Rosette's internals are described in [_A lightweight symbolic
-  virtual machine for solver-aided host languages._](http://homes.cs.washington.edu/~emina/pubs/rosette.pldi14.pdf) (PLDI'14).
+* For more on using Rosette, see [_The Rosette Guide_][1].  Rosette's internals are described in [PLDI'14][2].
+
+[1]: http://emina.github.io/rosette/doc/rosette-guide/index.html
+[2]: http://dl.acm.org/citation.cfm?id=2594340