[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]


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

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

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.