Re: [isabelle] jEdit problems

Regarding the SystemOnTPTP messsage, Jasmin Blanchette gave the solution
to have remote_vampire working again, so I'll just reproduce his answer

It turns out SystemOnTPTP has moved to a new URL. If you want it to work
again, you will need to change the file






That does not tell you why your settings do not get applied, but at
least you'll get rid of the error message.

On 06/26/2015 06:47 PM, Jason Dagit wrote:
> 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:
> 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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.