Email Gateway (Aug 22 2022 at 12:41): Email Gateway (Aug 22 2022 at 12:41):From: Serguei Mokhov <serguei@gmail.com>
Hello all,
Are there plans to facelift a bit the tutorial document in Isabelle
distribution? Is anyone working on it slowly?
If not, are contributions to it welcome or is it not worth the effort?
In particular, at the very least:
While there is a good volume of good stuff in there for instance it
still refers to Proof General in its tooltips; these could be
"refactored" into the way it is now done in jEdit with new tips added
or obsolete non-replaceable removed.
prog-prove and other docs have appeared over the last few years with
some more recent info, so at least these can be all referenced in the
beginning in the introduction to direct the reader to those other
places based on their need on datatypes, functions, locales, etc..
This is such that the tutorial cold be the starting point for all
branching out to other documentation, while the rest is being updated
or just stays as-is self-contained.
Email Gateway (Aug 22 2022 at 12:41):From: Tobias Nipkow <nipkow@in.tum.de>
On 18/02/2016 15:09, Serguei Mokhov wrote:
Hello all,
Are there plans to facelift a bit the tutorial document in Isabelle
distribution? Is anyone working on it slowly?
No. It is largely subsumed by the other tutorials. Hence "Programming and
Proving in Isabelle/HOL" says that the proof style is outdated. Maybe the web
page should move the tutorial down the list.
Tobias
If not, are contributions to it welcome or is it not worth the effort?
In particular, at the very least:
- While there is a good volume of good stuff in there for instance it
still refers to Proof General in its tooltips; these could be
"refactored" into the way it is now done in jEdit with new tips added
or obsolete non-replaceable removed.- prog-prove and other docs have appeared over the last few years with
some more recent info, so at least these can be all referenced in the
beginning in the introduction to direct the reader to those other
places based on their need on datatypes, functions, locales, etc..
This is such that the tutorial cold be the starting point for all
branching out to other documentation, while the rest is being updated
or just stays as-is self-contained.
Email Gateway (Aug 22 2022 at 12:41):From: Makarius <makarius@sketis.net>
The web page is a presentation of the same formal doc/Contents that are
part of the Isabelle distribution, and displayed in Isabelle/jEdit
Documentation. I am all for reforming that, but it is something for the
next release. E.g. the old "tutorial" could be moved to "Old Manuals".
Many years ago, the "Reference Manuals" were hardly maintained, but now
that part contains the most up-to-date material, while half of the
"Tutorials" stayed unchanged. The most current manual in Isabelle2016 is
the one on Isabelle/jEdit (last item in the visible list).
Makarius
Email Gateway (Aug 22 2022 at 12:41):From: Tobias Nipkow <nipkow@in.tum.de>
On 18/02/2016 15:48, Makarius wrote:
On Thu, 18 Feb 2016, Tobias Nipkow wrote:
Maybe the web page should move the tutorial down the list.
The web page is a presentation of the same formal doc/Contents that are part of
the Isabelle distribution, and displayed in Isabelle/jEdit Documentation. I am
all for reforming that, but it is something for the next release. E.g. the old
"tutorial" could be moved to "Old Manuals".
D'accord.
Tobias
Many years ago, the "Reference Manuals" were hardly maintained, but now that
part contains the most up-to-date material, while half of the "Tutorials" stayed
unchanged. The most current manual in Isabelle2016 is the one on Isabelle/jEdit
(last item in the visible list).Makarius
smime.p7s
Email Gateway (Aug 22 2022 at 12:42):From: Thomas Genet <thomas.genet@irisa.fr>
Dear all,
do you think that including a short "hands-on" tutorial (like the one I
posted some monthes ago) would be worth?
I tried it with 15 persons (programmers, Coq users) and it helped them
to quickly interact with the tool (and feel its power!), in less than 45
minutes.
Best regards,
Thomas
shortIsabelleTutorial.pdf
Email Gateway (Aug 22 2022 at 12:42):From: Lawrence Paulson <lp15@cam.ac.uk>
It’s great that people are preparing tutorials, but it’s probably better if we don’t try to take them over.
On the other hand, I imagine that could happen if one of them turned out to be really popular. Then we would want to keep it updated with the latest changes, while making sure it contained nothing we regard as bad advice.
Larry Paulson
Last updated: May 06 2024 at 12:29 UTC