Email Gateway (Aug 22 2022 at 20:02): Email Gateway (Aug 22 2022 at 20:02):From: Wolfram Kahl <kahl@cas.mcmaster.ca>
Would this perhaps also be a good home for a
``Getting Started with the Isabelle/jEdit IDE''
chapter or section?
Or does that exist anywhere? (I have not been able to find it.)
I gather from this mailing list that jEdit does not have a huge
user community outside Isabelle, so most Isabelle users will not have
met jEdit before.
The information needed for getting started with a decent mental model
of the interface presented by jEdit and Isabelle/jEdit appears to be
spread somewhat randomly over the not-so-short jEdit and Isabelle/jEdit
manuals --- the ``Getting Started with the Isabelle/jEdit IDE''
chapter/section/document I have in mind would collect all that,
with new users in mind.
Where to look'', what to look for'', what to wait for'', and
what not to wait for'' seem, to me, general questions where the
answers are not always obvious --- for example, keyboard-oriented
users may discover the crucial hover interface of Isabelle/jEdit only
by accident or not at all.
I found such an IDE introduction sorely missing
both for re-starting to use Isabelle myself after a hiatus of over a decade,
and for getting students started.
Wolfram
Email Gateway (Aug 22 2022 at 20:02):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Wolfram,
a very basic version of what you are asking for would be available here
https://arxiv.org/abs/1208.1368
But it is aimed at complete beginners.
cheers
chris
Email Gateway (Aug 22 2022 at 20:02):From: Wolfram Kahl <kahl@cas.mcmaster.ca>
Indeed --- thank you!
In my opinion, this urgently needs to be integrated into the
``Isabelle Tutorials'' list on the Isabelle Documentation page and
into the Isabelle documents list in the distribution, or even made
part of the prog-prove document.
Everything seems to suggest that prog-prove should be THE place to get
started, and then, if you try, you fail miserably on the jEdit
interaction front...
Wolfram
Email Gateway (Aug 22 2022 at 20:02):From: Makarius <makarius@sketis.net>
There is an official and updated Isabelle/jEdit manual in Isabelle2019,
right in the Documentation panel.
It also explains the relation to the original jEdit text editor,
including its documentation (a copy of that is in Documentation as well).
Makarius
Email Gateway (Aug 22 2022 at 20:03):From: Wolfram Kahl <kahl@cas.mcmaster.ca>
On Tue, Jun 18, 2019 at 08:44:28PM +0200, Makarius wrote:
On 18.06.19 17:01, Wolfram Kahl wrote:
On Tue, Jun 18, 2019 at 10:00:27AM +0000, Urban, Christian via
Cl-isabelle-users wrote:
The Isabelle Cookbook is intended to help beginners to get started
with Isabelle programming.Would this perhaps also be a good home for a
``Getting Started with the Isabelle/jEdit IDE''
chapter or section?
Or does that exist anywhere? (I have not been able to find it.)
There is an official and updated Isabelle/jEdit manual in Isabelle2019,
right in the Documentation panel.
I know, and I referred to that in my first message on this.
This is a reference manual, with information that is important already at the start
distributed over the whole document, and without a ``Getting Started'' section.
Even Christian Sternagel's short document
| a very basic version of what you are asking for would be available here |
|---|
| https://arxiv.org/abs/1208.1368 |
contains at least something about symbol input (section 4.1),
while section 1.2 of the ``jedit'' document contains nothing.
It also explains the relation to the original jEdit text editor,
including its documentation (a copy of that is in Documentation as well).
I also referred to that...
I'm now expanding the options of which I hope one will happen to three:
1) An improved/expanded version of https://arxiv.org/abs/1208.1368
is added to the document list, with very visible pointers
from prog-prove'' and jedit''.
2) A Getting Started with the Isabelle/jEdit interface'' section
(not necessarily with that title) is added to prog-prove'',
with a pointer from ``jedit''.
3) A Getting Started with the Isabelle/jEdit interface'' section
(not necessarily with that title) is added to jedit'',
with a very visible pointer from ``prog-prove''.
Wolfram
Email Gateway (Aug 22 2022 at 20:03):From: Thomas Genet <thomas.genet@irisa.fr>
Dear Wolfram,
maybe you will find this short tutorial relevant:
https://hal.inria.fr/hal-01208577v6/document
Initially it was designed for students using Isabelle/jEdit for the
first time (but having some knowledge in functional programming).
I updated it for Isabelle 2018 (thanks to updates provided by Jørgen
Villadsen).
Best regards,
Thomas
Last updated: Apr 20 2024 at 12:26 UTC