The --line flag has proven helpful. I might whip up a quick rust program that uses the tree-sitter grammar to find all lines with terminal proofs, runs tlapm FileName.tla --line N, measures the wall clock time for each, then prints out a sorted list of the longest-running proofs.
I'm having trouble proving a goal of type \E n \in Nat : P(n). It times out every other solver before Isabelle finally catches it. So I can reduce the time by specifying BY Isa, but I would be interested in knowing whether there's a way to break it down further to speed up checking:
Andrew
On Tuesday, March 28, 2023 at 2:47:55 AM UTC-4 Stephan Merz wrote:
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
I've written some arithmetic proofs where the prover does eventually validate the proof, albeit after a fairly long wait time. In general, can one reduce proof check time by breaking down a long-running proof into smaller substeps? Is there a way to check which steps are taking a long time so you know where to focus efforts?
Thanks!
Andrew
--
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/a754d530-0927-4337-bff3-3e51e7ea5b55n%40googlegroups.com.