Re: [isabelle-dev] Spike in isatest performance charts
On Sun, 5 Sep 2010, Tjark Weber wrote: On Fri, 2010-09-03 at 15:06 +0200, Makarius wrote: When composing log messages it is important do this from the perspective of someone who needs to figure out problems many months/years later, and needs to understand what was truely happening at some point. tuned Yes, of course. This is our internal jargon word, for saying that nothing really significant has changed. (No semantic change, no real structural change.) This is important information. A better counter example is fixed bug, because it looks like it addresses a significant issue without saying what it was. (And very often a perceived bug is actually an important feature.) Just a few days ago I was again standing before an ancient changeset that claimed to have fixed a bug, but it was otherwise unclear. So I had to guess at the greater context. Luckily such bad log entries are relatively rare. Makarius ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spike in isatest performance charts
Does it mean it's from that changeset? changeset: 39036:dff91b90d74c user:blanchet date:Thu Sep 02 11:29:02 2010 +0200 files: src/HOL/HOL.thy src/HOL/Hilbert_Choice.thy src/HOL/SAT.thy src/HOL/Sledgehammer.thy src/HOL/Tools/Sledgehammer/clausifier.ML description: use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd; this *really* speeds up things -- HOL now builds 12% faster on my machine I know this temptation to announce things on the log only too well. Empirically, the reality is much harder. When composing log messages it is important do this from the perspective of someone who needs to figure out problems many months/years later, and needs to understand what was truely happening at some point. (Not so much what the author thought he was doing, or when the author went on vacation etc.) Changelogs are neither NEWS nor personal Blog entries. And public mailing lists are not the best place to criticize your colleagues' writing style. Jasmin ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spike in isatest performance charts
On Sat, 4 Sep 2010, Jasmin Christian Blanchette wrote: When composing log messages it is important do this from the perspective of someone who needs to figure out problems many months/years later, and needs to understand what was truely happening at some point. And public mailing lists are not the best place to criticize your colleagues' writing style. The above is really the one main purpose of the whole history. You can read it as criticism if you want, but it does not change the fact. It is very important to report faithfully what has been done, and what is the current state of information. No promises, not future plans here, no excuses about failed attempts -- this happens routinely even to myself. Extra bonus points are for formal references backwards using changeset ids -- some Mercurial browsing tools turn them into hyperlinks. Makarius ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spike in isatest performance charts
On Fri, 2010-09-03 at 15:06 +0200, Makarius wrote: When composing log messages it is important do this from the perspective of someone who needs to figure out problems many months/years later, and needs to understand what was truely happening at some point. tuned Regards, Tjark ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Spike in isatest performance charts
Today's isatest indicates a significant drop in performance: http://isabelle.in.tum.de/devel/stats/at-poly/HOL-Metis_Examples.png http://isabelle.in.tum.de/devel/stats/mac-poly-M4/HOL-Metis_Examples.png http://isabelle.in.tum.de/devel/stats/mac-poly-M8/HOL-Metis_Examples.png Makarius ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spike in isatest performance charts
Am 03.09.2010 um 13:37 schrieb Makarius: Today's isatest indicates a significant drop in performance: http://isabelle.in.tum.de/devel/stats/at-poly/HOL-Metis_Examples.png http://isabelle.in.tum.de/devel/stats/mac-poly-M4/HOL-Metis_Examples.png http://isabelle.in.tum.de/devel/stats/mac-poly-M8/HOL-Metis_Examples.png I added definitional CNF to Metis yesterday, which had a positive effect on HOL and a neutral effect on the 1600 or so successful goals from the Judgement Day suite. I'll revert this and reintroduce it if and when it can be done without harming Metis_Examples (and other apps). (In fact, Larry now suggested I avoid clausification altogether, which I will investigate in the coming months.) Thanks for spotting this and letting us know! Jasmin ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
