Email Gateway (Aug 19 2022 at 09:42): Email Gateway (Aug 19 2022 at 09:42):From: Makarius <makarius@sketis.net>
Dear all,
this is one more step towards the Isabelle2013 release in mid-February.
See https://bitbucket.org/isabelle_project/isabelle-release for the main
website where this is organized. There is also a link to an issue tracker
on the same Bitbucket site.
The main Isabelle2013-RC2 download page is
http://isabelle.in.tum.de/website-Isabelle2013-RC2
Observations from testing release candidates may be discussed here on
isabelle-users, on the bitbucket tracker, or via private mail.
Makarius
Email Gateway (Aug 19 2022 at 09:44):From: Alfio Martini <alfio.martini@acm.org>
Hi Makarius,
After experimenting with Isabelle2013-RC2 for Windows (in my W7 laptop), I
can give the following feedback:
1) Intialization of Cygwin this time was successfull. Avast did not find
any problem with the following
program:
C:\Isabelle2013-RC1\contrib\cygwin\bin\peflags.exe
2) Avast it is however still very suspicious (considering them of low
reputation) with these ones, allowing
them to execute in sandbox mode though (after scrutinizing each file for
about half a minute):
C:\Isabelle2013-RC1\Isabelle2013.exe
C:\Users\AlfioMartini\Isabelle2013-RC2\contrib\polyml-5.5.0-3\x86-cygwin\poly.exe
C:\Users\AlfioMartini\Isabelle2013-RC2\contrib\exec_process-1.0.3\x86-cygwin\exec_process.exe
3) Old style of processing documents (via IsaMakefiles) is now working
again in this version (see image
attached)
4) Executing
isabelle build -o document=pdf -g doc
still shows the error when compiling the "Programming and Proving"
tutorial. Maybe the LaTeX setup
should be updated to include the package "eulervm.sty" or, as you suggest
in a previous e-mail,
that this package should not be used (or something else be used in its
place). See image attached.
5) Most important, those ambiguous and strange error messages (as discussed
in another live
thread) in the output window are
still present. I include here a file "error_test.thy" so you can see
exacty, on the spot, what
it is going on.
Best!
RC2-docprep-old-way-sucess.PNG
prog-prove-error.PNG
error_test.thy
Email Gateway (Aug 19 2022 at 09:44):From: Gottfried Barrow <gottfried.barrow@gmx.com>
So Sledgehammer is back in the saddle again. I run 13 ATPs together, and
the ATPs that normally find proofs all return normally. If I run 24 ATPs
together, then it seems to cause some of the ATPs to time out or
terminate when they otherwise wouldn't, but they terminate in a normal
manner by returning an error message.
Getting analytical about the output panel, I'd say there are two types
of information, primary information and secondary information.
With Sledgehammer set for a 60 second timeout, the output is always
going to be primary information, meaning that I'm always going to want
to look at the output from the time I start the command until the
command finishes.
It turns out that I've switched today to using the tooltip window to
look at the Sledgehammer window, since it doesn't get overwritten with
new data while Sledgehammer is running.
The cycle is something like this:
1) Start Sledgehammer.
2) Hover over "sledgehammer".
3) When the tooltip window pops up, click on the "Detach tooltip window"
icon so that it's a normal window and doesn't disappear if I click
somewhere else.
4) Scroll to the bottom to see if there's any new output there to think
about, and maybe go ahead and click on a proof to insert it and
terminate Sledgehammer.
5) Close the window.
6) Loop through items 2 through 5 until sledgehammer finishes, and then
do it one last time.
So, I use whatever features are there to be used. If the output panel
went away, I obviously wouldn't use it.
But some information you want to look at a lot, and some information you
only want to look at on an as need basis. So if you have to do more work
than you used to to look at information that you look at a lot, then you
will long for yesterday.
Regards,
GB
Email Gateway (Aug 19 2022 at 09:45):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Makarius,
once more I want to bring up an older thread (back then on isabelle-dev)
about the Output Panel.
See
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg03072.html
[*]
If we open a new empty theory file and do not immediately insert the
"end" (or any other character, for that matter) that belongs at the end
of a theory file, we are always one-off with the caret, i.e., error
messages as well as normal output is only visible after moving the caret
to the left once. Examples (caret position indicated by [...]):
theory Test[]
I expect "Outer syntax error: keyword "begin" expected, but end-of-input
was found" in the Output Panel, but see nothing, if I go back to "theory
Tes[t]" the error message shows up.
theory Test imports Main begin
thm refl[]
I expect "?t = ?t", but get nothing (again it works after changing to
"thm ref[l]").
find_theorems "_ = _"[]
It seems that the search is run, but we don't get the output until we
have "find_theorems "_ = _["]". The same hold, e.g., for sledgehammer:
the command is run, but we do not see the output.
All of this examples work as expected, as soon as at least 1 additional
character is added after the current position.
I think especially for beginners, starting from a completely empty file
is a common use case. End the current behavior might be a bit unexpected.
IIRC, you said that this is a general jEdit problem?
For the current release: is there a workaround (e.g., always append a
newline at the end of a new file)? Or otherwise, I would mention at a
(very) prominent place that we should always start by inserting "end" at
the end of a file. Or, even better, jEdit could insert a temple
automatically for any new *.thy file, e.g.,
theory <Filename>
imports <Import>
begin
[]
end
where <Filename> is taken from the user (if available), <Import> might
default to "Main" and [] is the initial cursor position).
cheers
chris
[*] An aside: I would very much like to link to the "official"
isabelle-dev mail archive, but it is not searchable, and even if you
managed to find a certain message somehow, links between threads are
just cut at month borders, which makes it very hard to follow longer
threads.)
Email Gateway (Aug 19 2022 at 09:47):From: Makarius <makarius@sketis.net>
On Wed, 30 Jan 2013, Christian Sternagel wrote:
If we open a new empty theory file and do not immediately insert the "end"
So why do it without? You need the end eventually, so you can make it
part of the standard habit of starting a new theory.
Examples (caret position indicated by [...]):
theory Test[]
I expect "Outer syntax error: keyword "begin" expected, but end-of-input was
found" in the Output Panel, but see nothing, if I go back to "theory Tes[t]"
the error message shows up.
IIRC, you said that this is a general jEdit problem?
Yes, jEdit has a blind spot at the very end of the buffer, due to special
tricks it does for handling files with or without final line terminator.
Even worse, the numeric length of the buffer is one off, so plugins
unaware of that easily produce NPE particles. I have once tried to file a
tracker item at the jEdit project, but these guys are not as reactive as
we are here on the Isabelle mailing lists. One should try again, ideally
in a constructive version, i.e. a patch proposal for jEdit.
I think especially for beginners, starting from a completely empty file
is a common use case. End the current behavior might be a bit
unexpected.
I think genuine beginners don't even get that far. They need to be told
to open some .thy file and put a certain template there. Some people do
not even manage to get Isabelle/jEdit start up -- in the last two releases
I tried to improve the success rate at that spot primarily.
For the current release: is there a workaround (e.g., always append a
newline at the end of a new file)?
The Isabelle2013 codebase already has various internal workarounds, and it
is close to a local optimum that is hard to change without breaking things
again. There used to be funny effects when moving the caret, like showing
old versions of output, instead of showing nothing, as it should be now.
Or otherwise, I would mention at a (very) prominent place that we should
always start by inserting "end" at the end of a file. Or, even better,
jEdit could insert a temple automatically for any new *.thy file, e.g.,
Most people don't even read the most prominent bits of information, like
ANNOUNCE or NEWS. It is better to make jEdit put a template there without
too much hassle, but that old idea did not make it in the Isabelle2013
release.
What could be done right now is to make a nice video for the first
encounter with Isabelle/jEdit, and put this somewhere on youtube.
An aside: I would very much like to link to the "official" isabelle-dev
mail archive, but it is not searchable, and even if you managed to find
a certain message somehow, links between threads are just cut at month
borders, which makes it very hard to follow longer threads.)
I never know myself how to quote our mailing lists and just use an
arbitrary archive from the main Isabelle website.
Makarius
Email Gateway (Aug 19 2022 at 09:48):From: Makarius <makarius@sketis.net>
It should actually work better than in Isabelle2012 now. It was just an
accident that the Cygwin version from that time was handling the
inherently fragile spawing of external processes most of the time. The
Cygwin in Isabelle2013-RC1 was less benign, and this old problem was
harder to ignore.
For Isabelle2013-RC2, David Matthews changed Poly/ML to work with parallel
Cygwin processes in a robust manner. I managed to run tests like
HOL-Nitpick_Example with all its Java processes for Kodkod without
problems.
If anybody still sees external Cygwin processes that crash in strange ways
(with stack dump), or left-over processes that are not cancelled properly,
please report this. (You can use the Windows task manager or "ps" on the
Cygwin Terminal to check this.)
Makarius
Email Gateway (Aug 19 2022 at 09:48):From: Makarius <makarius@sketis.net>
Yes, this is approaching a good way to do it. A minor technical snag
remains: the tooltip is not updated dynamically, and this won't happen for
Isabelle2013.
Makarius
Email Gateway (Aug 19 2022 at 10:01):From: Gottfried Barrow <gottfried.barrow@gmx.com>
It wasn't predictable, and it didn't happen but maybe once every 30
minutes, at the most, and when I was doing a lot of typing.
I did a little typing with the default jEdit install folder for
Isabelle2103-RC3, and it works, but I won't immediately find out if it's
a problem.
It could be related to the fact that I use two views to edit the same
file. The cursor of one view might be at the very bottom of the file,
and so every keystroke in the 2nd view causes the 1st view to have to do
its continuous proving thing. The typing gets sluggish, but I use it
like that quite a lot anyway.
Another mystery was that the side panel would close occasionally, as if
I had clicked on the side panel tab of the plugin.
Things have primarily been uneventful, especially with the
multi-threading fix for Cygwin.
Regards,
GB
Email Gateway (Aug 19 2022 at 10:24):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
I don't know if it's RC related or not, but the output format of the
“print_locales” command, could be improved, displaying one element at a
line instead of all elements in a flow. The actual output looks bulky in
the output pan.
Email Gateway (Aug 19 2022 at 10:24):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Another one (I installed RC2 when coming back to Isabelle, and don't
remember if it was the same before), also about what's displayed in the
output pan, now by the “display_rules” command.
Quick case: “thm conjI” displays “?P ⟹ ?Q ⟹ ?P ∧ ?Q” in the output pan.
OK, but “display_rules” displays “?P ⟹ ?Q ⟹ ?P ∧ ?Q” without its name,
which is “conjI”. Don't know if it's on purpose or a bug.
Email Gateway (Aug 19 2022 at 10:24):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Tiny mistake in “logics-HOL.pdf”. On page 8, it says “someI” is part of
HOL. It's not, it's in Main.
Email Gateway (Aug 19 2022 at 10:24):From: Christian Sternagel <c.sternagel@gmail.com>
To answer in a confusing way: Main is HOL ;)
But seriously. In the PDF, "HOL" refers to the logic HOL (not to the
theory file HOL.thy). And everything that is loaded by Main.thy
(including the theory Hilbert_Choice.thy, which adds "someI") is part of
the logic image HOL, and thus of the logic HOL as used in Isabelle/HOL.
(Additionally there are of course extensions like theories from
~~/src/HOL/Library or the AFP, but what Main.thy represents is kind of
the minimal version that a user should see.)
hope this helps,
chris
Email Gateway (Aug 19 2022 at 10:24):From: Christian Sternagel <c.sternagel@gmail.com>
Concerning documentation, there is a confusing paragraph in isabelle
doc locales page 2, starting with "The keyword notes denotes ...". (The
sentence starting with "Instead" does not seem to fit here.)
cheers
chris
Email Gateway (Aug 19 2022 at 10:25):From: Lawrence Paulson <lp15@cam.ac.uk>
You are absolutely right. This section describes the primitive HOL theory (HOL.thy). When it was written, Isabelle/HOL followed the traditional formalisation in which the existential quantifier was defined with reference to Hilbert's epsilon operator. Later, the formalisation was changed to eliminate this entirely unnecessary dependence on the axiom of choice, with Hilbert's epsilon being introduced much later in the development. It is now possible to formalise mathematics without use of the axiom of choice in Isabelle/HOL, but you would have to do without a great many things, including Sledgehammer.
Larry Paulson
Email Gateway (Aug 19 2022 at 10:25):From: Makarius <makarius@sketis.net>
It is always good to have people looking closely, but here it is a lost
cause.
The logics-HOL manual has been categorized as "old / outdated" for several
years. Material from it is (slowly) moving into more current manuals, and
one day it shall disappear altogether.
Makarius
Email Gateway (Aug 19 2022 at 10:26):From: Makarius <makarius@sketis.net>
I have never heard about "display_rules". Do you mean "print_statement"?
Trying this in Isabelle2013-RC2:
thm conjI
print_statement conjI
it looks fine to me. The first case just the proposition of the theorem,
and the second with the name of it (guessed according to certain internal
"name hints" that happen to work here).
Makarius
Email Gateway (Aug 19 2022 at 10:27):From: Yannick <yannick_duchene@yahoo.fr>
I use it to know what's the available rules for the “rule” proof method.
This help to to guess what “rule” alone used as much as to give “rule” an
explicit argument.
Email Gateway (Aug 19 2022 at 10:27):From: Makarius <makarius@sketis.net>
OK. In the meantime I have also added its documentation in isar-ref, so
it will be in Isabelle2013-RC3 soon.
Note that method "rule" is dynamically rebound in HOL to include rules
stemming from the classical reasoner, too. Cf. print_claset.
At some point I would like to see proper feedback by the Prover IDE about
these implicit single-step rules applied here. Next release ...
Makarius
Email Gateway (Aug 19 2022 at 10:27):From: Yannick <yannick_duchene@yahoo.fr>
On Wed, 06 Feb 2013 21:40:33 +0100, Makarius <makarius@sketis.net> wrote:
I use it to know what's the available rules for the “rule” proof method.
This help to to guess what “rule” alone used as much as to give “rule”
an explicit argument.OK. In the meantime I have also added its documentation in isar-ref, so
it will be in Isabelle2013-RC3 soon.
I will wait for RC3 and re‑read the isar-ref.pdf file so. Do you know if
RC3 “print_rules” will always displays the rules without names? Actually,
it helps for the first use case (guess what “rule” use), but not the
second (giving “rule” explicit arguments).
Note that method "rule" is dynamically rebound in HOL to include rules
stemming from the classical reasoner, too. Cf. print_claset.
I'm not sure to understand what it implies, but will learn “print_claset”,
as you mention it.
At some point I would like to see proper feedback by the Prover IDE about
these implicit single-step rules applied here. Next release ...
Wow, great! :) I was wishing this. Before I came to Isabelle, at the time
I didn't knew any prover system, I tried to imagine such things, and in my
mind, this was always coming with this: “if it automate some proof or
proof step, the user should be able to learn what the steps was, it should
be visible in some way”. That's important, as the matter, I feel, is not
only about the prover understanding a proof, but also about the human
author and human reader, understanding it too.
Many thanks for the great point!
Email Gateway (Aug 19 2022 at 10:27):From: Makarius <makarius@sketis.net>
On Wed, 6 Feb 2013, Yannick wrote:
Note that method "rule" is dynamically rebound in HOL to include rules
stemming from the classical reasoner, too. Cf. print_claset.I'm not sure to understand what it implies, but will learn
“print_claset”, as you mention it.
It means that the "rule" method in HOL has additional rules available: the
ones of Pure (print_rules) and the ones of the classical reasoner context
(print_claset). It is wired up in a way that you normally get what you
expect in the first place.
Before I came to Isabelle, at the time I didn't knew any prover system,
I tried to imagine such things, and in my mind, this was always coming
with this: “if it automate some proof or proof step, the user should be
able to learn what the steps was, it should be visible in some way”.
That's important, as the matter, I feel, is not only about the prover
understanding a proof, but also about the human author and human reader,
understanding it too.
Yes, this implicit use of single-step rules from the context according to
the structure of your problem, is an important aspect of Isar -- the
"Intellegible semi-automated reasoning" so to say. Fully automated
reasoning is used in different spots.
Until proper IDE feedback for "rule" steps arrives you can use rule_trace
as crude approximation:
notepad
begin
note [[rule_trace]]
have "A ∧ B"
proof -- trace
show A sorry
show B sorry
qed
from A ∧ B obtain A and B ..-- trace
end
This gives you the unfiltered uninstantiated candiates that the method
guesses from the situation.
(In Isabelle2012 the trace output needs to be enabled by the check-box in
the output panel; in Isabelle2013 it is always there.)
Makarius
Email Gateway (Aug 19 2022 at 10:27):From: Makarius <makarius@sketis.net>
I is still without names, the way it has been before.
It is not impossible to improve that eventually, but not trivial either.
For Isabelle2013 some print commands were improved --- e.g. find_theorems
and find_consts to markup their name references --- but not print_rules,
print_simpset, print_claset.
Makarius
Email Gateway (Aug 19 2022 at 10:28):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Maybe this solved a mysterious problem.
After reading the above, I looked at the options in the output panel to
see what check boxes are there. Until now, I've never done anything but
look at the output of the output panel.
A few minutes ago, I clicked on the "Detach" button, and an empty "Info"
window popped up, and that's what's been happening to me, an "Info"
window has been mysteriously opening up.
I'll be typing, and then an empty "Info" window will open up, and my
fingers haven't been near the CNTL or ALT keys. I've been looking high
and low for any shortcut that will do that, and I haven't found any.
I'll use this email as a means to mention the plugin that has become my
main plugin to get a global view of what's in my file.
Attached are two screenshots for a total of 150 Kbytes.
I create my search strings in the highlighter for individual words or
strings, as shown in the first image. I then group the keywords, one way
being to edit this plugin file:
\jedit\plugins\gatchan.highlight.HighlightPlugin\highlights.ser
The highlighter plugin not only highlights for me, but it becomes my
main way to get a sidebar list of the different groups of keywords, as
shown in the second image, where what is shown is the "everything group".
Sidekick doesn't work for me. I can't control the nesting very well;
it's either too expanded, or I have to click through too many nodes.
One flat list with highlighter is better than sidekick's tree.
Regards,
GB
highlighter 1 control.png
highlighter 2 tree.png
Email Gateway (Aug 19 2022 at 10:28):From: Yannick <yannick_duchene@yahoo.fr>
Typo on page 4 of Isar-ref.pdf says “There is notation to project
interval”: missing “a” (“There is a notation”).
Email Gateway (Aug 19 2022 at 10:29):From: Makarius <makarius@sketis.net>
Both sounds like an odd problem of window focus -- jEdit dockable windows
cannot be invoked with arguments, so I have to play tricks with focus
events to transfer content to the detached window.
Can you try this again with Isabelle2013-RC3 without any of your local
properties or plugins? A new release with a new name also gives you a
clean $ISABELLE_HOME_USER as you have probably noticed already.
Makarius
Last updated: Apr 19 2024 at 01:05 UTC