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
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.

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:
> 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
> 




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