Re: [isabelle] Documentation of ML sources [was: BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue]

Hi all,

the email snipplet below shows one of those often arising discussions about documentation of Isabelle's ML sources.

In fact, documentation of ML sources come in various facets:

- the existing ML source
- the historical variants of the ML sources in the last twenty years
- the annotations to the changesets
- Isabelle's mailing lists
- the unchecked code comments, that usually tells you what did not work in the past or could have been improved in the past

When modifying existing implementations, it is certainly profitable to spend an hour or two, investigating the sources and look at the changes, and search through the mailing list. Often, subtle "surprises" have been touched before, and implementations go through a number of iterations with some "pros" and "cons".

The ideas of the existing implementation is further documented in the Isabelle implementation manual. Reading it provides a dense reference of concepts for people, that want to understand concepts in more detail.

The Isabelle developer tutorial provides an simple access to programming in Isabelle with various examples, and a rather simplified view on some topic. It is helpful for starters and beginners, but also only scratches the surface of some functionalities.

I envisaged the Quickcheck tool for Isabelle's ML (presented last week in Munich) as some further project to address documentation of the sources. In the short term, I wanted that specifications would allow us to document oddities in the system by grading surprising specifications of functions, which could then be addressed at any point in the future if we consider the surprise severe enough to change.

In the long term, I was thinking that users and developers could discuss their expectations about functions in this formal setting of properties or contracts, and the Quickcheck tool would motivate using specifications when implementing, and a run-time monitoring tool for specifications would ease changing code in the maintenance process.

NB: Brian agreed with the idea of contracts, as he was pushing for more fine-grained types. His ideas were much more intrusive changing the implementation, whereas specifications/contracts would only add some fine-grained information in other files.

In my opinion, there is very much documentation for Isabelle's ML sources. As far as I see it, there are two further opportunities for improvements in a very long-term range: - Provide ways to cross-link the various documentation sources (and user interfaces to get all relevant documents) - Provide more fine-grained descriptions (e.g., provide specs that can be checked with the Quickcheck tool) and investigate if this simplifies or hinders our development process.


On 10/22/2012 06:45 PM, Peter Lammich wrote:
Anyway, if none of the two alternatives is appropriate, the rules for
composing conversions should be CLEANLY documented.

I consider this a bug, because it is nowhere documented that the user of conversions has to take care of beta-normalization manually.

Despite tons of manuals, which are often hard to keep in overview anyway, the real documentaion is the ML source:

On 10/23/2012 01:11 PM, Makarius wrote:
On Tue, 23 Oct 2012, Ondřej Kunčar wrote:

ML source is not the real documentation!

You also need to include its history.

It is a matter of long practice and endurance to make sense out of all that. It is important to make a serious start, by giving up what you think about it in the first impulse.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.