Re: [isabelle] Isabelle2014-RC0 available for testing



Hi,

thanks for the RC!

Am Samstag, den 05.07.2014, 20:04 +0200 schrieb Makarius:
> This is an opportunity to look how things will presumably be in the 
> release, and to report problems, either on the isabelle-users mailing list 
> or via private mail.

I tried to collect my minor observations, but it turns out that all of
them have been reported before. Anyways, here are those collected today:


 * I just observed an error message in the output window:
        Undefined constant: "list.size"⌂
  And I wonder what the ⌂ is about.


  * The spellchecker doesn’t know about a few probably Isabelle specific
    words such as “instantiation”. Maybe these should be added?


  * Messages like „Metis: Unused theorems:“ appear below the goal state
    in the output panel, which is less convenient than the previous
    order.

  * It is irritating that auto-completion does not work when there is a 
    letter following the cursor. But maybe I just need to get used to
    that.

  * No select-to-clipboard in the output window under Linux.

And another thing worth noting, although already present in the 2013
release: When jumping to a file that is loaded as part of the loaded
heap (e.g. Set), there is an error at the theory command: “Cannot update
finished theory "Set"”. That makes sense to me, but I don’t plan to
update the theory, I just want to navigate it. Currently, this prevents
me from using Ctrl-Click on definitions in that file to navigate
further.

Greetings and thanks,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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