Re: [isabelle] Isabelle2014-RC2 available for testing



On Wed, 6 Aug 2014, bnord wrote:

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.

According to NEWS there was a renaming of nat_add_commute ~> add.commute (and more like that).

Are you sure that the proof commands that still referred to this non-existing fact were actually applied successfully? I changed the error recovery recently, actually going back to some suggestions of yourself, but this change may now lead to some confusion.


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.

The relevant information is also context dependent. At the moment I won't expect any HW/OS specific non-determinism. In more than 50% of the cases, a "bug" is just user confusion anyway.


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.

In 2013 there was more than one Isabelle release: Isabelle2013 uses jedit-5.0.0, but Isabelle2013-2 uses jedit-5.1.0 like current Isabelle2014 release candidates. That could also make a difference, but I don't think so.

$ISABELLE_HOME_USERS/jedit/properties is the most relevant place to look for persistent state. If you sort this line-wise, you can compare the content with what you've had before.


	Makarius




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