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

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

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


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".

I restarted the Toolbox, but the error persists.

Any advice?  
C. M. Sperberg-McQueen
Black Mesa Technologies LLC

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.