search

HeisenbugLtd / spat

SPARK Proof Analysis Tool
https://github.heisenbug.eu/spat/
Do What The F*ck You Want To Public License
15 stars 4 forks source link

Emit warning if proof times do not match? #25

Closed Jellix closed 4 years ago

Jellix commented 4 years ago

While #22 is now documented under tool limitations it could be nice to issue a warning to the user if such data is encountered (i.e. the times reported in the file and the summed proof times vastly differ and most proof times are 0.0 s).

Describe the solution you'd like Emit a text like "Warning: Data seems to be from a non-pristine run, timing results will be inaccurate." to notify the user of the issue.

Additional context If the tool is used in "iterative proof mode" (see README), the additional warning may be more disturbing than helpful. Making the warning optional is pointless (as the user would actively need to enable it), forcing the user to say they do not want such warnings on each run could be annoying, too...

Jellix commented 4 years ago

I set it to wontfix for now, as pros and cons are not clear. It's a documented issue that can be used advantageously, so I am not certain if it's worth the effort to try to detect this condition to spit out a warning, just so that the user can ignore it.