No detailed information from TLA+ Parser Error

[fisherm...@gmail.com]

Hi all,

   My TLA+ toolbox(Win7 64bit / Java 8u171 64 bit / TLA+ toolbox 1.5.6 x64) don't display any detailed info about Parser Errors.

   For a TLA file with no error, the toolbox can run TLC check against it successfully.

   Can anyone help?

   Thanks

Fisher

  

[Markus Kuppe]

On 20.05.2018 14:43, fisherm...@gmail.com wrote:
>    My TLA+ toolbox(Win7 64bit / Java 8u171 64 bit / TLA+ toolbox 1.5.6
> x64) don't display any detailed info about Parser Errors.
>
>    For a TLA file with no error, the toolbox can run TLC check against
> it successfully.
>

Hi,

please try a recent TLAToolbox nightly build [1]. We recently fixed [2]
an issue [3] related to the Toolbox's parse error reporting.

Thanks
Markus

[1] https://tla.msr-inria.inria.fr/tlatoolbox/ci/products/
[2]
https://github.com/tlaplus/tlaplus/commit/77f1c6964bfc9d6ce3a1638815b9830591dc8197
[3] https://github.com/tlaplus/tlaplus/issues/145

[fisherm...@gmail.com]

Hi,

  The new build works for me.

Thanks