[isabelle-dev] \nexists

Joachim Breitner breitner at kit.edu
Mon Jul 18 11:05:42 CEST 2016


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.



Dr. rer. nat. Joachim Breitner
Wissenschaftlicher Mitarbeiter
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160718/79d6664b/attachment.sig>

More information about the isabelle-dev mailing list