[isabelle-dev] Spec_Check

[Makarius]

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