[isabelle-dev] introduction to Isabelle/jEdit for PG users?
c.sternagel at gmail.com
Fri Jan 25 04:10:48 CET 2013
On 01/25/2013 12:19 AM, Lawrence Paulson wrote:
> There is a lot of useful information in this paper! I think I have finally got the point of the document model.
Good to hear.
> It might be good to consolidate your main points in a much shorter webpage. Your paper is structured (naturally) as a paper, but for the corresponding webpage I would delete the abstract and most of the introductory material. I wouldn't actually state that Isabelle/jEdit is awesome (such judgements are always up to the reader), but simply outline what the document model is, and how it differs from approaches used in other systems.
I agree. Unfortunately, I will not have time to work on it until
February 4 (due to paper deadlines). When is the rollout of Isabelle2013
At some point makarius also suggested a screencast tutorial video for
jEdit (I gather you had something similar for emacs once). I'm still
interested in contributing to that (but the same time constraints as
above apply). I'm not sure if such a screencast should/could be part of
the Isabelle distribution, though. If not, time is not constrained by
the upcoming Isabelle release.
Another point. Since we are currently testing release candidates of
Isabelle/jEdit and thus there are still chances of changes, it might be
good to wait with any tutorial, until the testing phase is over?
> It might be good to keep the Proof General material separate, e.g. as a sidebar (assuming we make a webpage). Other users might be coming from systems such as Coq, which behave very differently, whether or not Proof General is involved.
> The other option is to put something like this right in Isabelle/jEdit's README file. Frankly I think the current version isn't that useful to beginners, and they are the main target of any README file.
> On 23 Jan 2013, at 00:19, Christian Sternagel <c.sternagel at gmail.com> wrote:
>> I tried to summarize most of the issues that made it to the Isabelle mailing lists (at that time) in my submission to the Isabelle Users Workshop.
>> It's definitely incomplete, but maybe it could help.
>> On 01/23/2013 04:07 AM, Tobias Nipkow wrote:
>>> In principle a good idea, but I don't think we want multiple intros for
>>> different audiences. Hence I would aim for a general intro that also covers
>>> points that PG users are used to.
>>> Am 22/01/2013 13:30, schrieb Lawrence Paulson:
>>>> Do we provide an introduction to Isabelle/jEdit for PG users? It might be a good idea to do so. I'm willing to make a first attempt at this, though I'm sure it will contain some mistakes, which I'm sure others of you would be only too happy to fix.
>>>> I have in mind a single webpage, with a couple of screenshots. In fact, I don't know the full possibilities of Isabelle/jEdit, so it will only be a start. But as usual, the first step seems to be the hardest.
>>>> isabelle-dev mailing list
>>>> isabelle-dev at in.tum.de
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
More information about the isabelle-dev