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

On Fri, 23 Nov 2012, Christoph LANGE wrote:

But I could imagine a better _guidance_, both on the documentation website ( 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.)


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