[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Re: TLAPS 1.2.1 released



Ah. Thanks a lot Stephan. The website uses _javascript_ to display the left menu and displays only the windows option when _javascript_ is disabled.


On Mon, Oct 28, 2013 at 3:35 PM, Stephan Merz <stepha...@xxxxxxxxx> wrote:
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.

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/X_NEKUzIUKg/unsubscribe.
To unsubscribe from this group and all its topics, 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.