[isabelle-dev] Relations vs. Predicates
makarius at sketis.net
Fri Apr 13 11:52:45 CEST 2012
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
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
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.
More information about the isabelle-dev