Email Gateway (Aug 19 2022 at 09:53): Email Gateway (Aug 19 2022 at 09:53):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,
I got this link off of the developers list:
http://www4.in.tum.de/~wenzelm/test/Isabelle_11-Jan-2013/
I wasn't going to switch over, but Isabelle 2012 started freezing up
regularly several months ago, and it was freezing up very frequently
today, so I made the switch using the above link.
Now, I have a few questions and comments.
\<^SUB> IS STILL THERE. IS IT STAYING THERE?
In Isabelle 2013, nothing has changed in regards to \<^isub>, \<^isup>,
\<^sub>, and \<^sup>. Are \<^sub> and \<^sup> (or something equivalent)
going to stay in Isar forever, or are they going away? If they're not
going away, I'll use them exclusively for the markup I talked about
previously. If they're going away, I won't use them at all.
Comment: The symbols tab is a nice addition. I had a THY that listed all
the symbols, but the symbols tab is even better. Things are gettin' down
right graphical, which they already were.
HOW DO I GET MY SHORTCUTS IN THE NEW JEDIT?
I copied over my ".isabelle\Isabelle2012\jedit\properties" to the folder
".isabelle\Isabelle_11-Jan-2013\jedit", and it configured most
everything, but my shortcuts don't get activated. I look in the
"properties" file, and I see my shortcuts in there, but they aren't used
in "Global Options / Shortcuts".
If I manually add a shortcut for an entry that's in the "properties"
file, such as for
+jm..markup/mu__ncx__newthm_counter_example.shortcut=A+j m n c x
jEdit writes the same exact entry to the "properties" files.
Anyone know how to get jEdit to use all my shortcuts in the "properties"
file?
NORTON QUARANTINES POLY.EXE
Norton quarantines "contrib\polyml-5.5.0\x86-cygwin\poly.exe", but it
started doing that with Isabelle 2012. With Isabelle 2013, it gives me a
error message that it didn't give me before about not being able to find
the file. Users in the future should be aware of that. I just
unquarantine poly.exe, and know that it's going to happen when it gets
run for the first time on a computer on which I run Norton.
SMT PROOFS DON'T RUN THAT RAN BEFORE, AND SLEDGEHAMMER WAS FIRST HAVING
PROBLEMS
I saw on the developers list that SMT causes problems, so that answered
my question about whether I should use SMT proofs. The reason I had a
couple is because they were about 4 times faster than the metis proofs
that were found.
Sledgehammer wasn't working correctly at first. It wasn't updating the
output window. It was possibly related to me trying to run it on the
theorems that had the SMT proofs that didn't work anymore. At some
point, after trying different options on different theorems,
Sledgehammer started working.
COMMENTS CONTENT IS PICKIER
I got several errors I didn't get before for stuff that was in comments.
I found what it was that made the comments happy.
Thanks,
GB
Email Gateway (Aug 19 2022 at 09:53):From: Gottfried Barrow <gottfried.barrow@gmx.com>
There's a new file for jEdit 5, which is:
jedit\keymaps\jEdit_keys.props
I deleted all my previous shortcuts in the file
"Isabelle2012\jedit\properties", and I put them in the file
"Isabelle_11-Jan-2013\jedit\keymaps\jEdit_keys.props".
The shortcuts showed up alongside my macros in the Macros menu, and
jEdit didn't write them back into the "jEdit\properties" files. So I
guess the new file is where the shortcuts are stored. I looked just a
little on the web for information on how to import configuration from
one version of jEdit to another, but I didn't find any info.
Regards,
GB
Email Gateway (Aug 19 2022 at 09:54):From: Makarius <makarius@sketis.net>
Can you be more specific? Problems can be solved only when they are made
known, and described according to minimal standards of empirical science.
Otherwise it is just guesswork.
Guessing nonetheless, the ML system could crash in certain situations of
running out of resources. See e.g.
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-September/msg00152.html
how to use polyml-5.5.0 with Isabelle2012. It gives you much more
headroom in typical "low" memory situations of 1-2 GB. On Windows it is
always running in 32bit mode, so this is expecially relevant.
Makarius
Email Gateway (Aug 19 2022 at 09:54):From: Makarius <makarius@sketis.net>
The problem is not \<^sub> and \<^sup>, but the second copy \<^isub> and
\<^isup> for identifier syntax. This is an old issue stemming from 2003,
when that feature was introduced. Back then there were reasons to do it
like that, and after the coming release one might considere re-opening
the can to sort it out.
At the moment there are far more pressing things, notably getting
Isabelle2013 in a stable state, not putting more changes and features in
at this point.
Makarius
Email Gateway (Aug 19 2022 at 09:54):From: Makarius <makarius@sketis.net>
The jEdit guys have changed that slightly for jedit-5.0.0. There is now a
separate ISABELLE_HOME_USER/jedit/keymaps/ directory. So far I only made
sure that the standard Isabelle/jEdit keyboard shortcuts end up in the
generated imported_keys.props, without investigating what happens when
users start shuffling different keymaps.
You might have to look around at the jedit website and/or its mailing
lists.
Makarius
Email Gateway (Aug 19 2022 at 09:54):From: Makarius <makarius@sketis.net>
So is there some way to buy "protection" for poly.exe from the Norton
mafia?
Makarius
Email Gateway (Aug 19 2022 at 09:54):From: Makarius <makarius@sketis.net>
On Sat, 12 Jan 2013, Gottfried Barrow wrote:
SMT PROOFS DON'T RUN THAT RAN BEFORE, AND SLEDGEHAMMER WAS FIRST HAVING
PROBLEMSI saw on the developers list that SMT causes problems, so that answered my
question about whether I should use SMT proofs. The reason I had a couple is
because they were about 4 times faster than the metis proofs that were found.
You need to be more specific about the kind of problems you throw at
SMT/Z3.
Sledgehammer wasn't working correctly at first. It wasn't updating the
output window. It was possibly related to me trying to run it on the
theorems that had the SMT proofs that didn't work anymore. At some
point, after trying different options on different theorems,
Sledgehammer started working.
Can you explain this further, beyond the "works for me state"? Was it
just confusion about slightly changed options and editor reactivity, or a
genuine problem to be isolated?
Makarius
Email Gateway (Aug 19 2022 at 09:54):From: Makarius <makarius@sketis.net>
Guessing and speculating again, it might be just malformed Isabelle
symbols: anything starting with \< that is not properly terminated
according to the \<foobar> or \<^foobar> syntax.
Makarius
Email Gateway (Aug 19 2022 at 09:54):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Isabelle2013 seems to have fixed that problem. It hasn't froze up once
in 3 days. Guessing, I would say that Isabelle2012 was freezing up at
least once an hour on me, and frequently it would freeze up twice within
about 10 minutes or less.
The last day I used it, I was getting about 10 characters before it
would freeze up. But I was using a vertical split window, which I had
only started doing that day. I quit using a vertical split window, and
it quit freezing up so bad.
It wasn't a memory problem. I have an icon in my task bar that shows my
memory usage, and it rarely shows greater than 50% of the memory being used.
Thanks for the test release. It's working out good so far, other than
maybe Sledgehammer and jEdit not working together so well, but I have to
do some experimenting first before I comment again on that.
Regards,
GB
Email Gateway (Aug 19 2022 at 09:55):From: Gottfried Barrow <gottfried.barrow@gmx.com>
I sent an email to Norton telling them they're flagging a legitimate
product that's being produced by Cambridge and TUM. What you need is to
get in their database of legitimate programs. They use a huge database
of known good and bad programs to speed up their scans.
Norton has two types of scans, a scan to check for whether it's known to
be infected, and a scan to check for whether it looks suspicious, and if
it does look suspicious, they make decisions based on it's reputation
among the user community.
Poly.exe is getting flagged based on reputation. It has none, and it's
not a native Windows application, so it kind of makes sense.
If I didn't have lots of experience knowing the difference between
Norton's typical behavior with normal Windows installs that I download
from legitimate looking web sites, and programs that come from "other"
places, I might get rid of Norton, because I've used Avast and AVG and
know they're more lenient.
However, I keep Norton because no one has so far broken into my bank
account. The "reputation" scan is short term pain, but long term gain.
They're doing more than just looking at known virus signatures.
I think it's their attempt to deal with things like zero-day attacks:
https://en.wikipedia.org/wiki/Zero-day_attack
Here are the results of 3 sites that I had check poly.exe. (I don't know
if the results will show up for you using these links.)
http://virusscan.jotti.org/en/scanresult/96b63157b869b555c344913bbd059127d2f59b1d
http://r.virscan.org/report/288e325b3bac3aa4d09586b4d3bf37d9.html
The good news is that poly.exe is flagged only by Symantec out of about
47 anti-virus programs, and only based on their reputation scan. The
other good news is that I use Norton, so you at least know it could
happen to a user.
Regards,
GB
Email Gateway (Aug 19 2022 at 09:55):From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,
So far I am quite happy with this new version of Isabelle. For the moment,
I have a question concerning this feature listed in the News:
Email Gateway (Aug 19 2022 at 09:55):From: Makarius <makarius@sketis.net>
On Tue, 15 Jan 2013, Alfio Martini wrote:
So far I am quite happy with this new version of Isabelle.
BTW, it is not a vew version of Isabelle yet, just a packaging test I made
in preparation of the coming release. It was leaked from isabelle-dev to
isabelle-users.
So it is pretty close to what should become Isabelle2013 during the next 4
weeks, or so. I hope to be able to start official Isabelle2013-RC1
testing at the end of this week. Right now we should count the above as
totally unofficial RC0. As you continue testing any of these versions, it
is important to update to consecutive release candidates whenever they
appear, to avoid getting stuck with these not fully finished snapshots.
Last time in the preparation of Isabelle2012, I introduced some small
problems in later release candidates as reaction to observation to earlier
ones. We need to avoided such accidents this time.
- Configuration option show_markup controls direct inlining of markup
into the printed representation of formal entities --- notably type
and sort constraints. This enables Prover IDE users to retrieve that
information via tooltips in the output window, for example.It seems that, at least for constant functions, one is not able to see
the type of the constant in the tooltip window (only the theory where it
is defined) as opposed to the the corresponding one in the normal edit
window (after Ctrl+hover)..I attach two images, where the situation described above can be clearly
exemplified.Is this still a restriction or maybe a lack of proper configuration from
my part?
The parse vs. print phases of logical terms are not fully symmetric. It
is just an accident that parse manages to report on result types produced
by type-inference, but print omits that information.
So it is just one of these things that still don't work for the coming
release.
Makarius
Email Gateway (Aug 19 2022 at 09:55):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Here are simplified examples of what was in my comments.
These 5 examples give me an error that I don't get in Isabelle2012:
(* \<...> *)
Error: Malformed command syntax
--"\<rbrace>", --"\<lbrace>", --{* \<lbrace> }, and --{ \<rbrace> *}
Error: Unbalanced antiquotation block parentheses
The first example fits your description. I haven't used anitquotations,
so I don't know why the other four examples give errors. Using any of
the other left or right delimiters by themselves don't cause a problem,
like using --"\<langle>" doesn't give an error.
I had actually mismatched \<lbrace and "}" in a comment for something
like this:
--{* \<lbrace>an_equation} *}
The left brace is used by itself sometimes in math. I'm not using it
like that, so I don't care, at least not today.
Regards,
GB
Email Gateway (Aug 19 2022 at 09:55):From: Gottfried Barrow <gottfried.barrow@gmx.com>
I'm not really asking for any changes or new features, I'm asking, in a
roundabout way, that you leave those four commands the way they are,
forever.
I could be asking for even less, merely to know what the future holds.
If you said, "The four will eventually be reduced down to two commands",
I would say to myself, "Ah, it was a nice thought that things would stay
the same, but at least I know the future."
I can see the need to reduce those four, as they're named, down to only
two commands, but that the executive decision might need some more time
to be thought out or to implement.
But, commands like \<^isub>\<lfloor> and \<^isub>\<rfloor> would make
good markup commands. I can't use those particular two because I might
use the floor function in the index of a sigma sum, not that I've
completely thought that out.
There are plenty of other characters to choose from, but in these
formative stages, when things haven't been set in stone, it doesn't hurt
to ask.
Regards,
GB
Email Gateway (Aug 19 2022 at 09:55):From: Makarius <makarius@sketis.net>
On Tue, 15 Jan 2013, Gottfried Barrow wrote:
These 5 examples give me an error that I don't get in Isabelle2012:
(* \<...> *)
Error: Malformed command syntax
All Isabelle source text needs to conform to the official Isabelle symbol
syntax. Isabelle2013 is more thorough in checking that, even inside
comments.
--"\<rbrace>", --"\<lbrace>", --{* \<lbrace> }, and --{ \<rbrace> *}
Error: Unbalanced antiquotation block parentheses
There was an omission of not observing these formal-comments. This is
done in Isabelle2013, so for example
-- {* look here @{term "λx. x"} *}
will have the proper formal markup for the embedded term inside the
antiquotation. \<rbrace> and \<lbrace> are part of the official
antiquotation syntax, although they are rarely used. You can evade by
inventing referring to funny symbols that are not used elsewhere yet.
Makarius
Last updated: Apr 25 2024 at 12:23 UTC