Re: [isabelle] Title of "Programming and Proving" [Re: ?spam? Re: Simpler theorem statements, and proofs for them]



>
>  Larry even goes as far saying, that nobody reads manuals anyway.
> Nonetheless I spend myself a lot of time to keep the main reference manuals
> up-to-date, with more and more examples.  And others have updated various
> tutorials over time.


Without all the Isabelle documentation, I would have no chance  with
this wonderful software system.

So, I am especially thankful that they are well-written and continuously
updated and
maintained!

Best!

On Fri, Nov 23, 2012 at 11:05 AM, Makarius <makarius at sketis.net> wrote:

> On Fri, 23 Nov 2012, Christoph LANGE wrote:
>
>  But I could imagine a better _guidance_, both on the documentation
>> website (http://isabelle.in.tum.de/**documentation.html<http://isabelle.in.tum.de/documentation.html>)
>> and in the "doc/Contents" file of the Isabelle installation
>>
>
>  On the website, Prog&Prove is listed first, but under a section header
>> "Miscellaneous tutorials".  The section title could be changed to "Getting
>> started", and each document link could be followed by a few words of
>> explanation, e.g.:
>>
>>    Programming and Proving in Isabelle/HOL – Isabelle by example; read
>> this first
>>
>
> This assumes a closed model of the documentation, and a uniform
> understanding of it that does not really exist.  Isabelle has many
> different manuals from many different angles looking at the system, and a
> long time-span covered in the writing of the texts. Larry even goes as far
> saying, that nobody reads manuals anyway. Nonetheless I spend myself a lot
> of time to keep the main reference manuals up-to-date, with more and more
> examples.  And others have updated various tutorials over time.
>
> Concerning "guidance", that is also an open issue for the Prover IDE. When
> I start Netbeans, it guides me quickly through the process of producing a
> simple Java program.  Little of that is there in Isabelle/jEdit so far. At
> least in Isabelle2012, you should get a near 100% success rate in starting
> it up on your platform, whatever it is (excluding *BSD).
>
>
>  at least I have /usr/share/doc/isabelle-2012/**doc/Contents when
>> installing from the Gentoo Linux package
>>
>
> Better ignore these home-made derivatives of the official Isabelle
> distribution, they will always be 1 or 2 steps behind the real thing.
>
> Many years ago, I was fond of making OS packages myself as a hobby, long
> before Debian and Gentoo existed.  It is rather pointless for Isabelle now,
> because the distribution is constructed in a way what would be called
> "portable application" these days.  So you don't care about "installing"
> it, you just put it somewhere and run it.  (This annoys packagers, because
> they become obsolete, but users usually like it.)
>
>
>         Makarius
>



-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil




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