Re: [isabelle] Documentation of ML sources [was: BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue]
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