Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Documentation of ML sources [was: BUG in conv....

Email Gateway (Aug 19 2022 at 09:03):

From: Lukas Bulwahn <bulwahn@in.tum.de>
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.

Lukas

Last updated: Apr 19 2024 at 08:19 UTC