Email Gateway (Aug 19 2022 at 15:08): Email Gateway (Aug 19 2022 at 15:08):From: Peter Lammich <lammich@in.tum.de>
Here is a list of issues that I encountered with RC1:
If a lemma is not properly closed, ie. the done or qed is missing,
the next command only issues a warning and recovers the state. As
warnings are omnipresent in Isabelle, it is very hard to spot such
places when
developing a theory. This leads to garbage accumulating in theory
files and probably only being discovered upon batch-build.
This feature may also cause surprises on bigger isar proofs, where it
is (in particuar as code-fold does not work) too easy to forget a qed.
In the output buffer, the standard Ctrl-Ins for "copy" does not work,
while it works in the main text area. Can these shortcuts be configured
separately? Or do I have to live with Ctrl-C?
Odd behaviour when focus lays in output buffer or any other panel:
Cursor movement and entering newlines still goes to the text area, but
other keyboard input goes to the panel (and may or may not be
interpreted there). The only indication for this is a slightly changed
color of the cursor in the main window.
No indentation feature. It is hard to keep track of big proofs and
indent them correctly, in particular as code-folding does not work
reliably.
In PG, there was a nice auto-indentation feature that worked reliable
for (almost) all cases.
When developing proofs:
The output window displays the current position
by default ... if you are typing a new command, it usually displays
"Syntax error".
However, while typing your next method/isar step, you usually want to
see the current goal state, not a the completely useless information
"syntax error".
In PG, the output was not updated before you explicitely processed
the command. Maybe, this can be simulated by turning auto-update off
and bind update to a convenient shortcut.
Email Gateway (Aug 19 2022 at 15:08):From: Lars Noschinski <noschinl@in.tum.de>
And a completion-related one: In a string context in a ML-context,
symbol completion is enabled. So, changing
setup {*
ML_Antiquotation.inline @{binding fundef} (Scan.succeed "raise Undefined")
*}
to
setup {*
ML_Antiquotation.inline @{binding fundef} (Scan.succeed "fn _ => raise
Undefined")
*}
yields
setup {*
ML_Antiquotation.inline @{binding fundef} (Scan.succeed "fn _ ⇒ raise
Undefined")
*}
instead with the default (immediate completion) settings.
Email Gateway (Aug 19 2022 at 15:08):From: Lars Noschinski <noschinl@in.tum.de>
Hi,
Here is a list of issues that I encountered with RC1:
Another issue I encountered with RC1 today (I didn't encounter the issue
with RC0, but my usage intensity might have been to low): I modified
some file (in a ML block), did some jumping around (through other
buffers), came back to the changed line and didn't see the change
anymore. I redid the change, which lead to an error message which made
it clear that the system saw something else than I was seeing in the
buffer. I reloaded the buffer and the error went away.
I haven't found a way to reproduce it yet.
BTW: Does someone know a software which is able to record the last n
minutes of a window (basically a screen recorder with a ring buffer)? I
often thought this would be helpful to describe these kind of issues.
-- Lars
Email Gateway (Aug 19 2022 at 15:08):From: Lars Noschinski <noschinl@in.tum.de>
And yet another issue: A method executing
error ""
produces an error marker in the right sidebar. However, the associated
apply command does not get underlined in red and the error marker in the
left sidebar is missing.
Reproduce with:
theory Scratch imports Pure begin
lemma "PROP P"
apply (tactic {* error "" *})
oops
end
Email Gateway (Aug 19 2022 at 15:08):From: Ondřej Kunčar <kuncar@in.tum.de>
And you can't see the error in the Output panel either.
Email Gateway (Aug 19 2022 at 15:08):From: Lars Noschinski <noschinl@in.tum.de>
Indeed. All of this is different to
ML {* error "" *}
which at least produces an empty red line as output (and thus gets the
other markers, too).
BTW: I always use(d) "error """ the way one uses "undefined" in Haskell.
The following construct (which Makarius showed me at ITP) is a bit nicer
(you get a trace and can jump to the location of the error), but
requires a few lines of initial setup:
signature UTIL = sig
exception Undefined
val setup : theory -> theory
end
structure Util : UTIL = struct
exception Undefined
val setup =
ML_Antiquotation.inline @{binding undef} (Scan.succeed "raise
Util.Undefined")
#> ML_Antiquotation.inline @{binding fundef} (Scan.succeed "fn _ =>
raise Util.Undefined")
end
BTW2: I assume there is no easy way to make Isabelle/ML accept ⊥ instead
of @{undef}?
-- Lars
Email Gateway (Aug 19 2022 at 15:09):From: Peter Lammich <lammich@in.tum.de>
An another feature request:
The sidekick panel is supposed to show an overview of the theory.
At the top-level of the hierarchy, you can see the first lines of lemma,
definition, etc commands, which may or may not contain useful
information. In the worst case, you just see "lemma" or "definition".
It is even worse if you look under a lemma command. This looks like:
+lemma
|- using
|- case
|- proof
|- apply
|- apply
|- done
|- qed
i.e., almost completely useless information.
The information that might be useful, i.e. the name and the proposition
of the lemma, is displayed nowhere!
Attached is a screenshot from a current development of mine, that
illustrates the problem.
shot.png
Email Gateway (Aug 19 2022 at 15:09):From: Makarius <makarius@sketis.net>
On Wed, 30 Jul 2014, Peter Lammich wrote:
- If a lemma is not properly closed, ie. the done or qed is missing, the
next command only issues a warning and recovers the state. As warnings
are omnipresent in Isabelle, it is very hard to spot such places when
developing a theory. This leads to garbage accumulating in theory
files and probably only being discovered upon batch-build.
That is actually a contribution in Isabelle2014 to make error recovery a
bit more useful, without doing the real job of (sub)structural checking
yet.
What do you mean by "warnings are omnipresent in Isabelle"? The prover
IDE shows them more prominently than in the TTY past, but that could be
taken as motivation to remove the reasons for warnings. Not all such
spots are bad, but an avarage theory normally has only few warnings.
- In the output buffer, the standard Ctrl-Ins for "copy" does not work,
while it works in the main text area. Can these shortcuts be configured
separately? Or do I have to live with Ctrl-C?
I did not know about Ctrl-Ins yet. What you observe here is merely the
known and documented difference of the main jEdit text area with its
actions and shortscuts vs. regular Java Swing GUI components. The latter
only have basic Ctrl-C, and it actually works routinely, which is a big
step forwards to the historic perspective.
If Ctrl-C does not work somewhere, it is actually an issue that needs to
be addressed.
- Odd behaviour when focus lays in output buffer or any other panel:
Cursor movement and entering newlines still goes to the text area, but
other keyboard input goes to the panel (and may or may not be
interpreted there). The only indication for this is a slightly changed
color of the cursor in the main window.
This belongs to normal jEdit policies. In Isabelle/jEdit for the coming
release I added the faint cursor to emphasize that -- normally it would be
just absent.
- No indentation feature. It is hard to keep track of big proofs and
indent them correctly, in particular as code-folding does not work
reliably.In PG, there was a nice auto-indentation feature that worked reliable
for (almost) all cases.
That is indeed a notable omission. In 1998, I added indentation to PG 2.x
quite early, and earned the name "The indentation Man" in the inner circle
of PG developers. In Isabelle/jEdit the lack of it has become a running
gag over the years: it needs to come one day, but so far I just wanted to
evade the wrath of users when the Prover IDE suddenly makes standard
indentation of Isar text by default.
- When developing proofs:
The output window displays the current position
by default ... if you are typing a new command, it usually displays
"Syntax error".
However, while typing your next method/isar step, you usually want to
see the current goal state, not a the completely useless information
"syntax error".In PG, the output was not updated before you explicitely processed
the command. Maybe, this can be simulated by turning auto-update off
and bind update to a convenient shortcut.
Nothing new about this observation. It belongs to general mismatch of
TTY/PG mechanics wrt. the document-oriented model. Note that you can also
use the Query panel to print proof states on demand and only on demand.
Makarius
Email Gateway (Aug 19 2022 at 15:09):From: Makarius <makarius@sketis.net>
Why is that an issue? The language context switches symbols on for ML
strings and comments, since both might use them.
The examples shown here are about embedded ML code, which is not really
the normal use of strings.
In general, the "guess what I mean" functionality of the system will
occasionally guess wrong. It is sometimes hard to get the defaults right,
but so far I don't see an indication to change them in this case.
Makarius
Email Gateway (Aug 19 2022 at 15:09):From: Makarius <makarius@sketis.net>
That is an interesting boundary case, but it is the same in
Isabelle2013-2 an no regression. It remains to be seen if it is an actual
problem.
The invocation of error "" is the same as raise ERROR "", which makes the
ML code fail and the Isar toplevel wrapper print the exeptions. The error
message is empty, which means it is vacous according to ancient Isabelle
traditions, which hold until today. The effect was not visible in the old
TTY times, because that adds a prefix of "*** " by default. Note that
there are other situations where ML failure might lead to no error output,
notably involving Exn.Interrupt.
Such non-printing exceptions should not show up under normal circumstances
-- they indicate a programming mistake somewhere.
The "implementation" manual explains the difference of user ERROR vs.
system Fail exceptions explicitly. The error function / ERROR exception
always had the implicit assumption that messages are non-empty, as a
proper human-readable message.
For your application of a meaningless ad-hoc failure, you could raise
Fail "" or even raise Match (which are both printed as usual). The
"undefined" function also does the latter.
Makarius
Email Gateway (Aug 19 2022 at 15:10):From: Makarius <makarius@sketis.net>
We need to keep an eye (or more) on this. I've seen myself a situation
some weeks ago were some ML_file was somehow out of sync.
Makarius
Email Gateway (Aug 19 2022 at 15:10):From: Makarius <makarius@sketis.net>
On Wed, 30 Jul 2014, Lars Noschinski wrote:
BTW: I always use(d) "error """ the way one uses "undefined" in Haskell.
The following construct (which Makarius showed me at ITP) is a bit nicer
(you get a trace and can jump to the location of the error), but
requires a few lines of initial setup:signature UTIL = sig
exception Undefined
val setup : theory -> theory
endstructure Util : UTIL = struct
exception Undefined
val setup =
ML_Antiquotation.inline @{binding undef} (Scan.succeed "raise
Util.Undefined")
#> ML_Antiquotation.inline @{binding fundef} (Scan.succeed "fn _ =>
raise Util.Undefined")end
After that ITP session, I recalled the more basic "raise Match" idiom, but
could not tell you about it. That is sufficiently short to be used
literally.
I assume there is no easy way to make Isabelle/ML accept ⊥ instead of
@{undef}?
That is the old questions how much of actual Standard ML we have in
Isabelle/ML. There is still the claim that there is no fundamental
difference, apart from antiquotations, although many delicate details have
accumulated over the years.
In the past, people have occasionally proposed actual syntactic
variations, like an actual arrow for fun/fn/case => like in Isabelle/HOL
notation, but I always tried to keep the divergence from actual SML in
check.
Technically, the token language could be "embraced and extended" further,
but I think fringe languages like ML should stay as faithful to their own
standards as possible. BTW, with symbols inside ML, the question of
language context will show up again: You would probably expect completion
for \<bottom>, but not for =>.
Makarius
Email Gateway (Aug 19 2022 at 15:10):From: Makarius <makarius@sketis.net>
On Wed, 30 Jul 2014, Peter Lammich wrote:
The sidekick panel is supposed to show an overview of the theory.
At the top-level of the hierarchy, you can see the first lines of lemma,
definition, etc commands, which may or may not contain useful
information. In the worst case, you just see "lemma" or "definition".It is even worse if you look under a lemma command. This looks like:
+lemma
|- using
|- case
|- proof
|- apply
|- apply
|- done
|- qedi.e., almost completely useless information.
The enumeration of the commands as "sections" is indeed a bit pointless.
The main use of Sidekick / isabelle is for document structure, with
chapter / section / subsection outline etc. When writing Isabelle
documentation, papers, slides etc. I use that routinely to keep an
overview.
More logical structure could be done in many ways, I have this on my list
for several years already to be revisited eventually.
The information that might be useful, i.e. the name and the proposition
of the lemma, is displayed nowhere!
Depends how you write your source text. jEdit folds and Sidekick trees
assume that the first line provides the main information. This is also
the reason why I write definitions and theorem statements these days a bit
differently than in the past, when Proof General was still there.
Of course, one could replace SideKick by a quite different Preview panel
for the proof document with its relevant structural information, even
proof state output according to certain policies of incremental editing of
sub-proofs, not scripts. That is just speculative at the moment -- too
many marginal technical problems still in the way of bigger steps
forwards.
Makarius
Email Gateway (Aug 19 2022 at 15:11):From: Lars Noschinski <noschinl@in.tum.de>
On 30.07.2014 21:53, Makarius wrote:
What do you mean by "warnings are omnipresent in Isabelle"? The
prover IDE shows them more prominently than in the TTY past, but that
could be taken as motivation to remove the reasons for warnings. Not
all such spots are bad, but an avarage theory normally has only few
warnings.
Often, the "Ignoring duplicate rewrite rule/intro/..." warnings get
annoying, as they are not always meaningful (for example, overwriting
intro by intro! triggers a warning). In particular, in certain
locale-heavy theories (HOL-Algebra comes to mind), interpreting (or
opening) a locale gives you a number of these warning and there is not
always a (nice) way around them (I'd even claim that these warnings are
mostly vacuous for theory interpretations, but this is another topic).
I had some theories where these warnings were common enough to obscure
the real ones.
Nothing new about this observation. It belongs to general mismatch of
TTY/PG mechanics wrt. the document-oriented model. Note that you can
also use the Query panel to print proof states on demand and only on
demand.
On the topic of the query panel: Some time in the future, I'd like to
see the equivalent of the jEdit action bar (or, to phrase it
differently, a "general" query panel) for Isabelle, where I enter an
arbitrary (diagnostic) command and get the output in the panel.
BTW: I just discovered that symbol completion works now in the
text-boxes in the panels, very nice!
-- Lars
Email Gateway (Aug 19 2022 at 15:11):From: Peter Lammich <lammich@in.tum.de>
What do you mean by "warnings are omnipresent in Isabelle"? The prover
IDE shows them more prominently than in the TTY past, but that could be
taken as motivation to remove the reasons for warnings. Not all such
spots are bad, but an avarage theory normally has only few warnings.
I mean that there are many warnings in my theories, usually from the
simplifier/classical reasoner that inform me that I have added rules
that were already present in the simpset/claset (including the spurious
warning when using intro! for an [intro] - rule).
Thus, in my case, it is difficult to write theories without warnings, or
to manually check every single warning whether it is bad (garbage in the
theory) or not (just some spurious simplifier warning).
The surprise will probably come in batch-build mode, as this will be the
time when the garbage will make problems.
I'm already looking forward to the tutorials of the semantics-lecture,
where students will definitely hand in lots of unfinished lemmas, many
of them convinced they actually have proven it ...
In PG, or even in older isabelle/jedits, I could just give them the rule
of thumb: Your theory must not contain errors, sorrys, or oops.
Also, I will have hard times checking the submissions, as I have to
manually check every warning to see wether the proof is actually
closed ...
- In the output buffer, the standard Ctrl-Ins for "copy" does not work,
while it works in the main text area. Can these shortcuts be configured
separately? Or do I have to live with Ctrl-C?I did not know about Ctrl-Ins yet. What you observe here is merely the
known and documented difference of the main jEdit text area with its
actions and shortscuts vs. regular Java Swing GUI components. The latter
only have basic Ctrl-C, and it actually works routinely, which is a big
step forwards to the historic perspective.If Ctrl-C does not work somewhere, it is actually an issue that needs to
be addressed.
Looks like I have to lower my expectations to modern user interfaces.
One of these expectations is full configurability, not forcing the user
to some fixed shortcuts that, depending on typing habits, may or may not
be convenient. Btw: the "old-fashioned" "ancient" emacs is fully
configurably in the above sense!
- Odd behaviour when focus lays in output buffer or any other panel:
This belongs to normal jEdit policies. In Isabelle/jEdit for the coming
release I added the faint cursor to emphasize that -- normally it would be
just absent.
Ok, maybe its a jEdit feature. Personally, I find it very odd and I have
hard times getting used to it: Whenever I used a query/sledgehammer
panel, I regularly forget to click into the text-area before typing ...
In PG, there was a nice auto-indentation feature that worked reliable
for (almost) all cases.That is indeed a notable omission. In 1998, I added indentation to PG 2.x
quite early, and earned the name "The indentation Man" in the inner circle
of PG developers.
It was a very useful feature, and I'm really missing it. As code-folding
also does not work, there is currently no feature that assists in
keeping track of the structure of big developments.
- When developing proofs:
The output window displays the current position
by default ... if you are typing a new command, it usually displays
"Syntax error".
However, while typing your next method/isar step, you usually want to
see the current goal state, not a the completely useless information
"syntax error".In PG, the output was not updated before you explicitely processed
the command. Maybe, this can be simulated by turning auto-update off
and bind update to a convenient shortcut.Nothing new about this observation. It belongs to general mismatch of
TTY/PG mechanics wrt. the document-oriented model. Note that you can also
use the Query panel to print proof states on demand and only on demand.
Let's hope I can bind these thing to some shortcuts ...
Email Gateway (Aug 19 2022 at 15:11):From: Peter Lammich <lammich@in.tum.de>
The question is "why are these errors/interrupts not visible?"
As discussed earlier on this list, they make false theorems look as if
proven, when the proof tactics contain an programming error (or fail due
to a bug in the parallel proof scheduling). This behaviour is contrary
to the spirit of LCF-provers. Moreover, if those things are programming
mistakes and should not show up under normal circumstances anyway, there
is no point in not highlighting them as an error.
Email Gateway (Aug 19 2022 at 15:11):From: Peter Lammich <lammich@in.tum.de>
My main restriction when writing proof text comes from the document
generation to latex, where I want a readable layout. And this forces me
to have no lines longer than roughly 80 characters. As I have many
longer lemma statements, I need to format them manually into multiple
lines.
Email Gateway (Aug 19 2022 at 15:11):From: Peter Lammich <lammich@in.tum.de>
I think this was called "issue prover command" in PG ("Ctrl-c v" in
standard config), and I used it from time to time. It only worked for
commands that did not change the prover state, e.g., for all diagnostic
commands.
In jEdit this has been replaced by the more heavyweight query-panels,
that only work for a small subset of the diagnostic commands, and
extending them to new commands is quite a big effort. So I would also
like to have this lightweight low-level possibility of issuing
diagnostic-commands, in addition to the heavyweight, high-level query
panels.
Email Gateway (Aug 19 2022 at 15:11):From: Lars Noschinski <noschinl@in.tum.de>
Take it as a data point for the long-term considerations about symbol
completion.
But there is also something not totally smooth outside of strings:
Yesterday, I occasionally had symbols complete in normal ML-code
(outside of strings; in a ML-block in a theory file). Typically, this
seemed to occur when I was typing pretty fast and changing the structure
of the code. It seemed unrelated to string literals.
One way to trigger this is placing the cursor directly after the closing
} of an antiquotation and typing a symbol fast. I can even type a few
spaces before typing the symbol and it will still get completed.
-- Lars
Email Gateway (Aug 19 2022 at 15:11):From: Lars Hupel <hupel@in.tum.de>
This would also greatly reduce the number of stray "thm" commands in our
theory sources (as in
<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-July/msg00239.html>)
:-)
Email Gateway (Aug 19 2022 at 15:20):From: Lars Noschinski <noschinl@in.tum.de>
An issue with symlinks:
Given file a file "/home/lars/projekte/test.ML" and symlink
"/home/lars/P" to "projekte" and a theory
theory Scratch imports Pure
begin
ML_file "/home/lars/P/test.ML"
end
Then a click on the file name will open the correct file, but without
any annotations.
Email Gateway (Aug 19 2022 at 15:21):From: Lars Noschinski <noschinl@in.tum.de>
A type error in a ML_file disables ctrl+click and hovering for type
annotations. Errors and warnings are still present. This behaviour does
not occur in a ML block.
(Don't know whether this is a regression).
Email Gateway (Aug 19 2022 at 15:27):From: Lars Noschinski <noschinl@in.tum.de>
An issue with the precedence of warnings and errors:
Under certain circumstances, if a method emits a warning and the apply
fails (with an error), the line is only marked as a warning in the
theories panel and the right side bar.
Reconstruct with:
theory Scratch imports Main begin
method_setup foo = ‹
Scan.succeed (fn ctxt => SIMPLE_METHOD' (warning "warning"; tracing
"trace"; K no_tac))
›
lemma P apply foo
end
-- Lars
Email Gateway (Aug 19 2022 at 15:32):From: Makarius <makarius@sketis.net>
On Thu, 31 Jul 2014, Peter Lammich wrote:
The invocation of error "" is the same as raise ERROR "", which makes the
ML code fail and the Isar toplevel wrapper print the exeptions. The error
message is empty, which means it is vacous according to ancient Isabelle
traditions, which hold until today. The effect was not visible in the old
TTY times, because that adds a prefix of "*** " by default. Note that
there are other situations where ML failure might lead to no error output,
notably involving Exn.Interrupt.Such non-printing exceptions should not show up under normal circumstances
-- they indicate a programming mistake somewhere.The question is "why are these errors/interrupts not visible?"
Interrupts are not program errors, but physical events. The
"implementation" manual explains the difference in the important section
0.5, with clear guidelines how user-space tools need to work with
interrupts, such that there are passed-through the code unhindered. The
system uses interrupts internally in various ways to manage executions,
but for this to work the user-space code needs to be done right.
ERROR "" used to be a semantic ML programming error until yesterday, when
I incorporated the concept into the "user error" notion to simplify life.
Regular Isabelle sources never suffered from that mistake in the past
decades to the best of my knowledge, but there is no problem here to make
the system more resiliant against improper use and declare it proper. So
in the next Isabelle2014-RC1 the error message will be "Error", both in ML
and Scala.
Nonetheless, it is important that Isabelle/ML users read the
implementation manual carefully, and more than just once in a life-time.
As discussed earlier on this list, they make false theorems look as if
proven, when the proof tactics contain an programming error (or fail due
to a bug in the parallel proof scheduling). This behaviour is contrary
to the spirit of LCF-provers.
The LCF approach in its strict sense is based on sucessully produced
values of some abstract datatype of theorems, not the absence of
user-level errors.
There is a general problem to ensure that errors actually reach the
end-user -- despite continuous efforts to make this as robust as feasible,
there are routinely situations where messages get dropped, e.g. by odd
Java/Swing GUI components.
This inherent unreliability of prover interfaces is well-known, it was the
same in the old days of Proof General.
The only official authentic check is a batch build.
Makarius
Email Gateway (Aug 19 2022 at 15:34):From: Makarius <makarius@sketis.net>
Semantic completion (i.e. the language context) works via the asynchronous
document model, so typing fast means the physical editor state and the
document markup range may disagree.
These delays are system options that may be adjusted as usual: most
notably editor_input_delay and editor_output_delay. Maybe you want to try
these by a factor of 5 or 10 faster -- results also depend on the amount
of CPU cycles you can spend on interactive document processing and GUI
rendering.
Makarius
Email Gateway (Aug 19 2022 at 15:36):From: Makarius <makarius@sketis.net>
That is a consequence of the redirection of ML reports for external files,
which reuses the asynchronous print infrastructure that I had presented at
ITP2014 in order to swap-in and swap-out massive IDE markups on demand.
By making the print function non-strict wrt. the main eval phase, it can
report static results even in the presence of failure: see d5b0fa6f1f7a,
or the next release candidate.
Makarius
Email Gateway (Aug 19 2022 at 15:38):From: Richard Molitor <gattschardo@googlemail.com>
And yet another issue: A method executing
error ""
produces an error marker in the right sidebar. However, the associated
apply command does not get underlined in red and the error marker in the
left sidebar is missing.
Reproduce with:
theory Scratch imports Pure begin
lemma "PROP P"
apply (tactic {* error "" *})
oops
end
Email Gateway (Aug 19 2022 at 15:40):From: Makarius <makarius@sketis.net>
The prover will open the wrong file, i.e. the one that is stored on the
file-system, instead of taking the buffer content from the editor as
expected. After some editing of the buffer, the divergence will become
apparant. The lack of detailed markup is a consequence of not going
through PIDE.
The superficial reason for that is a small mistake how PIDE document node
names are produced, with a disagreement about canonical forms due to
symblinks. This will work in the next release candidate.
The deeper problem is a confusion about responsibilities: the prover still
accesses the file-system as a fall-back, when the Prover IDE did not do
that. Thus mistakes in providing file content are silently turned into
unintended behaviour.
As explained earlier, this mixed responsibility is there to allow
Isabelle/HOL itself to be edited interactively on a small mobile device of
only 4--8 GB.
Makarius
Email Gateway (Aug 19 2022 at 15:42):From: Makarius <makarius@sketis.net>
It should we OK in the right side bar -- according to
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg05328.html
from May 2014. Back then I somehow forgot to apply the analogous change to
the theories panel as well.
My comment from that thread on isabelle-dev about the difficulty to pin
down the notion of "command status" still applies: the Prover IDE merely
visualizes certain aspects of very rich information; sometimes it might
come out in a misleading way.
Makarius
Email Gateway (Aug 19 2022 at 15:42):From: Makarius <makarius@sketis.net>
On Thu, 31 Jul 2014, Peter Lammich wrote:
On the topic of the query panel: Some time in the future, I'd like to
see the equivalent of the jEdit action bar (or, to phrase it
differently, a "general" query panel) for Isabelle, where I enter an
arbitrary (diagnostic) command and get the output in the panel.I think this was called "issue prover command" in PG ("Ctrl-c v" in
standard config), and I used it from time to time. It only worked for
commands that did not change the prover state, e.g., for all diagnostic
commands.
Such a mini command-line within Query is an obvious extension, but there
are also conceptual differences. There is no need to restrict it to
diagnostic command, because it is all stateless anyway. There is a need
to wrap up the hypothetical "script" a bit differently, to avoid spilling
of messages (wranings etc.) in the wrong place. This is why it is not
done yet -- the panel is new in the coming release anyway.
In jEdit this has been replaced by the more heavyweight query-panels
Again, and hopefully the last time, a quote from the Isabelle/jEdit
manual:
\item [jEdit] is a sophisticated text editor implemented in Java
\item [Isabelle/jEdit] is the main example application of the PIDE
framework and the default user-interface for Isabelle
If you need a short name for the Prover IDE, you can say "PIDE" -- it is
even easier to pronounce (and spell) than "jEdit". Yet another
alternative is to say just "Isabelle", according to the toplevel
application name.
Concerning the perceived heavyweightedness of the query panel: it is
actually relative simple, taking the whole conceptual complexity of
timeless/stateless asynchronous parallel document processing into account.
In contrast, issuing a single command on the spot is only simple under the
assumption of an existing TTY loop, which has its own complexities. Once
the TTY loop can be removed from Isabelle, great weights will disappear
from the overall system implementation.
that only work for a small subset of the diagnostic commands, and
extending them to new commands is quite a big effort.
The query panel is based on a general concept of query operation, which
are more flexible than old-style diagnostic commands, but also simpler.
The "Print Context" tab in the Query panel is a restricted application of
the general principle. The following one-liner installs a new item to be
printed there (without taking any arguments apart from the implicit
state):
ML ‹
Print_Operation.register "test" "test output" (fn st => [Pretty.str "test"])
›
After emitting that ML snippet in PIDE, the Query panel needs to be
re-docked and will then show another checkbox for "test" than can be
activated on demand.
Makarius
Email Gateway (Aug 19 2022 at 15:42):From: Makarius <makarius@sketis.net>
Keeping lines short (80-100 chars for source, 60-70 chars for LaTeX
documents) is important, but it is still possible to put relevant
information into the head-line of a fold or sidekick item, e.g. like this:
lemma name: short_statement
<proof>
lemma name:
long_statement
<proof>
definition name :: type_constraints
where short_definition
definition name :: type_constraints
where
short_definition
Proper support for folds is still missing, but the general side-conditions
for it are already given in jEdit.
Makarius
Email Gateway (Aug 19 2022 at 15:42):From: Makarius <makarius@sketis.net>
On Thu, 31 Jul 2014, Lars Noschinski wrote:
Often, the "Ignoring duplicate rewrite rule/intro/..." warnings get
annoying, as they are not always meaningful (for example, overwriting
intro by intro! triggers a warning). In particular, in certain
locale-heavy theories (HOL-Algebra comes to mind), interpreting (or
opening) a locale gives you a number of these warning and there is not
always a (nice) way around them (I'd even claim that these warnings are
mostly vacuous for theory interpretations, but this is another topic).
This touches general questions about these particular historic warnings.
Many other tools have already become smarter concerning relevance of
messages. It is a long term effort to sort this out further.
The is already Context_Position.is_visible for tools to check if the
situation is right for warnings. The system does not always maintain that
properly though, and many tools ignore it.
BTW: I just discovered that symbol completion works now in the
text-boxes in the panels, very nice!
Did this behaviour change wrt. Isabelle2013-2? It should be mostly the
same as before.
Makarius
Email Gateway (Aug 19 2022 at 15:42):From: Makarius <makarius@sketis.net>
On Thu, 31 Jul 2014, Peter Lammich wrote:
Thus, in my case, it is difficult to write theories without warnings, or
to manually check every single warning whether it is bad (garbage in the
theory) or not (just some spurious simplifier warning).The surprise will probably come in batch-build mode, as this will be the
time when the garbage will make problems.I'm already looking forward to the tutorials of the semantics-lecture,
where students will definitely hand in lots of unfinished lemmas, many
of them convinced they actually have proven it ...
In PG, or even in older isabelle/jedits, I could just give them the rule
of thumb: Your theory must not contain errors, sorrys, or oops.Also, I will have hard times checking the submissions, as I have to
manually check every warning to see wether the proof is actually closed
...
First note that I have changed the regular warning to an error_message in
https://bitbucket.org/isabelle_project/isabelle-release/commits/ae3eac418c5f
so it will be in the text release candidate. Hopefully people will
actually test all that has accumulated.
In general, we have always had the following situation:
* Authentic checking of theories requires a batch build. It was never
easier than today to do that (see the "system" manual).
People sometimes "forget" to make a proper ROOT for their stuff, or
don't know how it is done or that it is important. Whenever someone
shows me some theories that are not just small snippets, my first
reflex is to do the missing "isabelle mkroot" and then the batch
build to see if they are correct.
* Proof General in the past and Prover IDE front-ends in the present are
only an approximation, with a lot of conveniences, but without the
full detail of checking.
Proof General even had quick_and_dirty on by default over most of its
life time, until that broke by accident in the 3.x to 4.x transition.
In situations where proper builds are too much for small experiments, it
is possible to use the new "isabelle console" together with plain use_thy
in raw ML (which is not Isabelle/ML); see also the "system" manual. Note
that the old "isabelle tty" is already removed, although there is still
"Isar.main()" to invoke the old toplevel.
If Ctrl-C does not work somewhere, it is actually an issue that needs
to be addressed.Looks like I have to lower my expectations to modern user interfaces.
One of these expectations is full configurability, not forcing the user
to some fixed shortcuts that, depending on typing habits, may or may not
be convenient.
There is nothing modern about Java/AWT/Swing -- it is in fact legacy for
many years -- like most other GUI frameworks. Swing does have a lot of
configurability, but a bit too much for my taste, and I don't really
understand most of it. jEdit has its own Swing add-ons and bypasses to
provide a quite sane environment.
For Isabelle/jEdit, I've spent extra care from the start to make
copy-paste work almost universally. I remember Proof General / Emacs as
something were this rarely worked on all platforms and all versions; I am
surprised that it is now perceived differently.
When Isabelle/jEdit was young and fresh in 2008/2009, there was a local
presentation of it at TUM. Someone asked: "What will be its main
features?" My spontaneous response: "reliable copy-paste".
It was a very useful feature, and I'm really missing it. As code-folding
also does not work, there is currently no feature that assists in
keeping track of the structure of big developments.
jEdit also has explicit folds with funny {{{ }}} notation.
Makarius
Email Gateway (Aug 19 2022 at 15:42):From: Makarius <makarius@sketis.net>
I have completed two rounds through the new auxiliary file management in
the Prover IDE, and robustified it wrt. various fine points. When the
next release candidate is published, please keep an extra eye on that
aspect.
Makarius
Email Gateway (Aug 19 2022 at 15:42):From: Lars Noschinski <noschinl@in.tum.de>
I'm pretty sure, my original case had it wrong on the right side bar,
too. But indeed, my test case doesn't exhibit this behaviour and I
cannot reproduce what I rememeber to have seen. I'll keep an eye on this.
Email Gateway (Aug 19 2022 at 15:43):From: Lars Noschinski <noschinl@in.tum.de>
What I meant is that I can place the cursor directly after the closing
brace, wait for an arbitrary amount of time (to give the system time to
converge), and still get symbol completion if I type fast at that point
(see attached video).
antiquotation-completion.mp4
Email Gateway (Aug 19 2022 at 15:44):From: Makarius <makarius@sketis.net>
That is still within the convergence model sketched here, but there is an
additional coincidence: completion sits right in the input event loop.
When you type something there is always an edit-distance, and the language
context of the closing delimiter is stretched into the new space. Unless
there is a completion delay, the semantic information needs to be
retrieved on the spot, but it can never be accurate.
You can see the same effect when you insert new material quickly at the
end of some semantically marked up token (e.g. a free or bound variable).
It does not matter so much there, since it is only a transient visual
glitch.
In the next round of completion refinement (not for this release), one
could try to mark only the interior with the specific language context,
not the delimiters.
Makarius
Email Gateway (Aug 19 2022 at 15:44):From: Lars Noschinski <noschinl@in.tum.de>
When writing more then a few lines of code, I prefer a separate
"undefined" value -- "raise Match" has a double meaning as telling the
compiler not to bother me with warnings about inexhaustive cases.
-- Lars
Email Gateway (Aug 19 2022 at 15:46):From: Lars Noschinski <noschinl@in.tum.de>
On 30.07.2014 22:14, Makarius wrote:
The invocation of error "" is the same as raise ERROR "", which makes
the ML code fail and the Isar toplevel wrapper print the exeptions.
The error message is empty, which means it is vacous according to
ancient Isabelle traditions, which hold until today. The effect was
not visible in the old TTY times, because that adds a prefix of "*** "
by default. Note that there are other situations where ML failure
might lead to no error output, notably involving Exn.Interrupt.Such non-printing exceptions should not show up under normal
circumstances -- they indicate a programming mistake somewhere.
The following is probably not relevant to the 2014 release anymore, but
for the sake of completeness:
I encountered such a case yesterday (with 2014-RC2) with a tactic with
resulted in a non-productive result sequence, i.e. the equivalent of
ML <
fun inf_seq () = Seq.cons 0 (inf_seq ())
val nonprod_seq = Seq.filter (K false) (inf_seq ())
>
After some looking around, I found that I get a little hint in the Raw
Output panel -- if the panel is open while the failing code is executed.
I wonder whether the raw output panel could accumulate, say, the last 8k
worth of messages even if it is closed? Also, a "clear" button would be
nice (although closing/reopening works).
Interestingly, asking for an exception trace (via
[[ML_exception_trace]]) for this code sends polyml into a another
desperate quest for memory: It has been running on my machine a few
minutes with 4086M VIRT and 3956M RES -- so basically exhausting its
full address space -- before giving up:
Welcome to Isabelle/HOL (Isabelle2014-RC2: August 2014)
Warning - Unable to increase stack - interrupting thread
Warning - Unable to increase stack - interrupting thread
Warning - Unable to increase stack - interrupting thread
Warning - Unable to increase stack - interrupting thread
Run out of store - interrupting threads
Run out of store - interrupting threads
Failed to recover - exiting
message_output terminated
standard_output terminated
standard_error terminated
process terminated
command_input terminated
process_manager terminated
Return code: 1
In these cases I could be useful to get at least at a partial trace
(which would probably already indicate which functions
went into a loop).
Email Gateway (Aug 19 2022 at 15:47):From: Makarius <makarius@sketis.net>
On Thu, 7 Aug 2014, Lars Noschinski wrote:
I encountered such a case yesterday (with 2014-RC2) with a tactic with
resulted in a non-productive result sequence, i.e. the equivalent ofML <
fun inf_seq () = Seq.cons 0 (inf_seq ())
val nonprod_seq = Seq.filter (K false) (inf_seq ())
>After some looking around, I found that I get a little hint in the Raw
Output panel -- if the panel is open while the failing code is executed.
The above example provokes a soft breakdown of ML user code. The
Poly/ML run-time systems maps that to an interrupt, which is not printed
in PIDE. There are other visual clues that something is wrong with the
command transaction. It is then left as an exercise to find section "4.2
Low-level output" in the Isabelle/jEdit manual, and connect it
semantically to such sitations.
I wonder whether the raw output panel could accumulate, say, the last 8k
worth of messages even if it is closed?
There is always the question how much technology is built around low-level
errors. They occurr so rarely that an incident can become a big desaster
if the error handling infrastructure itself gets overloaded. This could
lead to spectacular events of "total failure of existence", which we've
had occasionally had in the past. (That phrase is from Starship Titanic
due to Douglas Adams and Terry Jones, where it is called S.M.E.F.
"Spontaneous Massive Existence Failure".)
Nonetheless, I have made some changes for the Isabelle2014 code base some
months ago concerning Syslog output -- to have a buffer and a limit on it,
with some hope that bombing the front-end is avoided. So there might be a
chance to print certain low-level messages on Syslog, instead of raw
output, but such experiments are not for this release.
Also, a "clear" button would be nice (although closing/reopening works).
The panel is a plain Swing text area, so you can just select all text and
deleted it.
Interestingly, asking for an exception trace (via
[[ML_exception_trace]]) for this code sends polyml into a another
desperate quest for memory: It has been running on my machine a few
minutes with 4086M VIRT and 3956M RES -- so basically exhausting its
full address space -- before giving up:In these cases I could be useful to get at least at a partial trace
(which would probably already indicate which functions went into a
loop).
This looks like a hard breakdown of the ML runtime system. David
Matthews is the only one who can say more about it.
Note that driving the system against a concrete wall routinely causes big
damage. In the past couple of years, David Matthews has managed to move
concrete walls many times, but it is a never ending process. (The JVM is
even more fragile under low-memory situations.)
After 32bit address space is left behind -- presumably soon -- such VM
problems will go away, and the good old disk-thrashing on swap space will
come back.
Makarius
Email Gateway (Aug 19 2022 at 15:47):From: David Matthews <dm@prolingua.co.uk>
I would guess, and it is only a guess since I haven't actually tested
this, is that there is an infinite or at least very deep recursion
there. The thread stacks are expanded until the process runs out of
space. The way exception-trace was done changed in Poly/ML 5.5.1.
Exception_trace now builds a list of the functions rather than directly
printing them to standard output as it used to. There is a problem,
though, if there is no space to build the list. I don't think there is
a way to limit the size of the stacks (these are the stacks of ML data
managed by the Poly/ML run-time not the C stacks allocated by the
system). Perhaps there should be.
David
Email Gateway (Aug 19 2022 at 15:47):From: Lars Noschinski <noschinl@in.tum.de>
This is indeed the case, so the the "soft breakdown", as Makarius put
it, is absolutely not surprising. I was mildly surprised when this
prevented the system from giving my some kind of trace.
Last updated: Apr 25 2024 at 12:23 UTC