[isabelle-dev] NEWS

[Jasmin Christian Blanchette]

Am 29.10.2010 um 19:18 schrieb Tobias Nipkow:

> Or timeout is universally in seconds, as an integer w/o unit.
> Simpler or more flexible. I have no strong view.

I would like to give quickly the rationale for "10 s" or "500 ms".

While seconds usually are enough, there are cases where they aren't. E.g. you probably don't want to give more than 500 ms to the termination prover in Nitpick, because it's only one of many components that's used.

At Trolltech, when designing the Qt APIs, we usually standardized on milliseconds. With version Qt 4.5, for the first time, we needed microseconds, which made a real mess of things. The lesson I learned from all of this is to always explicitly encode the units. The ML "Time.time" type does this right. At the user level, one could say that "10" means "10 s" by default, but even that is not always so readable.

Jasmin