Re: [isabelle] Isabelle2014-RC2 available for testing



Hi there,

some observation I made when moving my development to 2014-RC2:

When opening my Development in Isabelle/jEdit 2014-RC2 I got some (3-4) error markers that the theorem nat_add_commute was not found in some metis commands. I cleared them manually until all error markers were gone. Then when I restarted Isabelle/jEdit I got more error markers of the same kind, cleared them again manually until all were gone. But I still found 2 places were nat_add_commute was used using search afterwards which were not marked as errors.

Environment:
Macbook Pro, 2.4GHz Core i5 (2 Cores with 4 Threads), 8GB RAM, OS X 10.9.4, threads = 2, ML_OPTIONS="-H 500 --gcthreads 2"

Suggestion: Some "Report bug" or at least "Generate system report" support would be nice so you get the system information you need.

Side note: I used indentation folding in 2013 to get some basic folding support. I could enable it by moving my settings manually but the GUI support to changing this setting seems to be gone, at least I couldn't find it any more.

Best
    Benedikt

Am 04.08.14 17:52, schrieb Makarius:
Dear Isabelle users,

after 8 days of testing Isabelle2014-RC1, the second official
release candidate Isabelle2014-RC2 is now available:

  http://isabelle.in.tum.de/website-Isabelle2014-RC2


The following fine points that have been addressed:

  * tuning of documentation

  * update of Haskabelle to work with recent versions of ghc

  * minor changes to SMT2, sledgehammer, datatype_new tools

  * misc tuning and clarification of PIDE interaction


Observations and problems of release candidates may be discussed here on isabelle-users, or via private mail with the person who is responsible (when that is obvious).

In the next round it will become more difficult to find the remaining problems. People who have reported anything for previous release candiates should check again if the situation has indeed improved.

Ambitious users may already start updating their existing applications to work with Isabelle2014-RC2 -- it should be hardly distinguishable from final Isabelle2014.


    Makarius






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