Re: [tlaplus] Re: TLAPS 1.2.1 released

[Stephan Merz <stepha...@xxxxxxxxx>]

Dear Ivan,

have you noticed the tab called "Linux" to the left of the Download pane from where the binary is available? The direct link is http://tla.msr-inria.inria.fr/tlaps/content/Download/Binaries/Linux.html. (Haven't tried it myself but pretty sure that it's got nothing to do with Cygwin.)

Stephan


On 28 Oct 2013, at 17:34, ivans...@xxxxxxxxx wrote:

> 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
> 
> -- 
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at http://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/groups/opt_out.