Re: [isabelle-dev] Remaining uses of Proof General?
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 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. That is the normal future task farm, with its restricted worker thread pool. All PIDE execution works via some Future.fork, with different priorities in the queue. Proof tasks have low priority, print tasks have high priority. Once a task is running on some thread, it continues and cannot be preempted by newer tasks with higher priority. 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 can be hardly handled by anyone else later. 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. That would probably violate some implicit assumptions about print modes, which are a slightly odd intrusion into the purity of Pretty.T. What was the reason for incremental printing anyway? Just performance for huge goal states? There are other bottle-necks concerning that, and if goals really do get that big one should think about other ways to expose them, not by printing in the old-fashioned way. Incrementality might have other reasons and actual benefits. In the early years of PIDE I had more ambitions for that, but it caused so many additional problems in the document model and the GUI that I removed most of it for the sake of delivering something that is sufficiently stable to be usable in practice. 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. There is a deeper conceptual problem here. Several independent entities want to update content of some GUI component: output window, tree view etc. This requires a merge of these change of the GUI state, but that is usually only done by a hard reset on one side, ignoring the other side. You can see that in jEdit's SideKick tree view, Isabelle/jEdit's Output dockable with scrollbar and folds, or even just in a plain Terminal with the scrollbar. 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 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 while
writing the above, the closing parenthesis are not there yet. The prover sees
something like
text {* @{term A \un
lemma foo: ... by ...
But why? In the ancient times, input was always sequential, as depth-first
traversal of the intended tree structure. In less ancient times, some
people proposed rigid structural editors to make it impossible to escape
from nested boxes (still seen today in TeXmacs), although that is a bit
awkward. In the past 10 years or so, the standard IDE approach has
arrived somewhere in the middle: the user is free to type intermediate
non-sense, but the editor makes it easy to get it right by default.
Isabelle/jEdit still lacks serious templating, but there are beginnings of
it in the completion mechanism. The outer quotations and antiquotations
have specific support already: a single keystroke ` offers a template for
a well-formed cartouche, and the @{ prefix completes to a well-formed @{}
with the cursor in the middle. Even Proof General had C-c C-a C-a for
isar-antiquote already.
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 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 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. The mechanics of the Output panel are a bit old-fashioned, still assuming a single-focus proof script model. At some point I would like to see a proper Preview of a certain part of proof document, with state output just in the right spots (zero or more depending on proof structure). 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 spot. * The more flexible docking framework provided by the MyDoggy plugin, although it is unclear if that is more than a nice experiment by one of the old-time jEdit developers. 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 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 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 ...
But why? In the ancient times, input was always sequential, as depth-first
traversal of
the intended tree structure. In less ancient times, some people proposed rigid
structural
editors to make it impossible to escape from nested boxes (still seen today in
TeXmacs),
although that is a bit awkward. In the past 10 years or so, the standard IDE
approach has
arrived somewhere in the middle: the user is free to type intermediate
non-sense, but the
editor makes it easy to get it right by default.
I have used such templating mechanism with Eclipse and finally disabled them, because they
caused me more work than what they saved. I usually prefer to enter both delimiters
separately and to just see the matching parenthesis highlighted.
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 produce the following sequence of edits (the # denotes the position of the cursor)
text {* @{term #my_constant} *}
text {* @{term #my_constant} *}
text {* @{term my_constant#} *}
text {* @{term my_constant :: my_type#} *}
text {* @{term my_constant :: my_type#} *}
With the template mechanisms that I have seen so far, I get the following
sequence:
text {* @{term #my_constant} *}
text {* @{term #my_constant} *}
text {* @{term #my_constant} *}
text {* @{term my_constant#} *}
text {* @{term my_constant :: my_type#} *}
text {* @{term my_constant :: my_type#} *}
text {* @{term my_constant :: my_type#} *}
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 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 produce the following sequence of edits (the # denotes
the position of the cursor)
text {* @{term #my_constant} *}
text {* @{term #my_constant} *}
text {* @{term my_constant#} *}
text {* @{term my_constant :: my_type#} *}
text {* @{term my_constant :: my_type#} *}
With the template mechanisms that I have seen so far, I get the following
sequence:
text {* @{term #my_constant} *}
text {* @{term #my_constant} *}
text {* @{term #my_constant} *}
text {* @{term my_constant#} *}
text {* @{term my_constant :: my_type#} *}
text {* @{term my_constant :: my_type#} *}
text {* @{term my_constant :: my_type#} *}
I think the second form is not proper templating yet, just an escape hatch
of the IDE to produce balanced quotes by default, since it is more often
correct that the other way round.
The Isabelle text cartouches are an attempt to get rid of unbalanced
quotes altogether, and reduce the problem to one of balanced parentheses.
My ` completion is already better than the above, because it allows to
select all 3 cases: balance template, left side, right side.
jEdit has already nice actions to select a code block, depending on the
structure of parentheses. What is missing are ways to add or remove an
outermost pair of parentheses, which should not be too difficult to add.
Independently of code blocks, the Isabelle/jEdit actions to modify control
symbols already work with selections in a structured way. The completion
mechanism also knows a bit about the various forms of selection, and tries
to do something sensible with them.
The abobe example could be also handled by a double-click to select the
word of my_constant, and then perform a still hypothetical operation to
enclose it in quotes of some form.
Note that when I say jEdit it refers to the jEdit text editor, while the
Prover IDE is called Isabelle/jEdit. Getting the basic terminology right
helps to avoid confusion about what happens where, and who is ultimately
responsible for it.
We have an increasingly complex situation of many Isabelle sub-languages
and sub-systems, but being explicit about that is better than sweeping it
under the carpet. In contrast, the Coq guys have upheld the illusion of
one main language longer, and actually removed their quotes around the
term language long ago, and thus introduced many problems that persist
until today.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
