Re: [isabelle-dev] Remaining uses of Proof General?
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 of a hundred lines. I haven't yet found a convenient way to write the apply script in Isabelle/jEdit, because of reactivity issues (see item 2 below) and the continuous updates of the output window (when I scroll to some other part of the apply script using the cursor keys). Are there key bindings for scrolling that do not move the cursor? This reminds me of a very old insider jokes from the mid-1990-ies: Dieter Nazareth had finished the W0 formalization where he had turned half-decent tactic scripts into such compact one-liners, and shortly afterwards Wolfgang Naraschewski had to disentangle that again for the full W formalization, or rather start from scratch. A few years later, the Isar language emerged and made that approach in principle obsolete. I know, I have myself untangles such one-liners often enough when something has changed. Nevertheless, I believe that I'm still faster to build these one-liners than write pretty Isar proofs of hundreds of lines, just because the goal states are huge and all cases are shown in the same way. Back to the actual technical questions. What are the main performance bottle-necks here? Printing of intermediate goal states? Or applying intermediate steps repeatedly? 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 my output panel is not visible at the same time (that's why I would like to split the right dock in two). And when I scroll upwards to find a snippet of tactic script that I want to copy, the output updates and my current goal state is gone. (I know I could disable the updating, but then I have to enable it manually again.) I can say more when I understand the actual problem better. In such situations I normally have to see the dynamics of how you actually work. Maybe I can show you what my problems are at ITP in Vienna in July. Andreas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of Proof General?
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 colour from red to gray and then, apparently nothing happens for minutes before Isabelle turns it red again and starts reprocessing. Is there some way to explicitly tell Isabelle that it should now start to check again. Toggling "continuous checking" does not help. Sometimes, I even have to close the theory file and reopen it again. This sounds like the Poly/ML RTS is desparately trying to reclaim memory, by aggressive sharing huge amounts of data. Not long ago that situation lead into real memory problems on my good old 32 GB machine, but David Matthews managed once again to postpone the ultimate JinjaThreads implosion as a black hole of computing resources. For now just the usual game, according to Tim the Enchanter: * What are your exact hardware parameters: CPU, main memory? Intel® Core™ i7-3630QM CPU @ 2.40GHz, 8GB memory * What is your operating system? Ubuntu 12.04 LTS * What are your ML system settings, e.g. as shown by "isabelle build -?" ? ML_PLATFORM="x86-linux" ML_HOME="~/.isabelle/contrib/polyml-5.5.1-1/x86-linux" ML_SYSTEM="polyml-5.5.1" ML_OPTIONS="-H 500" * What are your JVM settings: ISABELLE_JAVA_SYSTEM_OPTIONS and JEDIT_JAVA_OPTIONS ? JEDIT_JAVA_OPTIONS="-Xms128m -Xmx3072m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false" * What are the options "threads" and "parallel_proofs" ? threads = 0, parallel_proofs = 2 Andreas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of Proof General?
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 keys. But the popup gobbles all the key strokes until I explicitly
close it
with ESC. As colons are used everywhere in Isabelle's outer syntax, it would
really be
great if the popup only appears when I am in inner syntax.
b) Sometimes, when I write a HOL term, I used to not get the completion popup
when I
enter something like \un if there were sufficiently many parse errors in that
partial
term. Even Ctrl-b did not help. However, I cannot reproduce it in a small
example at the
moment.
In the case a), I guess that you still have the completion delay 0.0, while I
presently
work with 0.5 to give the prover a chance to add semantic completion
information, before
any popups are shown.
My completion delay is 0.1. When writing Isabelle terms normally, this is the amount of
time that does not break my flow of typing.
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 while writing the above,
the closing parenthesis are not there yet. The prover sees something like
text {* @{term "A \un
lemma foo: "..." by ...
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 entries that are
not listed in the keywords file. I then usually insert ; as a delimiter. 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).
Andreas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of Proof General?
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 printing the output the user wants to see is waiting on some other computation finishing, creating the sensation of lag. Some evidence to back this up: 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 summary is that this helped a little sometimes, but I often still saw an empty Output panel for seconds after moving the cursor to a line that the continuous checker had already processed. I strongly suspect that the print request was waiting in a queue somewhere. The system would become responsive again once it finished doing something else. I don't think that this is to do with garbage collection or heap sharing - I don't recall a specific instance, but I'm sure I've seen this behaviour when there's been plenty of spare memory. Sometimes there would be purple lines in the buffer, suggesting that some of the worker threads were busy on other tasks, but not always. On incremental printing: it's easy to implement by generalising a couple of the relevant Pretty operations to produce a Seq.seq internally rather than a list. It looked promising initially, but then became really annoying, because Isabelle/jEdit or PIDE resets the Output buffer each time it gets more to display. So if you scroll down to look for something, you get scrolled back up for each time a subgoal prints, which can give the sensation that the editor is fighting you. That's why I didn't make any effort to suggest it upstream. I don't know if that helps. Perhaps if I run across a good demonstrative example I'll send it across. Cheers, Thomas. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of Proof General?
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 Isabelle/jEdit, but haven't invested the time in modifying my workflow. Can you say more about typical situations? When doing occasional debugging, either of tools or the system itself, I need more knowledge about what happens when exactly. I never do this in Proof General these days, but within the Prover IDE in a buffer that contains only the main items of interest. Then I edit carefully, based on educated guesses how the PIDE document model works, or I toggle the continuous checking that was newly introduced in Isabelle2013-2. 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 middle of a broken proof to explore, while ignoring all the following (also broken) proofs). Having said that, this cuts both ways. Isabelle/jEdit's behaviour of continuing in the face of broken proofs can allow me to explore a proof in the middle of a theory without needing to tediously repair the broken proofs preceding it. To summarise, I use whichever tool is most applicable to my current situation, but predominantly Isabelle/jEdit. I've also encountered the problems discussed in other threads of the Isabelle/jEdit GUI locking up when some tactic is looping and the JVM heap being exhausted with no indication from the UI. I reckon that this refers to the official Isabelle2013-2 release. I have reworked many details of scheduling in the past few months, even just now when writing this email. When the Isabelle2014-RC line starts (probably in July) you should look precisely at your typical applications to see how it works. I don't want to see again a situation where problem reports trickle only slowly *after* the release is shipped. Yes, sorry, you are correct. Either way, any UI issues I have encountered are subsumed by threads others have raised on this mailing list. The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of Proof General?
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 Isabelle/jEdit's heuristics decide when and what it processes, and make user intervention impossible at first place Isabelle/jEdit is indeed about giving up manual control: the system is moving so fast, that you cannot handle every part of it yourself. It is like a TGV: you buy a ticket and sit comfortably, while the machine is moving on its own. There is nothing really revolutionary about that. Any of the major IDEs work in a similar manner. I don't claim any orginality on ideas here. Last year at ITP Rennes, it was very interesting for me to see that the MSR guys are imitating a similar IDE model in Dafny, although that is a quite different prover and a quite different platform. Hopefully the ITP community will make further moves towards serious IDEs, not just boring copy paste from one buffer into another (where a sub-ordinate process consumes that). (Or even worse, force the user into workarounds like inserting semicolons or "end"s behind the current editing point, which seems to be common practice among Isabelle/jEdit users) I don't know much about common practice. Maybe that is just what people at TUM do occasionally. There is the general problem here that people are often too shy or just not capable to explain what they are doing. It is also difficult to describe verbally how interaction is done, but videos sometimes help. 2. In PG, when the processed region reaches the end of a theory file, I can be pretty sure that everything is fine with this theory. In Isabelle/jEdit, I have to scan the theory status panel manually for remaining red or pink bars, which is very inconvenient for large projects with hundreds of files. I can't follow this argument. The Theories panel is one of the things that is lacking in Proof General. I cannot imagine anymore how big libraries were managed in the old regime. What is indeed missing is the infamous "wrap-up" of a session, that I have explained on the Isabelle mailing lists many times, like what isabelle build does in batch mode. That is still not there, since the Theories panel already does a fairly good job, and doing it formally in the IDE document model is not completely trivial: such things need to be done in real time on the spot for large libraries. Moreover, I find it a bit scary that severe errors related to Isabelle/jEdit's document processing model (cf. https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-November/msg00170.html) can go undiscovered for several month, although most Isabelle users are on Isabelle/jEdit these days. I ask myself: Have they got so used to strange behaviours of the IDE that they do not realize severe errors any more? That was a severe problem, and I can guess only half of the reasons how this came about. I would not use that as an argument againts Isabelle/jEdit, though, since the problem was caused by some unclear bit of the implementation that had to care about standard mode (PIDE) and legacy mode (TTY / Proof General) at the same time. If the latter had been discontinued 2 years ago, we would all be in better shape today. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of Proof General?
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, apparently nothing happens for minutes before Isabelle turns it red again and starts reprocessing. Is there some way to explicitly tell Isabelle that it should now start to check again. Toggling "continuous checking" does not help. Sometimes, I even have to close the theory file and reopen it again. This sounds like the Poly/ML RTS is desparately trying to reclaim memory, by aggressive sharing huge amounts of data. Not long ago that situation lead into real memory problems on my good old 32 GB machine, but David Matthews managed once again to postpone the ultimate JinjaThreads implosion as a black hole of computing resources. For now just the usual game, according to Tim the Enchanter: * What are your exact hardware parameters: CPU, main memory? * What is your operating system? * What are your ML system settings, e.g. as shown by "isabelle build -?" ? * What are your JVM settings: ISABELLE_JAVA_SYSTEM_OPTIONS and JEDIT_JAVA_OPTIONS ? * What are the options "threads" and "parallel_proofs" ? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of Proof General?
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 keys. But the popup
gobbles all the key strokes until I explicitly close it with ESC. As
colons are used everywhere in Isabelle's outer syntax, it would really
be great if the popup only appears when I am in inner syntax.
b) Sometimes, when I write a HOL term, I used to not get the completion
popup when I enter something like \un if there were sufficiently many
parse errors in that partial term. Even Ctrl-b did not help. However, I
cannot reproduce it in a small example at the moment.
We should move anything concerning completion on specific threads on this
mailing list, with explicit subject what it is about. It will take quite
some time for the coming release to stabilize in that respect. There are
a bit too many ambitious and smart mechanisms involved here.
For now just a few notes.
In the case a), I guess that you still have the completion delay 0.0,
while I presently work with 0.5 to give the prover a chance to add
semantic completion information, before any popups are shown. That
includes a "no_completion" markup produced by the prover, specifically for
things like ":", although this introduces a real danger of
non-determinism.
The gobbling of key events by the popup should not happen, but there are
some uncertainties due to key event workarounds in jEdit, and workarounds
around these in Isabelle/jEdit. The basic idea is that the popup consumes
exactly those key strokes that are relevant to it, and passes everything
else to the main text area -- this is also what jEdit usually does. This
behaviour has fluctuated concerning cursor left and right keys several
times, and I need to check this once again soon.
For current 9c3f0ae99532 I confirm that the first cursor left/right event
is indeed absorbed.
Case b) with \foo sequences happens whenever there is some semantic
completion context and string literals involved: backslash sequences
destroy the string token, and thus may change the context again. Here is
an example:
text {*
@{term "A \un B"}
*}
The language context for 'text' disables symbol completion, because it is
in conflict with latex macros, as just seen on the thread on
isabelle-users "Symbol Shortcuts vs. LaTeX code". The antiquotation
changes the language context again to allow symbols, but the malformed
string "A \un B" breaks that, and it falls back into the enclosing text
context. So the \un cannot be completed.
One of the motivations for backslash escapes is to make them different
from usual legal input, but exactly that causes the problems here. I have
started to think about making bad string tokens more acceptable to certain
language layers, but that is once again an extra complication.
A different approach is to use new cartouche syntax instead, which
addresses old issues of quotation robustness and escape confusion
uniformly. Using that token syntax, the above example becomes this:
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. There is a different error, though: the term parser does not
accept outer cartouche tokens yet. It could allow that, but I found this
too ambitious as a start for the new syntax.
What is funny is that Proof General was actually one of the main reasons
of moving only slowly in such token language reforms. We are back again
in a dead-lock situation, and not the first time in the past few years.
Leaving the old Emacs world behind more decisively would free a lot of
hidden resources, and that could have been done at least 2 years ago
without any regrets.
Of course there is no fundamental problem of Proof General supporting
cartouches. There was once special code for nested comments that could be
reactivated. The point is that somebody would have to do something, and
not just expect that software magically maintains itself.
Makarius___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of Proof General?
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 found a convenient way to write the apply script in Isabelle/jEdit, because of reactivity issues (see item 2 below) and the continuous updates of the output window (when I scroll to some other part of the apply script using the cursor keys). Are there key bindings for scrolling that do not move the cursor? This reminds me of a very old insider jokes from the mid-1990-ies: Dieter Nazareth had finished the W0 formalization where he had turned half-decent tactic scripts into such compact one-liners, and shortly afterwards Wolfgang Naraschewski had to disentangle that again for the full W formalization, or rather start from scratch. A few years later, the Isar language emerged and made that approach in principle obsolete. Back to the actual technical questions. What are the main performance bottle-necks here? Printing of intermediate goal states? Or applying intermediate steps repeatedly? As you move the cursor over commands, the Output updates itself, without any activity from the prover. The prover prints states as you change the editor view, e.g. by scrolling or resizing the window. You can disable the Auto-update of the Output dockable, but that does not affect the proof process, only the display. You can prevent the prover from burning cycles either by reducing the number of worker threads, or disabling the continuous checking. I can say more when I understand the actual problem better. In such situations I normally have to see the dynamics of how you actually work. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] scala-2.11.0
On Fri, 25 Apr 2014, Makarius wrote: trimming it down to the simplest possible approach. I have done this now in Isabelle/e1317a26f8c0 (and the row of changes before it). So most of the PIDE "operating system" functionality is now re-implemented by more basic means, in just 48 hours. It is interesting that this can be done, but that is mostly a port of existing Isabelle/ML modules from src/Pure/Concurrent. The resulting Scala/PIDE sources are more concise, and the implementation presumably more robust and efficient. A bit more of this spring cleaning of the PIDE OS is now in Isabelle/59f70b89e5fd. The internal event propagation now bypasses the one central GUI thread of Swing, which is the canonical bottle neck of any non-tricial application. Thus the overall reactivity should be better, with less "GUI hangs" as the prover crunches big sessions and throws the results at the front-end. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of Proof General?
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 terminology for this creature?) I don't know all details about the terminology, which is also slightly varying over time. There are Isabelle tools called "emacs" and "jedit" after the underlying text editors, which I introduced myself some years ago, alongside with "isabelle tty" (which actually uses "rlwrap" as editor if that is available). "isabelle emacs" invokes "Proof General" or "Isabelle Proof General" (in contrast to the Coq version), or "Proof General Emacs" (in contrast to the Eclipse version) -- David Aspinall could explain that more precisely. I used myself wrongly "ProofGeneral" over many years, and David never told me that until it was rather late, but I changed that habit afterwards. "isabelle jedit" starts Isabelle/jEdit. This was once a tiny Isabelle plugin for the jEdit text editor (so the distinction did not exist yet), but is now a rather big IDE based on jEdit and a lot of extra functionality provided by the plugin + a few JVM bootstrap tricks. Regular users of official releases also get a native application wrapper that was newly introduced in Isabelle2013-2, and is different from the jEdit distribution. 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 Isabelle/jEdit, but haven't invested the time in modifying my workflow. Can you say more about typical situations? When doing occasional debugging, either of tools or the system itself, I need more knowledge about what happens when exactly. I never do this in Proof General these days, but within the Prover IDE in a buffer that contains only the main items of interest. Then I edit carefully, based on educated guesses how the PIDE document model works, or I toggle the continuous checking that was newly introduced in Isabelle2013-2. I've also encountered the problems discussed in other threads of the Isabelle/jEdit GUI locking up when some tactic is looping and the JVM heap being exhausted with no indication from the UI. I reckon that this refers to the official Isabelle2013-2 release. I have reworked many details of scheduling in the past few months, even just now when writing this email. When the Isabelle2014-RC line starts (probably in July) you should look precisely at your typical applications to see how it works. I don't want to see again a situation where problem reports trickle only slowly *after* the release is shipped. Isabelle/Emacs is capable of running on underpowered machines which do not have enough resources to run Isabelle/jEdit. This is not a good reason for maintaining legacy support, but there may be users in this situation. It is a normal sign of stagnation of some application that it suddenly runs blazingly fast on old or tiny hardware. At ITP 2013 last summer I've seen a few Coq users working comfortably with CoqIDE or Proof General on netbooks are small laptops. That surely can't be done with a full-scale Prover IDE like Isabelle/jEdit. When Proof General was young and strong, it was also huge and bloated compared to the hardware of that time, escpecially XEmacs was really heavy and we had many insider jokes about that. The relation of hardware vs. software performance is not an accident, but the result of the normal balancing of trade-offs: How much functionality can we afford on a certain range of hardware at the moment? I routinely walk through consumer electronics stores like Fnac Paris, to see what you get for 500..1000 EUR, to estimate what can be expected from typical users. Then I test on 3 systematically on 3 dissimilar systems, 2 of them actually > 3 years old. What I normally don't test is unplugged battery mode, because I am in the lucky situation of not commuting. People who do that routinely, should make some systematic experiments with the nominal number of Isabelle/ML threads at 0.5 of the true number of cores, i.e. 0.25 of the virtual number of cores on Intel. To simplify the calculation, just try the constant threads = 1 an see how it works. Last summer at Rennes, someone was surprised to have a "2 core laptop running at 600% CPU", but it actually turned out a new i7 with 8 virtual CPUs. The defaults were just burning down the batteries, without any extra benefit in those warm summer days. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of Proof General?
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 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 Isabelle/jEdit's heuristics decide when and what it processes, and make user intervention impossible at first place (Or even worse, force the user into workarounds like inserting semicolons or "end"s behind the current editing point, which seems to be common practice among Isabelle/jEdit users) 2. In PG, when the processed region reaches the end of a theory file, I can be pretty sure that everything is fine with this theory. In Isabelle/jEdit, I have to scan the theory status panel manually for remaining red or pink bars, which is very inconvenient for large projects with hundreds of files. Moreover, I find it a bit scary that severe errors related to Isabelle/jEdit's document processing model (cf. https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-November/msg00170.html) can go undiscovered for several month, although most Isabelle users are on Isabelle/jEdit these days. I ask myself: Have they got so used to strange behaviours of the IDE that they do not realize severe errors any more? -- Peter On Mo, 2014-04-28 at 09:14 +0200, Andreas Lochbihler wrote: > 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 setting and completion of fact names! Thanks! > > 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 found a > convenient way to > write the apply script in Isabelle/jEdit, because of reactivity issues (see > item 2 below) > and the continuous updates of the output window (when I scroll to some other > part of the > apply script using the cursor keys). Are there key bindings for scrolling > that do not move > the cursor? > > > Here are some things that could be improved in Isabelle/jEdit (I am currently > on > Isabelle/4e2a0d4e7a82): > > 1. Symbol completion in PG was absolutely deterministic. The immediate symbol > completion > in jEdit works great, too, I merely had to learn new sequences of key > strokes. Symbol > completion of non-unique results is not satisfactory. > > 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 keys. But the popup gobbles all the key strokes until I explicitly > close it with > ESC. As colons are used everywhere in Isabelle's outer syntax, it would > really be great if > the popup only appears when I am in inner syntax. > > b) Sometimes, when I write a HOL term, I used to not get the completion popup > when I enter > something like \un if there were sufficiently many parse errors in that > partial term. Even > Ctrl-b did not help. However, I cannot reproduce it in a small example at the > moment. > > > 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, apparently nothing happens for minutes before Isabelle > turns it red > again and starts reprocessing. Is there some way to explicitly tell Isabelle > that it > should now start to check again. Toggling "continuous checking" does not > help. Sometimes, > I even have to close the theory file and reopen it again. > > > 3. Navigation between theories files > > In PG, I usually have only a small subset of the loaded theories and ML files > open as > buffers, and I conveniently switch between them with Ctrl-x b. In jEdit, I > use Ctrl-` to > go to the previous file, but going to a different one is a pain, because I > have to search > it in the complete list of open files. > > It would be great if there was a list of just those files that I had on my > screen > previously, not all loaded files. > > Moreover, when I close a file and then press Ctrl-` in the file that shows > up, I do not > get to the file I have visited before the two, but to some arbitrary other. > Can jEdit > remember the order in which files have been visited? XEmacs at least doe
Re: [isabelle-dev] Remaining uses of Proof General?
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 setting and completion of fact names! Thanks! 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 found a convenient way to write the apply script in Isabelle/jEdit, because of reactivity issues (see item 2 below) and the continuous updates of the output window (when I scroll to some other part of the apply script using the cursor keys). Are there key bindings for scrolling that do not move the cursor? Here are some things that could be improved in Isabelle/jEdit (I am currently on Isabelle/4e2a0d4e7a82): 1. Symbol completion in PG was absolutely deterministic. The immediate symbol completion in jEdit works great, too, I merely had to learn new sequences of key strokes. Symbol completion of non-unique results is not satisfactory. 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 keys. But the popup gobbles all the key strokes until I explicitly close it with ESC. As colons are used everywhere in Isabelle's outer syntax, it would really be great if the popup only appears when I am in inner syntax. b) Sometimes, when I write a HOL term, I used to not get the completion popup when I enter something like \un if there were sufficiently many parse errors in that partial term. Even Ctrl-b did not help. However, I cannot reproduce it in a small example at the moment. 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, apparently nothing happens for minutes before Isabelle turns it red again and starts reprocessing. Is there some way to explicitly tell Isabelle that it should now start to check again. Toggling "continuous checking" does not help. Sometimes, I even have to close the theory file and reopen it again. 3. Navigation between theories files In PG, I usually have only a small subset of the loaded theories and ML files open as buffers, and I conveniently switch between them with Ctrl-x b. In jEdit, I use Ctrl-` to go to the previous file, but going to a different one is a pain, because I have to search it in the complete list of open files. It would be great if there was a list of just those files that I had on my screen previously, not all loaded files. Moreover, when I close a file and then press Ctrl-` in the file that shows up, I do not get to the file I have visited before the two, but to some arbitrary other. Can jEdit remember the order in which files have been visited? XEmacs at least does this. Maybe there are already solutions to the above annoyances, I just don't know them. There's another thing I would like to see in jEdit: The window layout has three columns (one dock on the left and one on the right) and the middle column (with the editor area) can be divided in three rows (dock - text - dock). Is there some way that I can split the right column into two rows to show two information areas at the same time (e.g. Output at the top and Find below)? Andreas On 27/04/14 20:14, Makarius wrote: 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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
