[isabelle-dev] \nexists

[Makarius]

On 18/07/16 11:05, Joachim Breitner wrote:
> Hi,
> 
> Am Montag, den 18.07.2016, 10:39 +0200 schrieb Lars Hupel:
>>>> - What about sessions that grow in size over time?
>>>
>>> That is indeed important, although we have just ignored it historically.
>>
>> Right. But how would we take it into account? What registers as a spike
>> in build time for a session could either be a performance regression in
>> Isabelle or growing material.
> 
> Wouldn’t that be quite obvoius from the a quick glance at the changeset
> in question?
> 
> I manually watch https://perf.haskell.org/ghc/ when I see a regression
> I apply common sense to decide whether to notify the authors, or
> whether it is genuine.
> 
> Sure, something fully automatic and reliable would be nice, but having
> numbers and graphs is still useful, even if “graph goes up →
> performance regression happened” does not hold unconditionally.

Nicely plotted graphs and for a human to inspect are indeed the most
important tool.

When we still had good physical measurements (some years ago), I used to
look at the graphs every morning, even before checking my email. And
then at the corresponding changesets to figure out what happened.

Another important application works the other way round: changes are
introduced with the intention to make some difference in performance,
and in the coming days the graph hopefully develops a noticable step
upwards or downwards.


	Makarius


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160718/25ca5bd3/attachment.sig>