[isabelle-dev] introduction to Isabelle/jEdit for PG users?

[Christian Sternagel]

Dear Larry,

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 
planned?

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.

cheers

chris
>
> Larry
>
> 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.
>>
>>   http://arxiv.org/abs/1208.1368
>>
>> It's definitely incomplete, but maybe it could help.
>>
>> cheers
>>
>> chris
>>
>> 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.
>>>
>>> Tobias
>>>
>>> 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.
>>>>
>>>> Larry
>>>>
>>>> _______________________________________________
>>>> isabelle-dev mailing list
>>>> isabelle-dev at in.tum.de
>>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>>
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>