[isabelle-dev] Spec_Check

[Makarius]

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