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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
