[isabelle-dev] Spec_Check

[David Greenaway]

On 24/06/13 21:20, Makarius wrote:
> Last week, I actually intended to make a proper exposition about
> Isabelle/ML futures in the "implementation" manual, but for now it
> just points to ~~/src/Pure/Concurrent/future.ML with its slightly odd
> "Notes" at the beginning.  That needs to be turned into proper text
> outside the sources, as part of the manual.

As a single data-point: I personally find the "Notes" at the top of the
file far more useful than out-of-line documentation. In particular,
I never think to look in the implementation manual because only a very
small percentage of the Isabelle sources are documented there.

> (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:
I would claim that a description at the top of the file---and perhaps
a few sentences on top of important functions---helps just as much as
pages of carefully typeset prose.

Further, the latter tends to require much more effort, 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.

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.)

Cheers,
David


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.