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

[C. M. Sperberg-McQueen]

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

[Stephan Merz]

Can you launch the prover from the command line? Using something like

/usr/local/bin/tlapm --toolbox m n -I /usr/local/lib/tlaps/ module.tla

where module.tla is the TLA module that contains the proof and m and n are the first and last line numbers of the part of the proof that you want to check?

Stephan

> --
> 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+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/87cz1jc5ea.fsf%40blackmesatech.com.