Re: [isabelle-dev] simplifier trace (and jedit)

2012-05-25 Thread Makarius

On Thu, 24 May 2012, Christian Sternagel wrote:

The Prover Session panel has check/cancel buttons that are reminiscent 
of manual control in PG. The keyboard shortcuts are C-SPACE and 
C-BACKSPACE, respectively. You need to avoid rash movements after 
cancelation, outerwise the checking process restarts.


I overlooked those, thanks! Unfortunately, this does not work very well 
(or maybe I misunderstood the intended way of use). I don't see the 
purpose of Check, since it seems that as soon as I start typing again, 
asynchronous checking does start anyway.


Normally the implicit execution process follows the perspective of the 
editor, i.e. the set of visible text ranges.  So when you move around and 
expose more text, it causes updates on the perspective (edits) and 
eventual checking.


The Check button or C-SPACE key pretends that the whole buffer is 
visible, and thus commences its full checking until you change the 
perspective again.


Eventually, I would like to make this yet more declarative, with some 
properties to control the checking process of the session, say to assert 
that a certain subgraph of the current session is processed continously.



While clicking on Cancel does not always cancel the process (or maybe 
there is just a huge delay, since the trace is so big; anyway the result 
is that jedit becomes unresponsive and I basically have to kill it).


This could well be.  The protocol is asynchronous and maximizes 
throughput, without any flow control.  So the prover can easily cause 
denial-of-service of the front-end side.


After all these years with this fundamental problem of high-volume traces, 
I think I now know how to avoid it in the first place.  The idea is to 
pause prover transactions in certain situations, say after a certain 
amount of tracing messages have been output.  The user then needs to react 
on it, by clicking somewhere in the Output window, or entering some text 
in an input field.


This could work via Future.promise/fulfill in a similar way like the 
Invoke_Scala.method function in Isabelle/ML.  This works, because the 
documen model is inherently multi-threaded.



The keyboard shortcuts do not work for me, C-SPACE is already in use in 
my GNOME, so I know why this does not work, but C-BACKSPACE apparently 
does backwards deletion of a word inside jedit; I'll check whether this 
works when I set different keyboard shortcuts).


It is C-E SPACE and C-E BACKSPACE, and a bit too close to 
ESCAPE-META-ALT-CONTROL-SHIFT.  C-E is a common jEdit prefix for certain 
extended key sequences.


See also the jEdit Shortcuts options in the Plugin: Isabelle section.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] simplifier trace (and jedit)

2012-05-23 Thread Tobias Nipkow
Am 23/05/2012 06:15, schrieb Christian Sternagel:
 - in the [1]Rewriting: messages, we actually just see the redex and the
 contractum, but not the context of a rewrite step. Why not show the whole 
 terms?
 (One reason against this is the high redundancy and potentially huge size of
 such traces, but on the other hand, they are traces and only generated when
 requested.)

Size is indeed an issue, but also that it would be a considerable amount of work
to implement it properly. Ideally you want an interactive tracer anyway, which
is yet more work.

Tobias
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] simplifier trace (and jedit)

2012-05-23 Thread Makarius

On Wed, 23 May 2012, Christian Sternagel wrote:

3) Furthermore, in my course I recommend students (which know about term 
rewriting before) to have a look at the simplifier trace whenever the 
simplifier does something unexpected or does not terminate. However, for 
the latter use-case (i.e., finding cause of nontermination) I do not 
even know how to do it myself in jedit. As soon as I write, e.g., apply 
simp the simplifier starts to loop, if I don't delete the command it 
continues looping (and thus the whole system becomes highly unresponsive 
very soon), if I delete the command, the trace is gone too. Is there any 
way (or workaround), such that I can generate (part of) the trace of a 
(potentially) looping reduction.


The Prover Session panel has check/cancel buttons that are reminiscent of 
manual control in PG.  The keyboard shortcuts are C-SPACE and C-BACKSPACE, 
respectively.  You need to avoid rash movements after cancelation, 
outerwise the checking process restarts.



Maybe giving a timeout to apply simp (but I don't know whether or how 
this is possible) does work?


Long-running commands are generally bad for reactivity.  Using timeouts 
with some kind of iterative deepening of the amount of checking might help 
here.  It is one of the many fine points in the scheduling that can be 
improved beyond the received PG/TTY model, so that manual cancelation can 
be discontinued altogether at some point.



Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] simplifier trace (and jedit)

2012-05-23 Thread Christian Sternagel

On 05/23/2012 10:38 PM, Makarius wrote:

On Wed, 23 May 2012, Christian Sternagel wrote:


3) Furthermore, in my course I recommend students (which know about
term rewriting before) to have a look at the simplifier trace whenever
the simplifier does something unexpected or does not terminate.
However, for the latter use-case (i.e., finding cause of
nontermination) I do not even know how to do it myself in jedit. As
soon as I write, e.g., apply simp the simplifier starts to loop, if
I don't delete the command it continues looping (and thus the whole
system becomes highly unresponsive very soon), if I delete the
command, the trace is gone too. Is there any way (or workaround), such
that I can generate (part of) the trace of a (potentially) looping
reduction.


The Prover Session panel has check/cancel buttons that are reminiscent
of manual control in PG. The keyboard shortcuts are C-SPACE and
C-BACKSPACE, respectively. You need to avoid rash movements after
cancelation, outerwise the checking process restarts.
I overlooked those, thanks! Unfortunately, this does not work very well 
(or maybe I misunderstood the intended way of use). I don't see the 
purpose of Check, since it seems that as soon as I start typing again, 
asynchronous checking does start anyway. While clicking on Cancel does 
not always cancel the process (or maybe there is just a huge delay, 
since the trace is so big; anyway the result is that jedit becomes 
unresponsive and I basically have to kill it). (The keyboard shortcuts 
do not work for me, C-SPACE is already in use in my GNOME, so I know why 
this does not work, but C-BACKSPACE apparently does backwards deletion 
of a word inside jedit; I'll check whether this works when I set 
different keyboard shortcuts).


cheers

chris
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] simplifier trace (and jedit)

2012-05-22 Thread Thomas Sewell
The _2 v.s. (2) thing is just silly. It's in find_theorems output too. 
It's just the way theorems get their names - probably one of these 
decisions made years ago and not compatible with Makarius' decisions 
about how to fetch theorems in Isar.


Adding context information to every reduction sounds too big in most 
cases - both for human consumption and for processing by fragile 
processes like ProofGeneral. I agree with you though that context can be 
hard to follow.


As for (simp only: ) vs unfolding - your rule is of the form Not (Suc 
nat = 0) which the simplifier preprocesses into (Suc nat = 0) == 
False but which the naive unfolder processes as (Not (Suc nat = 0)) == 
True. That is, without further setup, the rule is not really an 
unfoldable rule.


Yours,
Thomas.

On 23/05/12 14:15, Christian Sternagel wrote:

Dear all,

I wanted to write this already a long time ago (prompted by an Isabelle
course I gave) but somehow forgot about it. Now I had a look at my
slides again and was reminded.

1) The first thing is rather subjective, but maybe you could comment on
it. I think the simplifier trace would be less surprising for newbies
and slightly easier to read if
- names of rewrite rules would be printed in their original form.
Consider, e.g., the trace resulting from

lemma Suc 0 + 0 = 0
  using [[simp_trace]]
  apply simp

where we have (among others)

[1]Applying instance of rewrite rule Nat.nat.distinct_2:
Suc ?nat'2 = 0 ≡ False

Why not use the real name Nat.nat.distinct(2) in the trace (Okay,
the rule was preprocessed by the simplifier, but still, as far as I
can tell the printed name does not exist)?

- in the [1]Rewriting: messages, we actually just see the redex and
the contractum, but not the context of a rewrite step. Why not show the
whole terms? (One reason against this is the high redundancy and
potentially huge size of such traces, but on the other hand, they are
traces and only generated when requested.)

2) Some questions concerning the trace:
- When I explicitly use a single rule by unfolding rule-name, why is
there more in the trace than just the application of this rule?

- Why does apply (simp only: rule) and unfolding rule behave
differently? E.g., on the term Suc 0 = 0 with rule
Nat.nat.distinct(2) the former results in False, whereas the latter
does nothing. Is it important that those two commands behave differently?

3) Furthermore, in my course I recommend students (which know about term
rewriting before) to have a look at the simplifier trace whenever the
simplifier does something unexpected or does not terminate. However, for
the latter use-case (i.e., finding cause of nontermination) I do not
even know how to do it myself in jedit. As soon as I write, e.g., apply
simp the simplifier starts to loop, if I don't delete the command it
continues looping (and thus the whole system becomes highly unresponsive
very soon), if I delete the command, the trace is gone too. Is there any
way (or workaround), such that I can generate (part of) the trace of a
(potentially) looping reduction. Maybe giving a timeout to apply simp
(but I don't know whether or how this is possible) does work?

cheers

chris
___
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