[isabelle] A few questions about Isabelle2013



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













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