Email Gateway (Aug 19 2022 at 09:10): Email Gateway (Aug 19 2022 at 09:10):From: Christoph LANGE <c.lange@cs.bham.ac.uk>
2012-11-23 06:55 Tobias Nipkow:
OK, got the point. Now I really can't imagine a better title.
But I could imagine a better _guidance_, both on the documentation
website (http://isabelle.in.tum.de/documentation.html) and in the
"doc/Contents" file of the Isabelle installation (at least I have
/usr/share/doc/isabelle-2012/doc/Contents when installing from the
Gentoo Linux package).
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
Similarly, the doc/Contents file should not merely restate the _titles_
of the documents, but provide the same extra information.
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 09:11):From: Makarius <makarius@sketis.net>
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) 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
Email Gateway (Aug 19 2022 at 09:11):From: Alfio Martini <alfio.martini@acm.org>
(No email body)
Email Gateway (Aug 19 2022 at 09:11):From: Tobias Nipkow <nipkow@in.tum.de>
Am 23/11/2012 11:49, schrieb Christoph LANGE:
2012-11-23 06:55 Tobias Nipkow:
Am 22/11/2012 17:15, schrieb Christoph LANGE:
BTW, about "Programming and Proving": I had noticed this manual when I got
started with Isabelle, but then didn't take a closer look, as I was misled by
the "Programming". I thought it was some specific guide on verifying functional
programs.In a way it is. It starts from a functional programming perspective. If you have
a suggestion for a better title, let me know.OK, got the point. Now I really can't imagine a better title.
But I could imagine a better _guidance_, both on the documentation website
(http://isabelle.in.tum.de/documentation.html) and in the "doc/Contents" file of
the Isabelle installation (at least I have
/usr/share/doc/isabelle-2012/doc/Contents when installing from the Gentoo Linux
package).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
I think most of the titles are self-explanatory, and indicate that they are
special manuals. Except for the first two. But all of them come with an abstract
or intro, and prog-prove explains quite clearly what it is about (and mentions
that the second one is old fashioned). You might want to also have this abstract
on the web page, but that would require yet more mechanisms.
However, there is a small linguistic point, which you may or may not have
intended to make: "Miscellaneous" material usually comes at the end. These are
"Tutorials", no qualification. The next subsection isn't called "Miscellaneous
Reference Manuals" either, and the whole section is called "Tutorials and
manuals". Makarius, could you drop the "Miscellaneous", please?
Tobias
Similarly, the doc/Contents file should not merely restate the _titles_ of the
documents, but provide the same extra information.Cheers,
Christoph
Email Gateway (Aug 19 2022 at 09:11):From: Makarius <makarius@sketis.net>
There has been a lot of fluctuation and historical jokes in that file.
At some point the main reference manuals where pushed to the end along
with the "Old Manuals". Then there were "Miscellaneous Tutorials" and
"Main Reference Manuals", with "main" counted among the tutorials. Now it
is "Miscellaneous Tutorials" and "Reference Manuals", with "main" included
in reference manuals, which might explain why the title lost its "Main".
So the next logical step is indeed "Tutorials" and "Reference Manuals" for
the coming release, to disentangle that a bit more.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC