Re: [isabelle] A few questions about Isabelle2013

On Tue, 15 Jan 2013, Alfio Martini wrote:

So far I am quite happy with this new version of Isabelle.

BTW, it is not a vew version of Isabelle yet, just a packaging test I made in preparation of the coming release. It was leaked from isabelle-dev to isabelle-users.

So it is pretty close to what should become Isabelle2013 during the next 4 weeks, or so. I hope to be able to start official Isabelle2013-RC1 testing at the end of this week. Right now we should count the above as totally unofficial RC0. As you continue testing any of these versions, it is important to update to consecutive release candidates whenever they appear, to avoid getting stuck with these not fully finished snapshots. Last time in the preparation of Isabelle2012, I introduced some small problems in later release candidates as reaction to observation to earlier ones. We need to avoided such accidents this time.

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

The parse vs. print phases of logical terms are not fully symmetric. It is just an accident that parse manages to report on result types produced by type-inference, but print omits that information.

So it is just one of these things that still don't work for the coming release.


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