Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve (scale, extend) timeout values in suggested configuration #65

Open
Jellix opened this issue Oct 17, 2020 · 0 comments
Open

Improve (scale, extend) timeout values in suggested configuration #65

Jellix opened this issue Oct 17, 2020 · 0 comments
Assignees
Labels
documentation Improvements or additions to documentation enhancement New feature or request
Milestone

Comments

@Jellix
Copy link
Member

Jellix commented Oct 17, 2020

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.

@Jellix Jellix added documentation Improvements or additions to documentation enhancement New feature or request labels Oct 17, 2020
@Jellix Jellix added this to the V2.0.0 milestone Oct 17, 2020
@Jellix Jellix self-assigned this Oct 17, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
documentation Improvements or additions to documentation enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

1 participant