[tlaplus] after installation of tlaps, "Prove Step or Module" fails with Java NullPointerException

["C. M. Sperberg-McQueen" <cmsmcq@xxxxxxxxxxxxxxxxx>]

Greetings.  I am attempting to learn a bit about TLA+ and its proof
system.  To this end, I have installed the TLA+ Toolbox (twice, because
the Flatpak version does not have pdflatex installed and cannot see the
one that I have installed) and done a very few exercises.

Today I followed the instructions at

  https://tla.msr-inria.inria.fr/tlaps/content/Download/Binaries/Linux.html

to install TLAPS.  The installation process gave a few progress reports,
said it was running a self-test, reported no errors, said it was done,
and advised me to add /usr/local/lib/tlaps to the Toolbox preferences,
which I did (except that the GUI for adding a path ends the path with a
slash, so what I have is /usr/local/lib/tlaps/).

Then I right-clicked on a THEOREM statement in a model, selected TLA
Proof Manager / Prove Step or Module, and got a dialog box reporting an
error; the 'Details' button tells me

    An internal error occurred during: "Prover Launch".
    java.lang.NullPointerException

I restarted the Toolbox, but the error persists.

Any advice?  
-- 
C. M. Sperberg-McQueen
Black Mesa Technologies LLC
http://blackmesatech.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/87cz1jc5ea.fsf%40blackmesatech.com.