*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Remaining reasons for Proof General*From*: Jasmin Blanchette <jasmin.blanchette at gmail.com>*Date*: Tue, 12 Nov 2013 16:01:49 +0100*Cc*: isabelle-users Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <alpine.LNX.2.00.1311111531350.10735@macbroy21.informatik.tu-muenchen.de>*References*: <CANofLeJJ8O2Y2ktXUER1AsH1F4CQsBB21PPbLMVVQa-UfwjgoQ@mail.gmail.com> <353FF788-2AA0-4188-8AAD-28E803A1F647@gmail.com> <CANofLeLVT7QWSUE4HhNy+kq9UuCe4J7gsXVEzma0x_SO5C03wQ@mail.gmail.com> <26755B7F-E696-4A5D-9BE7-9BCFA0FF85B8@gmail.com> <alpine.LNX.2.00.1311111227510.20958@macbroy21.informatik.tu-muenchen.de> <5280E51C.3010703@inf.ethz.ch> <alpine.LNX.2.00.1311111531350.10735@macbroy21.informatik.tu-muenchen.de>

Hi Makarius, I still find myself using Proof General on a daily basis. The main reason for this is that it's much easier to reload ML code in PG than in jEdit. Here's a typical scenario. Suppose I want to debug a failure in "primcorec". Then I do the following: 1. Open a "Scratch" theory by starting PG with -l HOL-Cardinals (the base image of BNF). 2. Import "~~/src/HOL/BNF/BNF_GFP" and write a small example that reproduces the problem in "Scratch". 3. Add debugging commands, fix bugs, etc., in the ML files loaded (directly or indirectly) by "BNF_GFP" using some other editor. 4. Unprocess and reprocess "Scratch". 5. Repeat steps 3 and 4 dozens of times. Isabelle/PG was good at reloading exactly those theories that need to be reloaded, without baby sitting. Trying to achieve the same in jEdit requires a lot of clicking and a bit of thinking (to figure which .thy file has the right "ML_file" command). I understand my use case is not typical for most users, who do not spend their days writing long pieces of ML code, and I can live with PG to do that. Still, it would be nice if jEdit/PIDE, which is otherwise so smart about so many Isabelle specifics, would reach the level of PG on this one point. Jasmin

**Follow-Ups**:**Re: [isabelle] Remaining reasons for Proof General***From:*Makarius

**Re: [isabelle] Remaining reasons for Proof General***From:*Peter Lammich

**References**:**[isabelle] sledgehammer in RC4***From:*Randy Pollack

**Re: [isabelle] sledgehammer in RC4***From:*Jasmin Blanchette

**Re: [isabelle] sledgehammer in RC4***From:*Randy Pollack

**Re: [isabelle] sledgehammer in RC4***From:*Jasmin Blanchette

**Re: [isabelle] sledgehammer in RC4***From:*Makarius

**Re: [isabelle] sledgehammer in RC4***From:*Andreas Lochbihler

**[isabelle] Remaining reasons for Proof General***From:*Makarius

- Previous by Date: Re: [isabelle] Remaining reasons for Proof General
- Next by Date: Re: [isabelle] Remaining reasons for Proof General
- Previous by Thread: Re: [isabelle] Remaining reasons for Proof General
- Next by Thread: Re: [isabelle] Remaining reasons for Proof General
- Cl-isabelle-users November 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list