Is tla+.jj up to date on github?

[Raghav Boorgapally]

Hi,

I am reading through the source code of TLA+ and trying to play with the tla2sany currently.

I see that the javacc version used is javacc 4 and it generates the parser by taking the tla+.jj file as input.

I also see that the generated parser is checked in and is modified. So, is the tla+.jj accurate representation of the whole TLA+ parsing logic? Or have the maintainers started with that and made subsequent changes to the generated java files itself?

Javacc 4 seems to use raw java data structures without generics. When I tried to generate the parser with the latest version of javacc (7.0), it generated the parser with the modern java data structures with generics. Is there any plan to move to latest javacc version?

[Leslie Lamport]

I believe that no existing parser generator can generate a parser for TLA+ in a reasonable way.  The decision was made long ago to generate it with a kludge based on javacc rather than implementing it from scratch (or on top of an existing lexer).  That kludge requires modifying one or two of the files produced by javacc.  This is documented in the tlatools/javacc/README subdirectory of the TLA+ Tools Eclipse package.

It is difficult to maintain software that is built on top of infrastructure whose authors care little whether their next release breaks applications that depend on it.  Fortunately, we can at least avoid that problem with javacc by saving and executing the version used to construct the parser. 

Leslie

[Raghav Boorgapally]

Thanks Leslie!