On Tue, 25 Jun 2013, David Greenaway wrote:
(There is a conceptual problem with putting such explanations into the
sources, since they are built in bottom-up manner, but explanations
should be more top-down; this is also relevant for worked examples
that are actually run.)
Again, users don't need a function-by-function running commentary of the
sources, but just need to get a high-level idea of what is going on:
And this is the problem: you cannot give high-level explanations in a
bottom up manner. The manuals are there to do that, and people are urged
to study them (over and over again).
I know that many people just want to know things from a quick glancy at
the header of some file, but this does not work due to the inherent
complexity of what we are doing here. There is no way around spending a
lot of time, both with the sources and the manuals.
meaning that often the choice boils down to either having
quick-and-dirty notes in the source that exist, versus polished
documentation outside the sources that doesn't.
Sources need to be clean by definition -- no place for quick-and-dirty
things here. The manuals are usually less polished, and actually a bit
removed from the sources, so that is not a problem.
On this note, if you would like someone to go through and add
documentation inline to the Isabelle sources, I would be willing to put
my hand up to help out. (Assuming, of course, there was an interest in
committing the patches, and a willing expert to review them.)
Not that again. It will end up with tons of private scribbling by people
who think they know something about what the sources do. We had lots of
bad jokes from that department in distant past, from less clean sources.
Isabelle development has emerged over several decades. Your should invest
a bit more time to learn about how things work.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
