Re: [tlaplus]

[Stephan Merz <stephan.merz@xxxxxxxxx>]

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 <cmsmcq@xxxxxxxxxxxxxxxxx> 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
> 
> -- 
> 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/875y734swm.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/1196339C-162E-456B-849C-AA1F38B29B55%40gmail.com.