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

[Stephan Merz <stephan.merz@xxxxxxxxx>]

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


> On 26 Jun 2023, at 04:24, C. M. Sperberg-McQueen <cmsmcq@xxxxxxxxxxxxxxxxx> wrote:
> 
> 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.

-- 
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/B28A4EE1-D08E-4BF5-8ACA-76043863E532%40gmail.com.