[C. M. Sperberg-McQueen]

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

[Stephan Merz]

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

> --
> 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/875y734swm.fsf%40blackmesatech.com.

[C. M. Sperberg-McQueen]

Sorry to be so slow replying - my work on this was interrupted by external events.

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.

I did not find any file containing anything I recognize as a TLAPM console, but eventually found the Jetty log in ~/.tlaplus/.metadata/.log, which contains the following, which appears to be reflecting the problem I had:

!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)

Similar log messages appear for repeated attempts to run the prover from within the toolbox, up to and including this morning.

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

    THEOREM BadRange

        OBVIOUS

cannot be proved by Zenon, Isabelle, or SMT, which is not surprising since the formula named BadRange is not in fact correct.  For what it's worth, my attempt to formulate a true claim about the model is also not proved, but that is also to be expected. 

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.  

Thank you for your help.  I'm now in a position to continue with my original goal of learning a little bit about TLA+ and the proof system.

--C. M. Sperberg-McQueen

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