Give --resource-limit a default value

[keyboardDrummer]

The default value should be calibrated to target a particular maximum duration of verification, for some common type of hardware. I don't know what duration we should target, but I imagine something in the range 1-30 seconds.

The calibration should come in the form of a script that outputs what a good default --resource-limit is

[robin-aws]

Agreed a default value is a good idea, but it should be a fixed value. The point of encouraging --resource-limit is that the metric is deterministic and isn't influenced by hardware type or how much load is on the hardware. Faster hardware may run out of time faster, but still get the same answer as slower hardware. The motivation is reducing brittleness rather than preventing runaway builds: that's what --verification-time-limit is for.

Based on the user feedback we've got, and our own experience building DafnyStandardLibraries, it seems like 1M would be a good default value.

If we do set a default value, I think we need a way to opt in to no resource limit, something like --resource-limit None. And we may want to go a little further and prompt the user to try this mode if they get a verification failure because of running out of resources, since it's usually useful to figure out if your code can verify at all first, then worry about making it verify efficiently enough. Perhaps by temporarily adding {:resource_limit "None"} to the enclosing declaration?

[keyboardDrummer]

Agreed a default value is a good idea, but it should be a fixed value. The point of encouraging --resource-limit is that the metric is deterministic and isn't influenced by hardware type or how much load is on the hardware.

I agree, that's also what I'm proposing.

However, we could raise the default in the future, if solvers or hardware improves so that solver resources are consumed faster. I'm suggesting adding a script to calibrate the right default value for --resource-limit.

[robin-aws]

Ah gotcha. The 1M threshold is definitely only based on anecdotes and empirical evidence on a fairly small sample, on a mix of hardware. I like the idea of something like "the butterfly effect can frequently multiply verification cost, so let's pick a reasonable tolerable maximum verification time limit like 20 seconds and set the limit to effectively half of that, so we're not typically immediately broken by a single change".