[isabelle-dev] informative changelogs / typedef (open) unit

Makarius makarius at sketis.net
Thu Nov 18 22:58:02 CET 2010

Hi Brian,

can you say a few words about b994d855dbd2 just for the historical record?

Such changes deep down in HOL easily cause odd problems later on, so the 
one doing the bisection in some years might need more info via the mail 

I would also like to take the opportunity to recall our most basic 
changelog conventions:

   each item on a separate line;
   items ordered roughly by importance;

For some reason, many people have started to sequeze everything in a 
single line (frequent), or imitate the headline/body text format of other 
projects with a completely different structure (rare).  The reason might 
be as profane as the default web style of Mercurial, but at least on 
http://isabelle.in.tum.de/repos/isabelle the display follows the usual 
Isabelle format.

I spend a good portion of my time inspecting changesets, not just the 
incoming ones, but also really old ones when sorting out problems. So the 
little extra care when composing changelogs will help a lot in the overall 

The recent crash of find_theorems due to b654fa27fbc4 is just one example 
that changes deep in the system need routine reviewing.  It's on my list 
for several weeks, but I did not find the time to look at it so far.


More information about the isabelle-dev mailing list