Re: [tlaplus] TypeOK => TypeOK' with no other assumptions

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

The issue tracker for v2-tlapm is the one to use. Unfortunately, the transition to the new version of the PM has taken us far longer than we anticipated.

Stephan

> On 19 Feb 2018, at 13:11, tal...@xxxxxxxxx wrote:
> 
> Ah, OK. Is there a list of known issues somewhere?
> 
> I went to the tlaplug GitHub page (https://github.com/tlaplus). That pins the v2-tlapm repository, but it seems it isn't being used yet. Its README suggests https://tlaps.codeplex.com instead, but that has a "Shutdown Announcement". I also found https://github.com/tlaplus/v1-tlapm, but that has no issues (open or closed) and hasn't seen a release since Jan 2016.
> 
> (I was just curious to read the log for the fix commit)
> 
> Thanks,
> 
> 
> On Monday, February 19, 2018 at 11:02:04 AM UTC, Stephan Merz wrote:
>> Hello,
>> 
>> this is a known bug that has been fixed in the development version of TLAPS that is hopefully soon going to give rise to a new release. Indeed, you should not be using PTL for proving non-temporal (i.e., state- or action-level) proof obligations, but only for steps involving operators of temporal logic.
>> 
>> Sorry for the confusion,
>> Stephan
>> 
>> 
>>> On 19 Feb 2018, at 11:39, talex5 wrote:
>>> 
>>> Hi. I'm new to TLA+ and just tried my first proof. It appeared to work, and everything went green, but it seemed a bit too easy. After simplifying things, I ended up with this, which also goes all green:
>>> 
>>> ------------------------------- MODULE False -------------------------------
>>> 
>>> EXTENDS TLAPS
>>> 
>>> VARIABLE x
>>> 
>>> TypeOK == x = {}
>>> 
>>> THEOREM T0 ==
>>> ASSUME TypeOK
>>> PROVE  TypeOK'
>>> BY PTL DEF TypeOK
>>> 
>>> =============================================================================
>>> 
>>> Oddly, if I replace TypeOK with its definition then it no longer accepts it. It does still accept it if I remove the "DEF TypeOK" bit completely though.
>>> 
>>> Maybe I shouldn't be using "BY PTL" here, but could someone explain what this means?
>>> 
>>> This is Version 1.5.6 of 29 January 2018 and includes:
>>> - SANY Version 2.1 of 23 July 2017
>>> - TLC Version 2.12 of 29 January 2018
>>> - PlusCal Version 1.8 of 07 December 2015
>>> - TLATeX Version 1.0 of 20 September 2017
>>> 
>>> Thanks!
> 
> 
> -- 
> 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 https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.