Re: [tlaplus] Re: Error launching TLAPS on SimpleMath.tla and Bug Tracker Link broken

Hi Michael,

thanks for reporting this. No idea why the TLAPS parser get confused by this, even more so in a comment. Could you please file an issue at https://github.com/tlaplus/tlapm/issues?

Regards,

Stephan

On 19 Nov 2020, at 13:37, Michael Leuschel <michael.leuschel@xxxxxxxxx> wrote:

Hi,

I think I found the problem:, line 76 of SimpleMath.tla contains a comment that TLAPS does not seem to like
(*{a, b} \in {{a, b}, c, {d, e}}*)

Greetings,
Michael

On 19 Nov 2020, at 13:33, Michael Leuschel <michael.leuschel@xxxxxxxxx> wrote:

Hi,

I just downloaded and installed TLAPS 1.4.5 on macOS Mojave using the latest TLA+ Toolbox 1.7.0.
I wanted to try out TLAPS on some simple maths theorems and chose SimpleMath.tla (that comes with TLC, I think).
However, there was the error message below.
When clicking on the Link to submit the bug report and then clicking on “Bug tracker for TLAPS/tlapm" I get an error “requested URL was not found”.
Hence my message to this group, maybe somebody knows what is happening.

I was able to start TLAPS for the DieHard.tla example (but it has not theorems).

Greetings,
Michael

<Screenshot 2020-11-19 at 13.23.59.png>

<Screenshot 2020-11-19 at 13.31.39.png>

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/F828AFD2-EAD5-460B-9B57-08762EB87D92%40gmail.com.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CF71B92D-1ED5-4D0B-ADA4-A30D0C411B3B%40gmail.com.