TLAPS 1.2.1 released

[Damien Doligez <damien....@xxxxxxxx>]

Dear TLA+ users,

We have the pleasure of introducing a new release of TLAPS: version 1.2.1.

It is available as usual at:
  http://tla.msr-inria.inria.fr/tlaps/content/Download.html

Here are the main changes from version 1.1.1:

- many changes and improvements to the SMT back-ends
- addition of SMT to the default list of back-end provers
- new back-end pragmas: AllProvers[T], AllSMT[T], AllIsa[T]
- new library files with theorems on functions and finite sets (experimental)
- speed improvements in the handling of multi-module specifications
- removal of the (unsound) Cooper back-end
- addition of a back-end for using TPTP-based first-order provers (experimental)
- new option "--stretch <n>" to globally change all the timeouts on a given run
- various bug fixes

Note that we had to change the SMT back-ends to remove some soundness
bugs. This means that some of your proofs may not work any more. In that
case, you should try Z3 instead of the default CVC3, or decompose the
failing steps into more detailed proofs.

On some Linux machines, the binaries may fail with this error message:
  libc.so.6: version `GLIBC_2.15' not found
In this case, you will have to update your Linux or recompile from source.
If there is enough demand, we will provide binaries for these machines.

Thanks for your support and have fun with TLA+

-- Damien Doligez for the TLA+ team