Re: [isabelle] A few questions about Isabelle2013



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:

* 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?

Best!


On Sat, Jan 12, 2013 at 5:28 AM, Gottfried Barrow
<gottfried.barrow at gmx.com>wrote:

> Hi,
>
> I got this link off of the developers list: http://www4.in.tum.de/~**
> wenzelm/test/Isabelle_11-Jan-**2013/<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
>
>
>
>
>
>
>
>
>
>


-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil

Attachment: hoover-const-edit.PNG
Description: PNG image

Attachment: hoover-const-output.PNG
Description: PNG image



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