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

[tal...@xxxxxxxxx]

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!