On Sun, 2 Jun 2013, Alexander Krauss wrote:
On 05/30/2013 03:51 PM, Makarius wrote:
BTW, I've seen really good sources
recently: ACL2. They have a *strict* 80 char limit, and really good
writing style of "essays", not "code documentation".
This sounds interesting. Can you point to some examples of such essays?
I've come across this when studying the parallel proof support in recent
ACL 6.x, e.g.
http://www.cs.utexas.edu/users/moore/acl2/v6-2/distrib/acl2.tar.gz with
its acl2-sources/parallel-raw.lisp and the "Essay on Parallelism". There
are many more such essays in the ACL2 sources.
The general impression is that these guys take a lot of care of their
sources and the articles that are inline here, although it is not clear
how far it is formally correct in the face of changing definitions in the
actual source code -- or maybe these guys are just very conservative and
don't change things so much.
For us, the "essays" with the general explanations of concepts and
examples are the manuals. Just recently (d9fed6e99a57) I have managed to
eliminate the last remains of the old "ref" manual, which was still in
informal/unchecked LaTeX. The "implementation" manual has taken over the
role of explaining concepts and the main ML entry points, and also some
examples, with some degree of formal checking. That is a lot of work to
maintain in any case. Just to brush up the 180 pages of old "ref" I've
required approx. 5 years.
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. (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.)
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
