Re: TLAPS 1.2.1 released

[ivans...@xxxxxxxxx]

Where can one download linux binaries? The link here http://tla.msr-inria.inria.fr/tlaps/content/Home.html amusingly uses cygwin to get a *nix environment on windows, but doesn't provide linux binaries. 

Thanks,
Ivan 


On Friday, September 13, 2013 10:18:04 AM UTC-4, Damien Doligez wrote:
> 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