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] Recent instabilities of HOL-Decision_Procs
On Wed, 1 Sep 2010, Johannes Hölzl wrote: Am Mittwoch, den 01.09.2010, 15:40 +0200 schrieb Makarius: For some week or so there are sparadic failures of HOL-Decision_Procs like this: [..] The special things about the approximation method are: * uses reflection (i.e. the generated code as an oracle) * probably the only user of large ML-integers and division * long running proofs Is it possible to get a more detailed exception trace? There is some chance that it is due to large ML integers in the parallel setting -- this is a pre-5.4 version of Poly/ML where arbitrary precision arithmetic has been changed significantly. (It can optionally use GNU MP, although I did not compile it into that particular binary, IIRC.) The failure has now repeatly occured here: *** Theory loader: undefined theory entry for Approximation_Ex *** Failed to finish proof *** At command by (line 42 of /mnt/nfsbroy/home/isatest/isadist/Isabelle_04-Sep-2010/src/HOL/Decision_Procs/ex/Approximation_Ex.thy) i.e. this proof: lemma \bar exp 1.626 - 5.08346273 \bar (inverse 10 ^ 10 :: real) by (approximation 80) Is there a way to report the internal results produced here? Then we can show David Matthews some more concrete problem report than Failed to finish proof. 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
