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

[tlaplus] Re: Making PlusCal a first-class language for TLC

Thanks, Leslie!

On Tuesday, July 2, 2019 at 12:49:44 AM UTC-7, Leslie Lamport wrote:
Mea culpa.  There is no missing feature for going from error messages
to the PlusCal source of the error.  There was just a hole in my
memory.  When clicking on something takes you to the source of an
error in the TLA+ translation, holding the control key down when you
click takes you to the PlusCal source--if such a source exists.  That
includes clicking on TLA+ parsing errors and double-clicking on the
action-location line in an error trace.


On Saturday, June 29, 2019 at 3:45:24 AM UTC-7, Leslie Lamport wrote:
Hi Andrew,
Selecting a portion of the TLA+ translation and hitting F10 takes you
to the corresponding PlusCal source (if one exists).  I believe that
double clicking on a link in an error message to a line of the TLA+
translation used to take you to the PlusCal source, but bit rot seems to
have destroyed that feature.  But clicking and hitting F10 works fine.

Unfortunately, getting from the action line in an error trace to the
PlusCal source for the action isn't so nice because double-clicking on
the action line doesn't move focus to the module editor.  That should
be easy enough to fix and I hope it will be done soon, so double-clicking
on the line and hitting F10 will work.  For now, try hitting Control + F7
a few times to move the focus before hitting F10. 

It would be possible to hide under the covers the TLA+ translation and
the mapping from error locations reported by TLC to locations in the
PlusCal code.  And it might be doable in a few months if you were
willing to give up features like profiling.  But I suspect that it
would make debugging PlusCal code harder.  Rewriting TLC to work
directly on PlusCal would probably take a few person-years of effort;
I wouldn't want to hazard a guess on the number.  In any case, I will
provide no encouragement to any such project because it would
eliminate one of the purposes of PlusCal: to serve as a gateway drug
to TLA+.


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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ece9cb0b-f341-48fe-ae59-8f83365cb532%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.