| If you send me (off-list) your proofs, I can have a look, and that may help us optimize the encoding for the back-end provers. My hunch is that it's not just arithmetic but rather a combination, such as function application and arithmetic. Breaking down complex proofs into smaller steps will in general help speed up proof checking, as may introducing local definitions for abstracting complex subformulas. A trivial way to reduce wall-clock time is to explicitly indicate the relevant back-end if SMT (which is called first) doesn't succeed so that you don't have to wait for it to time out. But my advice would be not to exaggerate: this is a rabbit hole that's probably not worth exploring. Not sure I understand your last question, but perhaps you systematically invoke the prover on the entire module (from the command line). The Toolbox GUI really helps for launching the prover on individual obligations, but you can also run it from the command line using tlapm --toolbox m n where m and n denote the interval of lines in the module that you'd like the prover to check. 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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/29233EBE-DCFE-40F5-B65A-031F96782E27%40gmail.com. |