Email Gateway (Aug 19 2022 at 15:43): Email Gateway (Aug 19 2022 at 15:43):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 15:45):From: bnord <bnord01@gmail.com>
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
Email Gateway (Aug 19 2022 at 15:45):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 15:45):From: bnord <bnord01@gmail.com>
Am 06.08.14 13:11, schrieb Makarius:
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).
Yes I figured that out, but my first go was just sledgehammer again
which worked fine. Later I did a find/replace which edited two more
occurrences.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.
No I wasn't sure just made the above observations. But I figured this
one out now, just noticed that for long documents the bar on the right
(whatever you call it) doesn't display markers for the whole document
but only for some part. You have to scroll through the whole document
after processing it to see whether there are any markers. This isn't
what one is used to from other editors with such a feature.
Best
Benedikt
Email Gateway (Aug 19 2022 at 15:45):From: Makarius <makarius@sketis.net>
That is called "text overview". There is an Isabelle plugin option "Text
Overview Limit" with a default of 65536. You can probably use the double
of that on your machine, without significant slowdown of real-time update
and painting.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC