[tlaplus]

["C. M. Sperberg-McQueen" <cmsmcq@xxxxxxxxxxxxxxxxx>]

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.