Is your feature request related to a problem? Please describe.
If you use the --suggest switch, the resulting suggested timeouts are rather optimistic and fragile. For instance, if a proof takes 1.9 seconds in the run that spat analysed, the suggested timeout configuration is --timeout=2 (essentially the ceiling value). Even if you run the proof always on the same machine dedicated only for proofs, times are in no way guaranteed due to different load, task scheduling, occasionally running background jobs, etc. pp. Cutting it so close may lead to random proof failures when using that configuration.
This also warrants an explanation in the documentation, so that the user is at least be made more aware of this.
Describe the solution you'd like
Suggested timeout values should have a (constant) minimum value to cater for load variations on the proofing machine and should be scaled by some percentage on the upper end. Roughly like:
Timeout_Value := (Maximum_Proof_Time (VC) + Min_Timeout) * 1.1; -- force a minimum time out and add 10% slack
For special needs such parameters could maybe also be passed on the command line to override the internal defaults.
Describe alternatives you've considered
Well, you can always do rough calculations like that manually, but this is error-prone and not user-friendly. This might be fine for "toy" projects with maybe a dozen of files, but becomes infeasible with larger project with many files.
Additional context
As a bare minimum, the proof time which was used for calculating the timeout should be added as a comment after the Proof_Switches line. That way, the user has at least an idea, how close the value to the timeout actually is. It makes no sense to increase a timeout to five seconds or so by default, if the maximum proof time is in the order of a couple of milliseconds.
Chances are, it will never ever come close to running for a whole second. It's a whole different case, if the recorded proof time is already 980 ms, then it is almost a certainty it will exceed a one second limit at some time. Right now, spat handles both cases as if they were the same.
Is your feature request related to a problem? Please describe.
If you use the
--suggestswitch, the resulting suggested timeouts are rather optimistic and fragile. For instance, if a proof takes 1.9 seconds in the run thatspatanalysed, the suggested timeout configuration is--timeout=2(essentially the ceiling value). Even if you run the proof always on the same machine dedicated only for proofs, times are in no way guaranteed due to different load, task scheduling, occasionally running background jobs, etc. pp. Cutting it so close may lead to random proof failures when using that configuration.This also warrants an explanation in the documentation, so that the user is at least be made more aware of this.
Describe the solution you'd like
Suggested timeout values should have a (constant) minimum value to cater for load variations on the proofing machine and should be scaled by some percentage on the upper end. Roughly like:
For special needs such parameters could maybe also be passed on the command line to override the internal defaults.
Describe alternatives you've considered
Well, you can always do rough calculations like that manually, but this is error-prone and not user-friendly. This might be fine for "toy" projects with maybe a dozen of files, but becomes infeasible with larger project with many files.
Additional context
As a bare minimum, the proof time which was used for calculating the timeout should be added as a comment after the Proof_Switches line. That way, the user has at least an idea, how close the value to the timeout actually is. It makes no sense to increase a timeout to five seconds or so by default, if the maximum proof time is in the order of a couple of milliseconds. Chances are, it will never ever come close to running for a whole second. It's a whole different case, if the recorded proof time is already 980 ms, then it is almost a certainty it will exceed a one second limit at some time. Right now,
spathandles both cases as if they were the same.