[isabelle-dev] Relations vs. Predicates

[Makarius]

On Fri, 13 Apr 2012, Christian Sternagel wrote:

>> Moreover, incoming changesets needs to be easy to inspect in a few 
>> seconds or minutes. (This is why I always ask to write each log item on 
>> a separate line, but still with a delimiter such as ";").
> Indeed. I hope my commit messages have at least been "correct" in this 
> respect?

I've mentioned the line separation specifically for Isabelle/b75ce48a93ee. 
The README_REPOSITORY has this long exposition on this detail:

   * The standard changelog entry format of the Isabelle repository
     admits several (vaguely related) items to be rolled into one
     changeset.  Each item is then described on a separate line that
     may become longer as screen line and is terminated by punctuation.
     These lines are roughly ordered by importance.

     This format conforms to established Isabelle tradition.  In
     contrast, the default of Mercurial prefers a single headline
     followed by a long body text.  The reason for that is a somewhat
     different development model of typical "distributed" projects,
     where external changes pass through a hierarchy of reviewers and
     maintainers, until they end up in some authoritative repository.
     Isabelle changesets can be more spontaneous, growing from the
     bottom-up.

     The web style of http://isabelle.in.tum.de/repos/isabelle/
     accommodates the Isabelle changelog format.  Note that multiple
     lines will sometimes display as a single paragraph in HTML, so
     some terminating punctuation is required.  Do not squeeze multiple
     items on the same line in the original text!

It takes a few extra seconds in the routine "eye balling" process to 
reparse a long line to chop it into the respective items.  This time is 
better invested in looking at the content.  I hope that I am not the only 
one who keeps an eye on incoming changes; there are often small issues 
that need to be discussed.


 	Makarius