Re: TLAPS 1.2.1 released

[freder...@xxxxxxxxxxx]

Le vendredi 13 septembre 2013 16:18:04 UTC+2, Damien Doligez a écrit :
> 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.

It would be nice. I have spent several hours to compile eveything. And I
still have problems with a "smt3" that is not found

By the way may I suggest that a combined release with batteries included
could help the end user. I mean toolbox, tlaps end so on