Email Gateway (Aug 22 2022 at 10:22): Email Gateway (Aug 22 2022 at 10:22):From: Jason Dagit <dagitj@gmail.com>
I'm using Isabelle 2015 on OS X 10.10.3 and I'm having a few problems.
First, if I leave jEdit running then when I come back to my computer I will
often find jEdit has crashed:
Application Specific Information:
*** Terminating app due to uncaught exception 'JavaNativeException',
reason: 'java.lang.StackOverflowError'
terminating with uncaught exception of type JNFException
abort() called
I upgraded to the latest JRE (1.8), but I think jEdit is still using 1.7? I
don't know a good way to tell so I'm basing that on what it says in the
"About" screen in the jEdit menu. On the other hand, typing "java -version"
at the command line returns this:
java version "1.8.0"
Java(TM) SE Runtime Environment (build 1.8.0-b132)
Second, I use OS X to remap my keyboard to the dvorak layout, but when I
use a modifier key such as control jEdit interprets my keypress
incorrectly. I can even see this happening from the keyboard test utility
under the troubleshooting menu. This makes it impossible for me to use
certain shortcuts or to even use certain keys. This looks similar to my
problem:
https://bugs.openjdk.java.net/browse/JDK-8028617
Third, when I use sledgehammer remote_vampire always gives an error about
SystemOnTPTP, which makes me think remote_vampire is broken at the moment.
So instead of continuing to hammer their website, I wanted to remove
remote_vampire. So I removed remote_vampire in the jEdit options, but it
seemed to have no effect. I had to add a line like this to my
theory: sledgehammer_params[cvc4 z3 spass e]
Fourth, at this point I wanted to go back to using emacs so that at least
the first two issues would go away. The official tutorial, dated May of
this year, even has this to say:
"The recommended interface for Isabelle/Isar is the (X)Emacs-based Proof
General [1, 2]." But when I tried to connect Proof General to Isabelle, I
discovered that it never connects because tty support was removed! So is
Proof General still the recommended interface as the tutorial says?
Fifth, there have been several times when I thought Isabelle accepted my
proof, but actually there was an error and jEdit makes this difficult to
see. It's hard to explain this one without lots of screenshots. The problem
seems to be that jEdit tries to be clever and runs parts of the proof in
parallel or something. Is there a way to make it work like Proof General
where you can enter and retract the steps one at a time and explicitly?
I've tried toggling the "Auto Update" checkbox but then I can't tell what
part of the buffer has been accepted. Also, I don't see a way to make a
shortcut for requesting an update. Switching back to the mouse constantly
is annoying. So for now I use the "Auto Update" feature but I don't have a
good way to be sure Isabelle has completely accepted my input. It's also
easy to accidentally interrupt slow queries, such as sledgehammer which is
mildly annoying and a waste of time.
Sixth, I like to version control my configuration files and put them on
github so that I can easy restore my account or setup a new account on a
new computer. How do I export my jEdit settings?
Thanks,
Jason
Email Gateway (Aug 22 2022 at 10:22):From: Makarius <makarius@sketis.net>
On Fri, 26 Jun 2015, Jason Dagit wrote:
I'm using Isabelle 2015 on OS X 10.10.3 and I'm having a few problems.
I will pick some items off the list below, although I foresee a rather
entangled mailing list thread with so many different points under the same
Subject head line.
First, if I leave jEdit running then when I come back to my computer I will
often find jEdit has crashed:
Application Specific Information:
*** Terminating app due to uncaught exception 'JavaNativeException',
reason: 'java.lang.StackOverflowError'
terminating with uncaught exception of type JNFException
abort() called
That might be a generic JVM problem due to scarce resources. The defaults
are made to ensure that the system comes up in most hardware
configurations, but it is not so much for really big things. On Mac OS X,
the Isabelle2015.app has an Info.plist with JVMOptions; you can carefully
edit that to say something like:
-Xms1024m -Xmx4096m -Xss4m
These options correspond to the normal java command-line. See the
standard documentation by Oracle.
I upgraded to the latest JRE (1.8), but I think jEdit is still using 1.7?
We are talking about the Isabelle application here, which runs the jEdit
text editor as outer shell. Everything is bundled, even the JDK. You
should not need to change anything there. (It can be done in theory, but
requires manual tinkering.)
I don't know a good way to tell so I'm basing that on what it says in
the "About" screen in the jEdit menu. On the other hand, typing "java
-version" at the command line returns this: java version "1.8.0"
Java(TM) SE Runtime Environment (build 1.8.0-b132)
It just means the shell has a different idea about the default Java than
Isabelle. On the command-line, you would have to use "isabelle java
-version", where the "isabelle" executable is from the Isabelle
distribution inside the .app directory. It also has an "isabelle jedit"
command-line tool, but if you use that instead of the .app you need to
provide JEDIT_JAVA_OPTIONS via $ISABELLE_HOME_USER/etc/settings (which is
a bash script and absent by default).
Makarius
Email Gateway (Aug 22 2022 at 10:22):From: Makarius <makarius@sketis.net>
On Fri, 26 Jun 2015, Jason Dagit wrote:
Second, I use OS X to remap my keyboard to the dvorak layout, but when I
use a modifier key such as control jEdit interprets my keypress
incorrectly. I can even see this happening from the keyboard test
utility under the troubleshooting menu. This makes it impossible for me
to use certain shortcuts or to even use certain keys. This looks similar
to my problem: https://bugs.openjdk.java.net/browse/JDK-8028617
This sounds like a generic Java or jEdit problem. You can try plain jEdit
from http://www.jedit.org to see if it is the same. Depending on that, we
can continue the discussion here or on the jedit tracker
http://sourceforge.net/p/jedit/_list/tickets?source=navbar
Fourth, at this point I wanted to go back to using emacs so that at
least the first two issues would go away. The official tutorial, dated
May of this year, even has this to say: "The recommended interface for
Isabelle/Isar is the (X)Emacs-based Proof General [1, 2]."
That is probably the "tutorial" entry in the Documentation collection, but
that is fairly outdated. The "prog-prove" tutorial is more up-to-date,
although its Isabelle/jEdit screenshot is a bit old.
We have so many manuals from such a long time, that there are many layers
of historic sediments. After some time, you should develop a sense which
sources of information help in which situation. The "Reference Manuals"
section is updated more often, but that is not a tutorial.
But when I tried to connect Proof General to Isabelle, I discovered that
it never connects because tty support was removed! So is Proof General
still the recommended interface as the tutorial says?
The NEWS file for each Isabelle release is the most up-to-date piece of
information. For Isabelle2015 it says:
Makarius
Email Gateway (Aug 22 2022 at 10:22):From: Makarius <makarius@sketis.net>
On Fri, 26 Jun 2015, Jason Dagit wrote:
Fifth, there have been several times when I thought Isabelle accepted my
proof, but actually there was an error and jEdit makes this difficult to
see. It's hard to explain this one without lots of screenshots. The problem
seems to be that jEdit tries to be clever and runs parts of the proof in
parallel or something.
The way you use the name "jEdit" proves that you did not read the
Isabelle/jEdit manual, which has the label "jedit" in the Isabelle
Documentation panel.
Is there a way to make it work like Proof General where you can enter
and retract the steps one at a time and explicitly?
No.
Sixth, I like to version control my configuration files and put them on
github so that I can easy restore my account or setup a new account on a
new computer. How do I export my jEdit settings?
See also the Isabelle/jEdit manual.
Makarius
Email Gateway (Aug 22 2022 at 10:22):From: Quentin Hibon <quentin.hibon@polytechnique.edu>
Regarding the SystemOnTPTP messsage, Jasmin Blanchette gave the solution
to have remote_vampire working again, so I'll just reproduce his answer
below:
[quote]
It turns out SystemOnTPTP has moved to a new URL. If you want it to work
again, you will need to change the file
src/HOL/Tools/ATP/scripts/remote_atp
replacing
"http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply”;
with
"http://pages.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply”;
[/quote]
That does not tell you why your settings do not get applied, but at
least you'll get rid of the error message.
Email Gateway (Aug 22 2022 at 10:22):From: Jason Dagit <dagitj@gmail.com>
Thanks. That fixes it!
Email Gateway (Aug 22 2022 at 10:23):From: Jason Dagit <dagitj@gmail.com>
On Fri, Jun 26, 2015 at 11:13 AM, Makarius <makarius@sketis.net> wrote:
On Fri, 26 Jun 2015, Jason Dagit wrote:
I'm using Isabelle 2015 on OS X 10.10.3 and I'm having a few problems.
>I will pick some items off the list below, although I foresee a rather
entangled mailing list thread with so many different points under the same
Subject head line.First, if I leave jEdit running then when I come back to my computer I
will
often find jEdit has crashed:
Application Specific Information:
*** Terminating app due to uncaught exception 'JavaNativeException',
reason: 'java.lang.StackOverflowError'
terminating with uncaught exception of type JNFException
abort() called
That might be a generic JVM problem due to scarce resources. The defaults
are made to ensure that the system comes up in most hardware
configurations, but it is not so much for really big things. On Mac OS X,
the Isabelle2015.app has an Info.plist with JVMOptions; you can carefully
edit that to say something like:-Xms1024m -Xmx4096m -Xss4m
These options correspond to the normal java command-line. See the
standard documentation by Oracle.
Thanks. I've made this change, hopefully it will stop the crashes.
I upgraded to the latest JRE (1.8), but I think jEdit is still using 1.7?
>We are talking about the Isabelle application here, which runs the jEdit
text editor as outer shell. Everything is bundled, even the JDK. You
should not need to change anything there. (It can be done in theory, but
requires manual tinkering.)
I didn't realize Isabelle bundles the JDK.
Email Gateway (Aug 22 2022 at 10:23):From: Jason Dagit <dagitj@gmail.com>
It's a Java issue. I tried with the latest JRE and standalone jEdit and
it's still present. It's present in other Java programs as well. I doubt
there is much the jEdit developers can do about it.
By the way, while it doesn't appear to be a problem with this particular
download be careful about sourceforge installers. Some of the installers
bundle additional programs that are not good (they walk the line between
legitimate software and malware):
http://www.howtogeek.com/218764/warning-don%E2%80%99t-download-software-from-sourceforge-if-you-can-help-it/
Email Gateway (Aug 22 2022 at 10:25):From: Jason Dagit <dagitj@gmail.com>
This didn't help. It still crashes. Given this and the other problems I'm
seeing, I've moved back to Isabelle2013-2 so that I can use emacs and proof
general. I feel like I gave jEdit a try, but it's too frustrating to try
simultaneously adapting to an unfamiliar language, unfamiliar/quirky
editor, AND to deal with frequent crashes / keybinding issues.
Last updated: Apr 20 2024 at 01:05 UTC