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

[Brian Huffman]

The effect of my change "typedef (open) unit" is to remove the
definition of the following constant

unit_def: "unit == {True}"

thus making the name "unit" available to users.

- Brian

On Thu, Nov 18, 2010 at 1:58 PM, Makarius <makarius at sketis.net> wrote:
> 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 archive.
>
>
> 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
> process.
>
> 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.
>
>
>        Makarius
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>