Re: [tlaplus] JavaNullPointerException on Prove Step or Module

I have good news and bad news. The good news is that the interface to the prover has apparently begun working as it should. The bad news is that the interface appears to be working as it should, I have no idea what fixed it, and I now have no way to reproduce the problem I was having.

!ENTRY org.eclipse.core.jobs 4 2 2023-06-25 20:13:58.658
!MESSAGE An internal error occurred during: "Prover Launch".
!STACK 0
java.lang.NullPointerException
at org.lamport.tla.toolbox.tool.prover.ui.util.ProverHelper.prepareTreeForProverLaunch(ProverHelper.java:630)
at org.lamport.tla.toolbox.tool.prover.ui.util.ProverHelper$1.run(ProverHelper.java:560)
at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:2292)
at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:2317)
at org.lamport.tla.toolbox.tool.prover.ui.util.ProverHelper.prepareModuleForProverLaunch(ProverHelper.java:571)
at org.lamport.tla.toolbox.tool.prover.job.ProverJob.run(ProverJob.java:354)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)

This afternoon, right-clicking on the statement of a theorem and selecting TLA Proof Manager / Prove Step or Module no longer produces a popup message reporting a null pointer exception; instead, a pane opens on the right with a tab labeled Interesting Obligations for [modulename] and a tab labeled Console. The Interesting Obligations tab reports that

The main event of potential relevance between the failure of this morning and the success of this afternoon is that my machine shut itself down when the battery ran down, and I rebooted. It seems unlikely that between 25 June when I first attempted to use the proof system and today, this is the first time I've rebooted, but it is possible -- in which case it may be something as simple as an updated PATH or something similar.

On Thursday, July 6, 2023 at 7:34:12 AM UTC-6 Stephan Merz wrote:

Have you been able to make progress on this issue? Is there some message in the TLAPM console (in the Toolbox) that could help you identify what the problem is?

Stephan

> On 1 Jul 2023, at 16:06, C. M. Sperberg-McQueen wrote:
>
>
> On Jun 26, 2023, Stephan Merz wrote:
>
>> 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?
>
> Thank you. My apologies for the delay in my reply.
>
> Yes, issuing that command from the command line elicits what looks (to
> my untutored eye) like a normal report of an attempt (failed, in this
> case) to prove the theorem stated on the lines indicated. From that I
> infer that the proof system has been installed successfully, but that
> there is some issue in the interface between the toolbox and the proof
> system.
>
> If there are other tests I can run, I'll be happy to run them, though it
> may take me some days to do so.
>
> --
> C. M. Sperberg-McQueen
> Black Mesa Technologies LLC
> http://blackmesatech.com

Re: [tlaplus] JavaNullPointerException on Prove Step or Module - problem persisted but has now vanished