Re: [isabelle-dev] Remaining uses of Proof General?

2014-07-25 Thread Gerwin Klein
On 25 Jul 2014, at 10:23 am, Makarius makar...@sketis.net wrote: Oddly, people are still seen using 'find_theorems' etc. inlined into the source text. That was an intermediate approach from several years ago. If it is still used today, what are the remaining resons for it? Not having to

Re: [isabelle-dev] Remaining uses of Proof General?

2014-07-25 Thread Makarius
On Fri, 25 Jul 2014, Gerwin Klein wrote: On 25 Jul 2014, at 10:23 am, Makarius makar...@sketis.net wrote: Oddly, people are still seen using 'find_theorems' etc. inlined into the source text. That was an intermediate approach from several years ago. If it is still used today, what are the

Re: [isabelle-dev] Remaining uses of Proof General?

2014-07-25 Thread Gerwin Klein
On 25 Jul 2014, at 11:20 am, Makarius makar...@sketis.net wrote: On Fri, 25 Jul 2014, Gerwin Klein wrote: On 25 Jul 2014, at 10:23 am, Makarius makar...@sketis.net wrote: Oddly, people are still seen using 'find_theorems' etc. inlined into the source text. That was an intermediate

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-30 Thread Makarius
On Sun, 29 Jun 2014, Cezary Kaliszyk wrote: Hi Makarius, On Thu, Jun 26, 2014 at 11:08 PM, Makarius makar...@sketis.net wrote: At the moment (06599233e54e) there are no remaining uses of Proof General to the best of my knowledge. If anybody has counter-examples they should be put on the

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-30 Thread Cezary Kaliszyk
Hi Makarius, On Thu, Jun 26, 2014 at 11:08 PM, Makarius makar...@sketis.net wrote: At the moment (06599233e54e) there are no remaining uses of Proof General to the best of my knowledge. If anybody has counter-examples they should be put on the table for discussion. I am using Isabelle via

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-28 Thread Lars Noschinski
On 27.06.2014 23:47, Makarius wrote: Just a side remark: in the repository version we are talking about, and thus the coming release, ML in auxiliary files works smoothly and often better than the ML blocks, because the file gets its own ML mode. For ML files, I occasionally had the problem

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Lars Noschinski
On 27.06.2014 07:52, John Wickerson wrote: Moreover, I would like an incremental search, but there is probably a jEdit pluging somewhere? (Probably with the same problems of entering non-ASCII characters) There is already an incremental search, but by default it has no keyboard shortcut.

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Makarius
On Fri, 27 Jun 2014, Peter Lammich wrote: I have compiled a list of problems that I encountered during my work. OK, I will go through it one by one to eliminate them -- either by pointing out known ways how to do it in Isabelle/jEdit, or by fine-tuning the system in this stage before the

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Makarius
On Fri, 27 Jun 2014, Peter Lammich wrote: My overall impression is that Isabelle/jEdit is usable but much less mature than PG: It does not scale well to large projects, and tends to be unstable. It has many cool advanced features, but lacks important basic ones. Better reverse all that, just

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Makarius
On Fri, 27 Jun 2014, Peter Lammich wrote: SCALABILITY STABILITY: * Isabelle/jEdit gets really slow and unresponsive when many files are loaded (you have to wait seconds for a keystroke to show its effect). As all prerequisite theories (not in an image) are automatically loaded, this is

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Makarius
On Fri, 27 Jun 2014, Peter Lammich wrote: * Isabelle/jEdit does not scale to large files. Error markers on the right side are only displayed for a context around the current cursor position. There seems to be no way to jump to the error position. If the error happens to be displayed as a red

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Makarius
On Fri, 27 Jun 2014, Peter Lammich wrote: * Isabelle/jEdit seems to be quite unstable. Within one week, it happened several (3 or 4) times that the whole thing just became unresponsive, and had to be restarted to continue work. In PG, those things happen perhaps once in a month. The

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Makarius
On Fri, 27 Jun 2014, Peter Lammich wrote: * Isabelle/jEdit does not support highlighting of paranthesis in the output window (it does work in PG!). This is an essential feature to read bigger goal states. Moreover, the output buffer does not support middle-mouse-button copy-and-paste on my

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Makarius
On Fri, 27 Jun 2014, Peter Lammich wrote: * Long list of warnings, e.g. duplicate simp rule, or tracing messages produced by a method appear before the subgoals in the output, and thus makes them inaccessible without lots of scrolling. This feature is a real flow-stopper when exploring proofs.

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Peter Lammich
That clickable area is convenient, but not strictly necessary. It is absent in PG anyway. Whenever the Prover IDE outputs an error message, e.g. in tooltips or the Output panel, it includes the source position information, *if* that is available. The problem is, that I cannot make the

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Peter Lammich
The default guess is that the JVM has too little heap space. You have called 4 GB unreasonably large before, which is an indication that your defaults are far too low. OK, I'll try more on my 8Gb machine ... or upgrade my machine. If problems happen again with 4-8 GB JVM heap, you

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Makarius
On Fri, 27 Jun 2014, Peter Lammich wrote: * If sledgehammer (both over panel and as command) is running, further processing of the file is blocked/very slow. Thus, it is not possible to run sledgehammer and, in parallel, continue exploration to find your own proof. In PG, parallel

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Makarius
On Fri, 27 Jun 2014, Peter Lammich wrote: * Isabelle/jEdit cannot open a theory-file without processing it. This is in particular a problem when porting stuff and opening the original version of the same file to look something up. Even worse: Once opened, you cannot close the file again, and it

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Makarius
On Fri, 27 Jun 2014, Peter Lammich wrote: Moreover, I would like an incremental search, but there is probably a jEdit pluging somewhere? (Probably with the same problems of entering non-ASCII characters) Other people have given some hints already. You should also take the time to *print* and

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Peter Lammich
On Fr, 2014-06-27 at 13:58 +0200, Makarius wrote: On Fri, 27 Jun 2014, Peter Lammich wrote: * Long list of warnings, e.g. duplicate simp rule, or tracing messages produced by a method appear before the subgoals in the output, and thus makes them inaccessible without lots of scrolling.

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Makarius
On Fri, 27 Jun 2014, Peter Lammich wrote: * When theories have inconsistent file/theory name, you will only find the error by stepwise going back the chain of bad theory - errors, file by file. This is simply tedious. In PG, you got a backtrace in the output, and could immediately identify the

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Makarius
On Fri, 27 Jun 2014, Peter Lammich wrote: * Auto-Completion does not really work. You have to decide for a completion delay. If you choose it too short, some completions will not appear at all. If you choose it too long, it interrupts your typing flow when entering special characters. In PG,

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Makarius
On Fri, 27 Jun 2014, Peter Lammich wrote: * Disappearing Proofs in PG is a really nice feature to keep overview, in particular in larger files. In PG, I used it heavily. There is nothing similar in Isabelle/jEdit. Code-folding can be used to a certain extent, but it cannot handle

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Makarius
On Fri, 27 Jun 2014, Peter Lammich wrote: If problems happen again with 4-8 GB JVM heap, you should describe what really happens, with clear experimental setup. Giving a clear experimental setup is a real problem for errors that appear nondeterministically. The first thing is to describe

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Makarius
On Fri, 27 Jun 2014, Peter Lammich wrote: * Regular messages (writeln, warning, error) also appear in the squiggly rendering of the sources, to be hovered over and inspected without scrolling *the* Output. There is in fact no reason to have just one (or two or three) focal

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Makarius
On Fri, 27 Jun 2014, Makarius wrote: On Fri, 27 Jun 2014, Peter Lammich wrote: * If sledgehammer (both over panel and as command) is running, further processing of the file is blocked/very slow. Thus, it is not possible to run sledgehammer and, in parallel, continue exploration to find

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Peter Lammich
On Fr, 2014-06-27 at 14:22 +0200, Makarius wrote: On Fri, 27 Jun 2014, Peter Lammich wrote: If problems happen again with 4-8 GB JVM heap, you should describe what really happens, with clear experimental setup. Giving a clear experimental setup is a real problem for errors that appear

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Makarius
Some more explanations on the meta-model of this thread: * We have about 1 week left on isabelle-dev, to discuss whatever might prevent using Isabelle/jEdit smoothly, and why people fall-back on PG as a reflex. * Then there will be Isabelle2014-RC0, as a published release candidate,

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-27 Thread Makarius
On Fri, 27 Jun 2014, Peter Lammich wrote: * Writing tools in ML (ML-blocks in thy-file) Just a side remark: in the repository version we are talking about, and thus the coming release, ML in auxiliary files works smoothly and often better than the ML blocks, because the file gets its own

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-26 Thread Makarius
This is a reminder that this thread is still open, until the end of next week when the question will be moved to isabelle-users, with the appearance of Isabelle2014-RC0 (that will be published from the running repository *without* a repository fork yet). At the moment (06599233e54e) there are

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-26 Thread Peter Lammich
Hi all. I have given Isabelle/jEdit another try and worked with it for almost two weeks, on different tasks: * Porting the CAVA afp entries (depending on 300 theory files) from 2013-2 to devel. * Formalizations and proof development (The standard usage) * Writing tools in ML (ML-blocks in

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-26 Thread John Wickerson
Great list Peter! * The standard search (Ctrl-F) function does not allow to enter non-ASCII characters at all. This is a real show-stopper if you search for a text containing such characters. In PG, you could at least use \... - tokens to enter non-ASCII characters. Moreover, I would like

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-25 Thread Jasmin Christian Blanchette
(For now the list of Remaining uses of Proof General / Emacs seems to be empty. If there is anything remaining, this thread is still open to submissions.) Let me make this list nonempty again. In the course of a day, I typically find myself pulling from the Isabelle repository several

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-25 Thread Makarius
On Sun, 25 May 2014, Jasmin Christian Blanchette wrote: In the course of a day, I typically find myself pulling from the Isabelle repository several times. I am encouraged in this by my use of Mercurial queues. So it's not untypical that my HOL image is slightly out of date, usually in a

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-25 Thread Jasmin Blanchette
Am 25.05.2014 um 14:59 schrieb Makarius makar...@sketis.net: On Sun, 25 May 2014, Jasmin Christian Blanchette wrote: In the course of a day, I typically find myself pulling from the Isabelle repository several times. I am encouraged in this by my use of Mercurial queues. So it's not

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-25 Thread Makarius
On Sun, 25 May 2014, Jasmin Blanchette wrote: -n no build dialog for session image on startup I thought this only controlled whether the dialog is shown; not whether the build takes place. That was once a separate build_dialog tool, but it is now just an implicit build, so I

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-24 Thread Makarius
On Tue, 29 Apr 2014, Matthew Fernandez wrote: Currently most of my theories are generated by another tool. When debugging the generated theories, I often have to open a file that I know contains many broken proofs. In these circumstances it can be beneficial to have a way of stepping into the

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-24 Thread Makarius
This is not a remaining use of Proof General, but of the Emacs text editor: trimming the final newline of theory sources for document preparation. This could lead to extra white space between sections in the last decades, but it was just one of these habits to take care of that manually.

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-13 Thread Andreas Lochbihler
Thanks a lot. Andreas On 12/05/14 20:07, Florian Haftmann wrote: 1. Violation of well-sortedness constraints: type ... not an instance of ... declare [[show_sorts]] code_thms constant to be exported Then, I use educated guessing and Emacs' incremental search to navigate the code equations

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-12 Thread Makarius
On Fri, 2 May 2014, Makarius wrote: On Tue, 29 Apr 2014, Andreas Lochbihler wrote: Until then there are various approximations: * Multiple floating instances of Output, with different Update / Auto update state. * The Output / Detach button to produce an unchanging Info window on the

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-12 Thread Makarius
On Tue, 29 Apr 2014, Thomas Sewell wrote: Back to the actual technical questions. What are the main performance bottle-necks here? Printing of intermediate goal states? Or applying intermediate steps repeatedly? I suspect that the problem is not that the printing or the intermediate

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-12 Thread Florian Haftmann
1. Violation of well-sortedness constraints: type ... not an instance of ... declare [[show_sorts]] code_thms constant to be exported Then, I use educated guessing and Emacs' incremental search to navigate the code equations that have been output until I find the fault -- usually, it's

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-12 Thread Makarius
The list of remaining uses of Proof General is shrinking dramatically every day. We can continue this a bit more during May, all referring to ongoing repository development. During the month of June, I will be mostly on vacation. After that the convergence towards the release needs to

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-08 Thread Thomas Sewell
Thanks Makarius. A few of us at NICTA have ported this change to our various versions of Isabelle and begun playing with it. It seems to improve the situation sometimes, though we haven't yet got a feel for when in particular it helps. In fact, we haven't really understood what the change

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-08 Thread Makarius
On Thu, 8 May 2014, Thomas Sewell wrote: If I knew a proper way to reduce the priority (or to pre-empt) worker threads for that, I would do it. But it probably needs some work by David Matthews on the ML thread infrastructure. Consider me an unashamed pragmatist. The important point is

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-08 Thread David Matthews
On 08/05/2014 11:25, Makarius wrote: On Thu, 8 May 2014, Thomas Sewell wrote: If I knew a proper way to reduce the priority (or to pre-empt) worker threads for that, I would do it. But it probably needs some work by David Matthews on the ML thread infrastructure. Preempting long-running

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-07 Thread Makarius
On Mon, 5 May 2014, Makarius wrote: Users running on batteries might also want a mode that restricts all threads to the behaviour above. Have you tried that with threads = 1 (there is also a special treatment for high-priority prints in that mode)? So far I guess that most people run with

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-07 Thread Makarius
On Fri, 2 May 2014, Makarius wrote: On Tue, 29 Apr 2014, Andreas Lochbihler wrote: text ‹ @{term ‹A \un B›} › Here the \un works as expected -- the cartouche remains intact independently of its content, as long as the funny parentheses are nested properly. But this

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-05 Thread Makarius
On Mon, 5 May 2014, Thomas Sewell wrote: The basic assumption is that each proof task does not run too long, and if it does it is something to be improved in the application to make it more smooth. In contrast, Proof General makes it more easy to produce huge and heavy proof scripts that

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-04 Thread Thomas Sewell
On 03/05/14 00:05, Makarius wrote: On Tue, 29 Apr 2014, Thomas Sewell wrote: I tried an adjustment a while ago in which I had the goal state print incrementally. Even if some of the subgoals took a while to print, you'd see the line with goal (12 subgoals) immediately, and then the subgoals

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-02 Thread Makarius
On Tue, 29 Apr 2014, Thomas Sewell wrote: I tried an adjustment a while ago in which I had the goal state print incrementally. Even if some of the subgoals took a while to print, you'd see the line with goal (12 subgoals) immediately, and then the subgoals as they were formatted. The short

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-02 Thread Makarius
On Tue, 29 Apr 2014, Andreas Lochbihler wrote: text ‹ @{term ‹A \un B›} › Here the \un works as expected -- the cartouche remains intact independently of its content, as long as the funny parentheses are nested properly. But this correct nesting is exactly the problem. When I type \un

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-02 Thread Makarius
On Tue, 29 Apr 2014, Andreas Lochbihler wrote: There are hardly any performance problems in terms of computing power, possibly except for Isabelle processing a slow call to auto over and over again. The efficiency problem is the interaction with the IDE. I use the Find panel a lot, but then

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-02 Thread Andreas Lochbihler
On 02/05/14 16:16, Makarius wrote: On Tue, 29 Apr 2014, Andreas Lochbihler wrote: text ‹ @{term ‹A \un B›} › Here the \un works as expected -- the cartouche remains intact independently of its content, as long as the funny parentheses are nested properly. But this correct nesting is

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-02 Thread Makarius
On Fri, 2 May 2014, Andreas Lochbihler wrote: The reason is that I often add the delimiters only later. For example, when I write a single-identifier term, I use text {* @{term my_constant} *} and some time later, I figure out that I have to add something, e.g., a type constraint. Hence, I

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-01 Thread Florian Haftmann
But I try to process such theories with jEdit and only go back to XEmacs/PG when I cannot stand Isabelle/jEdit any longer (which usually happens when I debug the code generator setup). That's an interesting observation. What are the particular properties of »debugging« here that make PG

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-29 Thread Andreas Lochbihler
Hi Makarius, On 28/04/14 23:10, Makarius wrote: a) Given some text like definition foo where foo = ... when I add an attribute like [simp]: after the where, I get a symbol completion popup to replace the : with the element sign. Usually, my next thing is to move the cursor with the cursor

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-29 Thread Andreas Lochbihler
On 28/04/14 23:18, Makarius wrote: On Mon, 28 Apr 2014, Andreas Lochbihler wrote: 2. Reactivity when processing large files With PG, I knew how to control the Isabelle prover. When I edit a large file in a larger project like JinjaThreads, every now and then, Isabelle changes the background

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-29 Thread Andreas Lochbihler
On 28/04/14 22:25, Makarius wrote: On Mon, 28 Apr 2014, Andreas Lochbihler wrote: My main usage of PG is when I want to construct a complicated proof method call like (fastforce intro: ... dest: ... elim: ... simp add: ... cong: ... del: ... simp del: ...)+ that collapses an apply script

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-29 Thread René Neumann
What is funny is that Proof General was actually one of the main reasons of moving only slowly in such token language reforms. I am glad that PG still works for most of my theories and I try to keep that state as long as feasible. There are already problems with new keywords declared by AFP

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-29 Thread Makarius
On Tue, 29 Apr 2014, Andreas Lochbihler wrote: * What are your exact hardware parameters: CPU, main memory? Intel® Core™ i7-3630QM CPU @ 2.40GHz, 8GB memory That is a recent high-end laptop or a midrange desktop machine. JinjaThreads is *the* biggest Isabelle application on the planet,

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-28 Thread Andreas Lochbihler
Hi Makarius, Over the past weeks, I've been using Isabelle/jEdit about half of my Isabelle time (and ProofGeneral 3.7.1.1 with XEmacs the other half). Isabelle/jEdit is great when it comes to working on small projects or refactoring existing sources. I really like the negative line spacing

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-28 Thread Peter Lammich
I'm still a regular user of PG. From time to time, I test Isabelle/jEdit, and my reasons for switching back to PG are somewhat similar to what Andreas reported. My main problems with Isabelle/JEdit are: 1. I cannot really control what Isabelle/Jedit processes when, and it invests computation

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-28 Thread Makarius
On Mon, 28 Apr 2014, Matthew Fernandez wrote: On 28/04/14 04:14, Makarius wrote: Are there any remaining uses of Proof General, e.g. in the situation of current Isabelle/5b6f4655e2f2 ? I'm mostly on Isabelle/jEdit now, but I do delve back into Isabelle/Emacs (is that the current

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-28 Thread Makarius
On Mon, 28 Apr 2014, Andreas Lochbihler wrote: My main usage of PG is when I want to construct a complicated proof method call like (fastforce intro: ... dest: ... elim: ... simp add: ... cong: ... del: ... simp del: ...)+ that collapses an apply script of a hundred lines. I haven't yet

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-28 Thread Makarius
On Mon, 28 Apr 2014, Andreas Lochbihler wrote: a) Given some text like definition foo where foo = ... when I add an attribute like [simp]: after the where, I get a symbol completion popup to replace the : with the element sign. Usually, my next thing is to move the cursor with the cursor

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-28 Thread Makarius
On Mon, 28 Apr 2014, Andreas Lochbihler wrote: 2. Reactivity when processing large files With PG, I knew how to control the Isabelle prover. When I edit a large file in a larger project like JinjaThreads, every now and then, Isabelle changes the background colour from red to gray and then,

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-28 Thread Makarius
On Mon, 28 Apr 2014, Peter Lammich wrote: 1. I cannot really control what Isabelle/Jedit processes when, and it invests computation power on the meaningless parts of the file directly after the point where I am editing. I'm not even convinced that it is the right approach to let

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-28 Thread Matthew Fernandez
On 29/04/14 01:04, Makarius wrote: On Mon, 28 Apr 2014, Matthew Fernandez wrote: My reasons are mostly predictable execution, as I can control what the prover is up to with explicit stepping forwards and backwards. I can probably achieve the same result toggling continuous checking on/off in

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-28 Thread Thomas Sewell
Back to the actual technical questions. What are the main performance bottle-necks here? Printing of intermediate goal states? Or applying intermediate steps repeatedly? I suspect that the problem is not that the printing or the intermediate calculations are taking too long. It's that

[isabelle-dev] Remaining uses of Proof General?

2014-04-27 Thread Makarius
Are there any remaining uses of Proof General, e.g. in the situation of current Isabelle/5b6f4655e2f2 ? This is neither a joke nor a running gag -- I just can't think of anything myself after the introduction of the spell checker. Makarius

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-27 Thread Manuel Eberl
Hallo, I am not, as it were, a user of Proof General anymore; however, I would like, if I may, to point out one thing that annoys me in jEdit and that was, in my opinion, better in Proof General: the handling of abbreviations for Unicode characters. The current behaviour with “immediate

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-27 Thread Makarius
On Sun, 27 Apr 2014, Manuel Eberl wrote: I am not, as it were, a user of Proof General anymore; however, I would like, if I may, to point out one thing that annoys me in jEdit and that was, in my opinion, better in Proof General: the handling of abbreviations for Unicode characters. Please

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-27 Thread Matthew Fernandez
On 28/04/14 04:14, Makarius wrote: Are there any remaining uses of Proof General, e.g. in the situation of current Isabelle/5b6f4655e2f2 ? I'm mostly on Isabelle/jEdit now, but I do delve back into Isabelle/Emacs (is that the current terminology for this creature?) every now and then. My