[isabelle-dev] Advice for replacing @{simpset} with @{context}.
Hi all, I am in the process of updating some of our local tools to the repository version of Isabelle, in preparation for the next Isabelle release (possibly named Isabelle 2013-1?) One of the changes that has occurred since Isabelle 2013 is that simpsets have been deprecated in favour of storing simplifier rules directly in the context. In this new world order, what is the best way to manage long-term simpsets when they are not in active use? For example, imagine that I have a theorem attribute foo, which adds a rule to a set of theorems: lemma a [foo]: ... lemma b [foo]: ... lemma c [foo]: ... I also have a tactic bar which internally passes this set of theorems to the simplifier. The implementation in Isabelle 2013 is simple: have a simpset floating around in your theory data, add new theorems to it on demand, and finally use it when needed. I am not sure what the best way to port this forward is. I could store the theorems as a list in my theory data, but that would mean it would need to be converted into a discrimination net each time the tactic bar was used, which could have performance implications when the number of theorems is large. I could convert back and forth from a context each time a new rule is added as such: val new_ss = simpset_of ((put_simpset convenient ctxt old_ss) addsimps [new_thm]) but I suspect that this was not the intended solution. Any suggestions as to the best way to manage sets of rules that will eventually be fed into the simplifier? Thanks so much, David The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Advice for replacing @{simpset} with @{context}.
On 13/09/13 04:17, Makarius wrote: The NEWS file explains what will happen in the coming release with simpset vs. Proof.context -- the Simplifier was one of the last hold-outs of non-localized tools, so after long delays we are mostly through with it. Sorry, I should have mentioned that I read the NEWS file; I understood that the simplifier now accepted a context instead of a simpset, and that addsimps operated on contexts instead of simpsets. My question was instead related to the best way to perform operations on long-lived simpsets which need to be mutated over time, now that there are no exposed APIs for manipulating them. Florian's reply was helpful in pointing out some code (the code generator) which also had this problem, and its solution to this which amounts to: (i) taking your old simpset; (ii) putting it into a dummy context; (iii) performing your addsimp/addcong/etc operation; (iv) extract the simpset out again. Cheers, David The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle_12-Sep-2013
Hi Makarius,
Thanks for your hard work for putting this together.
Most things I tried seemed to work out of the box on my 64-bit Linux
system, including sledgehammer, nitpick, etc.
I understand this is an integration test, and not a general release
candidate, but nevertheless I will write about a few small issues
I hit while playing with it:
* While auto try, auto quickcheck and auto nitpick seemed
to work, I couldn't get auto sledgehammer to give me a response.
The lemma I tried was:
lemma length xs 0 ⟹ hd (rev xs) = last xs
which sledgehammer is easily able to solve in less than two seconds
on my machine.
* It would be nice if symbol completion worked in the new find
panel. Similarly, using the standard Isabelle font in the search box
probably makes sense.
* The new find panel doesn't report the number of matches; only
the number displayed. For example, searching True displays:
displaying 40 theorem(s)
in the panel, while find_theorems reports:
found 222 theorem(s) (40 displayed):
which is perhaps more informative.
* Key-bindings (or at least hooks for keybindings) would be helpful
for the new find panel and sledgehammer panels. isabelle-find and
isabelle-sledgehammer hooks exist, but don't place focus on the
search box nor start a sledgehammer run.
* The abbreviations described in the README panel for sub, sup
and bold do not appear to work.
* The new superscripts are confusing me. term T\^suba parses,
but T\^supa does not. I must confess I don't understand the top
NEWS entry describing what has changed.
Also, using a clean Isabelle install without local patches applied
reminded me of a number of longer standing issues:
* The default Error color and Running color colours are very
similar, making them hard to distinguish in the theories panel
(Is there an error in that theory, or is it just taking a long time
to process?). I personally modify my Running color to be
a pleasant blue.
* When opening a theory from the command line, it would be nice to
have an option to automatically open dependent theory files without
prompting. It is nice to type:
isabelle jedit -l SomeLongRunningHeap FileWithManyDeps.thy
go away for a coffee, and come back with everything ready to go.
Currently, you have to click yes after the heap has built before
Isabelle will start processing FileWithManyDeps.thy.
* The output panel has a habit of scrolling to the top each time
the current output is appended to. It would be nice to preserve the
user's position.
For example, trying to view the current progress of the command:
ML {*
map (fn x = (tracing (PolyML.makestring x);
OS.Process.sleep (seconds 0.1))) (1 upto 100)
*}
is difficult.
I am, of course, happy to submit patches for review for any (or all) of
these problems if there is any indication that such patches would be
appreciated.
Thanks again for all your hard work, and my apologies in advance if
I am raising issues that you are already aware of.
Cheers,
David
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spec_Check
On 24/06/13 21:20, Makarius wrote: Last week, I actually intended to make a proper exposition about Isabelle/ML futures in the implementation manual, but for now it just points to ~~/src/Pure/Concurrent/future.ML with its slightly odd Notes at the beginning. That needs to be turned into proper text outside the sources, as part of the manual. As a single data-point: I personally find the Notes at the top of the file far more useful than out-of-line documentation. In particular, I never think to look in the implementation manual because only a very small percentage of the Isabelle sources are documented there. (There is a conceptual problem with putting such explanations into the sources, since they are built in bottom-up manner, but explanations should be more top-down; this is also relevant for worked examples that are actually run.) Again, users don't need a function-by-function running commentary of the sources, but just need to get a high-level idea of what is going on: I would claim that a description at the top of the file---and perhaps a few sentences on top of important functions---helps just as much as pages of carefully typeset prose. Further, the latter tends to require much more effort, meaning that often the choice boils down to either having quick-and-dirty notes in the source that exist, versus polished documentation outside the sources that doesn't. On this note, if you would like someone to go through and add documentation inline to the Isabelle sources, I would be willing to put my hand up to help out. (Assuming, of course, there was an interest in committing the patches, and a willing expert to review them.) Cheers, David The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [PATCH 1 of 1] Fix top-level printing of exception messages containing forced-line breaks
Hi Makarius, On 09/04/13 02:06, Makarius wrote: Sorry, I did not mean to re-open this messy thread anytime soon, but David Matthews had offered his help with forced breaks in Poly/ML in privite mail. Since I did not want to waste his time as well, I've looked through the situation in Isabelle/ML once more, eventually resulting in http://isabelle.in.tum.de/repos/isabelle/rev/b7f908c99546 Thank you for these changes. I just wanted to confirm that in this revision the forced-break-in-an-exception printing problem that I was experiencing appears to fixed, as is the forced-break-in-a-PolyML.makestring problem. Cheers, David The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [PATCH 0 of 1] Fix top-level printing of exception messages containing forced-line breaks
On 05/04/13 09:32, Makarius wrote: On Fri, 5 Apr 2013, David Greenaway wrote: What practical things could such volunteers do that you would find helpful? So how about maintaining Proof General, seriously, no-nonse? As somebody who isn't a Proof General user, nor an Emacs user, nor has ever worked with elisp, this doesn't fall particularly well within my skill-set, unfortunately. And there are other unmaintained parts, such as WWW_Find. (Note that several other people have worked there in the meantime, and they should be included in the discussion, to benefit from the experience gained from certain find_theorems experiements that never hit the repository so far.) WWW_Find is perhaps closer to my skill set, but still not a tool I use. Volunteers, counter-intuitively, require payment. Sometimes such payment is a simple thanks on a public mailing list or a changeset being accepted into the official repository. Other times it requires seeing an itch that they have been facing being scratched. If we wanted to start a discussion about replacing WWW_Find with a custom server that the inbuilt find_theorems command could be set up to automatically probe...: find_theorems (_ :: word32) + _ 2 ^ 32 searched for: _ + _ 2 ^ 32 0 theorem(s) found in current session. 2 theorem(s) found from theorem server example.com: WordLemmaBucket.word_add_power_off: [...] (requires import of WordLemmaBucket) LemmaBucket.word_add_bits: [...] (requires import of LemmaBucket) ...then we would be talking about an itch that I would be willing to volunteer some time to scratch. Cheers, David The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [PATCH 0 of 1] Fix top-level printing of exception messages containing forced-line breaks
Hi Makarius, On 02/04/13 21:17, Makarius wrote: On Tue, 2 Apr 2013, David Greenaway wrote: I would appreciate it if an Isabelle expert could review that patch and, if acceptable, apply it to mainline. (This can be easily done with hg import patch-file). before you send more patches, can you please go back to the very start of the mail thread from last time, which contains a lot of hints how things are done, including pointers to the documentation. I am not going to spend such an amount of time again, especially when it looks like it is being wasted. My apologies if your time has been wasted. It was my hope that sending a bug report, along with an analysis of its cause and a suggested fix would waste far less of your time than simply sending through just the bug report with nothing more. I also fear that your hints have been too subtle for me. I have re-read README_REPOSITORY (which appears to be mostly a HG tutorial, which a short paragraph describing the desired commit message content) and chapter 0 of the implementation manual (which, amongst other things, includes a longer discussion of the desired ML style, variables names, etc). Despite this, I must confess that I am still not sure what I am doing wrong. Does my 4 line patch violate the Isabelle style guidelines, or have I missed something about the correct etiquette for submitting patches? I would greatly appreciate if someone could let me know what I am doing wrong, so I can avoid wasting both your time and my time in the future. A single sentence such as: You should be sending Mercurial bundles instead of patches to the list; or Your name 'str_of_exn' should use the whole word 'string'; or Your line 'a | b | c' should be split into three; existing usages where they are on the same line are wrong; or You are dereferencing 'Pretty.margin_default' unsafely; the existing code that does this is wrong; or Your commit message is far too verbose, etc. would be immensely useful. Indeed, such a critique need not come from you Makarius, but from anyone on the list involved with Isabelle development who knows better than me. Cheers, David The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [PATCH 0 of 1] Fix top-level printing of exception messages containing forced-line breaks
Hi Alexander,
Thanks for your helpful reply.
On 04/04/13 08:58, Alexander Krauss wrote:
Hi David,
On 04/03/2013 09:18 AM, David Greenaway wrote:
[...]
Does my 4 line patch violate the Isabelle style guidelines, or have
I missed something about the correct etiquette for submitting patches?
I would greatly appreciate if someone could let me know what I am doing
wrong, so I can avoid wasting both your time and my time in the future.
Some points that I noticed (but this is neither exhaustive nor
authoritative):
- Architecture violation: Isabelle/ML code may not refer to the PolyML
structure directly, since it must use the compatibility layer. Your code
does not compile with SML/NJ which is still formally supported.
Possibly, something similar could be done in the compatibility layer,
but one has to consider the consequences very carefully.
Ah, this indeed is a serious problem that I should have considered more
carefully. Thank you for pointing it out.
- Process: You are assuming/proposing a fix, but there has been no
discussion whether the behavior you are seeing is actually something
that should be fixed. In particular, you seem to be expecting the
display of low-level exceptions to be as convenient as user-level pretty
printing. AFAIK, this is not the case in general. Due to the complexity
of the system, there are many grey areas that are neither right nor
wrong. I would say that pretty printing of low-level exceptions is such
a case.
So you should describe your actual real-life problem, and we can then
also look for other solutions.
The problem is that Isabelle will sometimes render thm's and cterm's
with a large number of spaces.
For example, in the testcase posted earlier:
definition test a b ≡ undefined
notation (output) test (test // (_) // (_))
ML {* raise (CTERM (test, [@{cterm test x y }])) *}
jEdit will render to the output:
test 9 spaces x 9 spaces y,
making the x and y hard to see. For users of ProofGeneral, this will
also tend to lock up emacs for long periods of time (as it attempts to
process the large amount of data). The sheer amount of data will even
give jEdit pause, especially when the number of forced line breaks in
a term starts to increase.
The cause of the problem, as far as I can see, is that when Isabelle is
converting its own pretty-print format into PolyML's pretty-print format
it translates forced line breaks into a directive to print 9
spaces. Presumably the assumption is that PolyML will decide that it
can't possibly fit 9 spaces on the current line, and convert the
spaces into a newline.
This works most of the time, except in two scenarios:
PolyML.makestring assumes that the line width is infinite, so will
simply render the spaces. General.exnMessage (which converts
ML exceptions into strings) internally calls PolyML.makestring, so
suffers the same fate.
The problem arises in practice when developing with Isabelle: unhandled
exceptions containing thm's or cterm's are mis-rendered, and
PolyML.makestring can't be used as a debugging aid when these
problematic terms are floating around.
It might also be interesting to know if the problem has always been
there or has been introduced by some change. I personally saw quite some
long CTERM exceptions and never noticed strange printing, so it might
also be a new issue (just speculating here).
The problem has been present for quite some time: I seem to recall
seeing it in Isabelle 2009 up to now. I only recently managed to take
track down the precise cause of the problem (i.e., the interaction
between forced line breaks and PolyML's pretty-printer) this past week.
- Style: Your commit message is indeed too verbose, according to the
usual standards, and it has the wrong format. The question whether
Isabelle's terse style is good or bad is a different issue, but the
conventions are like that, see README_REPOSITORY.
Thank you for the pointer. I misinterpreted the README_REPOSITORY as
being permissive of short messages (as opposed to prescriptive), but
will ensure future commit messages are more concise.
Hope this helps a bit...
Very much so, thank you.
Cheers,
David
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] [PATCH 1 of 1] Fix top-level printing of exception messages containing forced-line breaks
# HG changeset patch
# User David Greenaway david.greena...@nicta.com.au
# Date 1364864695 -39600
# Node ID 27bd348e777a3ffa4a4bf5bb18faa0a8428e468f
# Parent d40aec502416a0eaa094e5aef1f317f7c4867852
Fix top-level printing of exception messages containing forced-line breaks.
Both Isabelle and PolyML have pretty printers. One problem arises when
converting from Isabelle's format to PolyML's format, in that the former
supports forced line breaks while the latter does not. The current solution
is to expand such line-breaks into a large number of spaces (9, to be
precise), preventing PolyML from fitting the spaces on a line, and hence
forcing it to produce a line-break.
This approach, unfortunately, falls down in two areas: PolyML.makestring
renders the large amount of spaces, producing undesirable results. Similarly,
General.exnMessage in PolyML simply calls PolyML.makestring, and hence has
the same problem.
The problem can be seen with the following testcase:
definition test a b ≡ undefined
notation (output) test (test // (_) // (_))
ML {* raise (CTERM (test, [@{cterm test x y }])) *}
This patch fixes one instance of this problem by using an alternative mechanism
to pretty-print unhanded exceptions which prevents the large number of spaces
being rendered.
diff --git a/src/Pure/Isar/runtime.ML b/src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML
+++ b/src/Pure/Isar/runtime.ML
@@ -65,6 +65,10 @@
SOME exns = maps (flatten context) exns
| NONE = [(context, identify exn)]);
+fun str_of_exn (exn : exn) =
+ PolyML.prettyRepresentation (exn, ! Pretty.margin_default)
+ | pretty_ml | Pretty.from_ML | Pretty.string_of
+
in
fun exn_messages_ids exn_position e =
@@ -104,7 +108,7 @@
| THM (msg, i, thms) =
raised exn (THM ^ string_of_int i)
(msg :: if_context context Display.string_of_thm thms)
-| _ = raised exn (General.exnMessage exn) []);
+| _ = raised exn (str_of_exn exn) []);
in [((i, msg), id)] end)
and sorted_msgs context exn =
sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn));
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] [PATCH 0 of 1] Fix top-level printing of exception messages containing forced-line breaks
Hi all,
I have noticed that in c ertain circumstances both Isabelle/jEdit and
Isabelle/ProofGeneral will render certain constructs with a large number
of spaces in them.
The problem can be seen with the following testcase:
definition test a b ≡ undefined
notation (output) test (test // (_) // (_))
ML {* raise (CTERM (test, [@{cterm test x y }])) *}
The root cause is related to the interaction between Isabelle and
PolyML's pretty-printers. A problem arises when converting from
Isabelle's format to PolyML's format, in that the former supports
forced line breaks while the latter does not. The current solution is
to expand such line-breaks into a directive to print a large number of
spaces (9, to be precise), preventing PolyML from fitting the spaces
on a line, and hence forcing it to produce a line-break.
This approach, unfortunately, falls down in two areas:
PolyML.makestring renders the large amount of spaces, producing
undesirable results. Similarly, General.exnMessage in PolyML simply
calls PolyML.makestring, and hence has the same problem.
This attached patch fixes one instance of this problem by using an
alternative mechanism to pretty-print unhanded exceptions which prevents
the large number of spaces being rendered, fixing the problem above.
I would appreciate it if an Isabelle expert could review that patch and,
if acceptable, apply it to mainline. (This can be easily done with hg
import patch-file).
The patch is based off the current Isabelle tip, which is d40aec502416
at time of writing.
Thanks so much,
David
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [PATCH 0 of 3] Reduce Isabelle/jEdit output window overflow.
On 26/03/13 00:40, Makarius wrote: On Mon, 25 Mar 2013, David Greenaway wrote: [...] The problem that this patch fixes is internal to the Isabelle sources, and not directly related to how jEdit measures strings. As mentioned above, Pretty uses FontMetrics.stringWidth to determine if text will overflow, while Rich_Text_Area actually uses Font.getStringBounds to layout text. Because the two values disagree for the same strings, we get inadvertant overflow to the right. I've come across that part of jEdit and Isabelle/Scala sources again (presenty at Isabelle/193ba70666bd). That seems to have improved the situation significantly, thank you. My impression is that FontMetrics.stringWidth and FontMetrics.getStringBounds merely differ in the result type: Int vs. Double. I also hope that FontMetrics.getStringBounds and Font.getStringBounds are the same, if provided by suitable parameters, but there is no problem to use the latter uniformly. It seems that Java 2D text is normally snapped on a pixel grid, unless you explicitly ask for fractional font metrics as rendering hint. This is off by default, and normally degrades rendering quality. (Did you have that enabled? Did it actually improve visual appearance? On which physical display?) Font hinting tends to be a matter of personal preference. Some people prefer that fonts are rendered snapped to the monitor's pixel grid so everything looks sharp, while others (such as myself) prefer accurate glyphs, even if it means fonts look a little blurry. (A nice overview of the different problems and possible solutions is at [1].) [1]: http://www.antigrain.com/research/font_rasterization/ What is also funny is that the idea of avarage char width that I've got wrong in the first attempt is also a bit confused in the jEdit sources (hidden behind misleading Javadocs and slightly outdated code), although jEdit gets its visual tab width and preferred window geometry right in the end, just due to the way how slightly confusing operations happen to be used. To improve general uniformity and potential of surprise, I've clarified the Pretty.Metric and JEdit_Lib.Pretty_Metric notions once again, to make more explicit what this is all about. It does not change the situation of occasionaly scrollbars and 0.3 of a character off the vieport, though. There must be other effects, about jEdit calculating scrollbar parameters. I'm still confused as to why everything needs to be normalised to the width of a space, but in general the code seems to make more sense now. Thanks for the changes. Generally note, that the font metric business can never be 100% right -- not just because of floating point arithmetic. When text is actually rendered, its font-style might change again in the tokenization. I don't think this tiny snag deserves more of this undue priority right now. (There are no bugs, no fixes, just continous improvements of approximations, until perfection is reached in the limit.) Yes, I did notice that and understand that fixing this would require deeper changes that not even I am motivated to investigate right now. Now that the font rendering code has settled down again, should I update and resubmit my documentation patches to pretty.scala? If so, would you prefer ScalaDoc or just plain Scala comments? Cheers, David The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] [PATCH 2 of 3] pretty: Ensure we are consistent in our use of space-widths versus character-widths
src/Pure/General/pretty.scala | 20 +---
src/Tools/jEdit/src/jedit_lib.scala| 6 +++---
src/Tools/jEdit/src/pretty_text_area.scala | 2 +-
src/Tools/jEdit/src/pretty_tooltip.scala | 2 +-
src/Tools/jEdit/src/rich_text_area.scala | 2 +-
5 files changed, 15 insertions(+), 17 deletions(-)
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
# HG changeset patch
# User David Greenaway david.greena...@nicta.com.au
# Date 1363843205 -39600
# Node ID b1420574b7273225672a9f7e6a5b3e9c6c84b75d
# Parent e0c74b23d0a87547465aced2020de1998175662a
pretty: Ensure we are consistent in our use of space-widths versus character-widths.
The current version of pretty.scala internally uses spaces to pad out
indented lines. Unfortunately, it internally measures the width of these
strings of spaces using char_width, which is an approximation of the average
width of characters in the current font. This is particularly noticeable in
jEdit when using a font where the width of a space character is a significantly
different width from other characters.
We replace char_width and char_width_int with a new method space_width,
and adjust callers to use these new methods instead.
diff --git a/src/Pure/General/pretty.scala b/src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala
+++ b/src/Pure/General/pretty.scala
@@ -163,14 +163,13 @@
/** Default implementation for measuring a string. */
private def metric_default(s: String) = s.length.toDouble
- /** Returns an approximation of the width of an average character in the
-* given [[FontMetrics]], measured in pixels. */
- def char_width(metrics: FontMetrics): Double = metrics.stringWidth(mix).toDouble / 3
- def char_width_int(metrics: FontMetrics): Int = char_width(metrics).round.toInt
+ /** Returns the width of a single space character in the given [[FontMetrics]],
+* measured in pixels. */
+ def space_width(metrics: FontMetrics): Int = metrics.stringWidth( ) max 1
- /** Returns the width of the given string.
+ /** Returns the width of the given string, in spaces.
*
-* The unit returned is average character widths. For example:
+* For example:
*
*{{{
*font_metic(font, isabelle)
@@ -180,11 +179,10 @@
* in.
*/
def font_metric(metrics: FontMetrics): String = Double =
-if (metrics == null) ((s: String) = s.length.toDouble)
-else {
- val unit = char_width(metrics)
- ((s: String) = if (s == \n) 1.0 else metrics.stringWidth(s) / unit)
-}
+ {
+val unit = space_width(metrics)
+((s: String) = metrics.stringWidth(s) / unit)
+ }
/** Annotates the given [[XML.Body]] containing indentation and line breaking
* information with concrete formatting directives so that it can be printed
diff --git a/src/Tools/jEdit/src/jedit_lib.scala b/src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala
+++ b/src/Tools/jEdit/src/jedit_lib.scala
@@ -168,7 +168,7 @@
// NB: last line lacks \n
def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
{
-val char_width = Pretty.char_width_int(text_area.getPainter.getFontMetrics)
+val space_width = Pretty.space_width(text_area.getPainter.getFontMetrics)
val buffer = text_area.getBuffer
@@ -179,9 +179,9 @@
try {
val p = text_area.offsetToXY(range.start)
val (q, r) =
- if (stop = end) (text_area.offsetToXY(end), char_width * (stop - end))
+ if (stop = end) (text_area.offsetToXY(end), space_width * (stop - end))
else if (stop 0 buffer.getText(stop - 1, 1) == \n)
-(text_area.offsetToXY(stop - 1), char_width)
+(text_area.offsetToXY(stop - 1), space_width)
else (text_area.offsetToXY(stop), 0)
(p, q, r)
}
diff --git a/src/Tools/jEdit/src/pretty_text_area.scala b/src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala
+++ b/src/Tools/jEdit/src/pretty_text_area.scala
@@ -109,7 +109,7 @@
if (getWidth 0) {
val fm = getPainter.getFontMetrics
- val margin = (getPainter.getWidth / (Pretty.char_width_int(fm) max 1)) max 20
+ val margin = (getPainter.getWidth / Pretty.space_width(fm)) max 20
val base_snapshot = current_base_snapshot
val base_results = current_base_results
diff --git a/src/Tools/jEdit/src/pretty_tooltip.scala b/src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala
@@ -208,7 +208,7 @@
val bounds = rendering.tooltip_bounds
val w =
-((Pretty.char_width(fm) * (margin + 1)).round.toInt + deco_width) min
+((Pretty.space_width(fm) * (margin + 1
[isabelle-dev] [PATCH 0 of 3] Reduce Isabelle/jEdit output window overflow.
Hi all, Attached is a patch series which attempts to improve the font rendering in the Isabelle/jEdit output window. In particular, it attempts to reduce the number of cases where text is inadvertently rendered off the right-hand-side of the output window, requiring the user to scroll across to see the last few characters. A summary of the patches is as follows: [PATCH 1 of 3] pretty: Add ScalaDoc comments to Pure/General/pretty.scala Adds ScalaDoc comments to the pretty.scala file. I found that I had a hard time understanding what was going on. Hopefully these comments will assist future users and developers get up to speed a little faster. [PATCH 2 of 3] pretty: Ensure we are consistent in our use of space-widths versus character-widths Modifies pretty.scala to use the width of a space character (instead of an approximation of the width of an average character) when calculating how wide a string of spaces is. More details are in the patch comment. [PATCH 3 of 3] pretty: Use a more accurate method of measuring string lengths Use Font.getStringBounds instead of FontMetrics.stringWidth to measure string widths. The two calls give different values, and the former is the one actually used when performing rendering, and hence should be more accurate. Again, more details are in the patch comment. I would appreciate it if Isabelle experts could review these patches and, if acceptable, apply to mainline. The patches are based off revision 60472a1b4536, the tip of the Isabelle repo at time of writing. If these patches are acceptable, I would also propose a few more changes which I would be willing to draft: * pretty.scala currently uses space-widths as its internal unit. It may be beneficial to refactor this to use an arbitrary unit internally (chosen by the caller) and measure the space strings it generates (also updating pretty.ML to match). This would prevent the current dance of needing to divide out the width of a space everywhere. * Rich_Text_Area.print_valid_line and TextAreaPainter.PaintText.paintValidLine use two different text rendering techniques. The current implementation of Rich_Text_Area uses the former to paint text, while the latter to calculate the width of the painted text. This means that a horizontal scrollbar may be enabled when no actual text overflows the right hand side of the screen. We should probably do our own width calculations instead of calling jEdit to paint the text a second time. (It is probably also worth inspecting the implementation of PaintText.paintValidLine to determine if their font-rendering method choices are preferable). * Markup.SEPARATOR, as far as I can tell, is currently ignored when rendering text. It would be nice to have some sort of visual indicator between different blocks of text. For example, in the output of find_theorems, it is hard to determine when one theorem ends and another starts. Ideally, a small vertical gap could be rendered between different blocks. This may be hard in jEdit, which might assume that all lines are of the same height. An alternative would be to have a subtle visual marker, such as a faint line between different blocks. * The jEdit subpixel text rendering option is currently ignored by Rich_Text_Area. It would be nice to add support for this, which may require some rethinking of how the cursor rendering code works. Thoughts about these proposed patches would also be appreciated. The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] [PATCH 3 of 3] pretty: Use a more accurate method of measuring string lengths
src/Pure/General/pretty.scala | 16
src/Tools/jEdit/src/jedit_lib.scala| 13 -
src/Tools/jEdit/src/pretty_text_area.scala | 12 +---
src/Tools/jEdit/src/pretty_tooltip.scala | 20
src/Tools/jEdit/src/rich_text_area.scala | 6 +-
5 files changed, 46 insertions(+), 21 deletions(-)
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
# HG changeset patch
# User David Greenaway david.greena...@nicta.com.au
# Date 1363843205 -39600
# Node ID 10e9fed2f208cbaf93fd351d260c26c82cedb931
# Parent b1420574b7273225672a9f7e6a5b3e9c6c84b75d
pretty: Use a more accurate method of measuring string lengths.
pretty.scala currently uses FontMetrics.stringWidth to calculate the width
of a string, while the jEdit rendering engine uses Font.getStringBounds to
measure strings. These values do not always match, especially when using
anti-aliased fonts, non-hinted fonts, or subpixel text rendering.
We modify pretty.scala to use the more accurate Font.getStringBounds which
prevents text being inadvertanly rendered off the side of the screen.
diff --git a/src/Pure/General/pretty.scala b/src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala
+++ b/src/Pure/General/pretty.scala
@@ -8,6 +8,7 @@
import java.awt.FontMetrics
+import java.awt.font.FontRenderContext
/** Re-formats [[XML.Body]] instances so that long lines are wrapped
* onto multiple lines with human-readable indentation.
@@ -165,7 +166,8 @@
/** Returns the width of a single space character in the given [[FontMetrics]],
* measured in pixels. */
- def space_width(metrics: FontMetrics): Int = metrics.stringWidth( ) max 1
+ def space_width(metrics: FontMetrics, font_context: FontRenderContext): Double =
+metrics.getFont.getStringBounds( , font_context).getWidth
/** Returns the width of the given string, in spaces.
*
@@ -178,12 +180,18 @@
* will return approximately `8.0`, depending on the [[FontMetrics]] passed
* in.
*/
- def font_metric(metrics: FontMetrics): String = Double =
+ def font_metric(metrics: FontMetrics, font_context: FontRenderContext): String = Double =
{
-val unit = space_width(metrics)
-((s: String) = metrics.stringWidth(s) / unit)
+val unit = space_width(metrics, font_context)
+((s: String) = metrics.getFont.getStringBounds(s, font_context).getWidth / unit)
}
+ /** Returns the number of space characters that will fit into the given
+* number of pixels. */
+ def pixels_to_spaces(metrics: FontMetrics,
+ font_context: FontRenderContext, pixels: Int): Double =
+pixels / space_width(metrics, font_context)
+
/** Annotates the given [[XML.Body]] containing indentation and line breaking
* information with concrete formatting directives so that it can be printed
* within a canvas having width `margin` spaces.
diff --git a/src/Tools/jEdit/src/jedit_lib.scala b/src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala
+++ b/src/Tools/jEdit/src/jedit_lib.scala
@@ -9,13 +9,15 @@
import isabelle._
-import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle}
+import java.awt.{Component, Container, Window, GraphicsEnvironment,
+Point, Rectangle, FontMetrics, Graphics, Graphics2D}
+import java.awt.font.TextLayout
import scala.annotation.tailrec
import org.gjt.sp.jedit.{jEdit, Buffer, View}
import org.gjt.sp.jedit.buffer.JEditBuffer
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
object JEdit_Lib
@@ -168,7 +170,8 @@
// NB: last line lacks \n
def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
{
-val space_width = Pretty.space_width(text_area.getPainter.getFontMetrics)
+val painter = text_area.getPainter
+val space_width = Pretty.space_width(painter.getFontMetrics, painter.getFontRenderContext)
val buffer = text_area.getBuffer
@@ -179,9 +182,9 @@
try {
val p = text_area.offsetToXY(range.start)
val (q, r) =
- if (stop = end) (text_area.offsetToXY(end), space_width * (stop - end))
+ if (stop = end) (text_area.offsetToXY(end), (space_width * (stop - end)).ceil.toInt)
else if (stop 0 buffer.getText(stop - 1, 1) == \n)
-(text_area.offsetToXY(stop - 1), space_width)
+(text_area.offsetToXY(stop - 1), space_width.ceil.toInt)
else (text_area.offsetToXY(stop), 0)
(p, q, r)
}
diff --git a/src/Tools/jEdit/src/pretty_text_area.scala b/src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala
+++ b/src/Tools/jEdit/src
[isabelle-dev] [PATCH 1 of 3] pretty: Add ScalaDoc comments to Pure/General/pretty.scala
src/Pure/General/pretty.ML|4 +
src/Pure/General/pretty.scala | 140 -
2 files changed, 139 insertions(+), 5 deletions(-)
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
# HG changeset patch
# User David Greenaway david.greena...@nicta.com.au
# Date 1363843205 -39600
# Node ID e0c74b23d0a87547465aced2020de1998175662a
# Parent 60472a1b4536ce2b1fd27fdb8f00d3036bd0457c
pretty: Add ScalaDoc comments to Pure/General/pretty.scala.
Additionally, add a small note to pretty.ML indicating that pretty.scala
mirrors it.
diff --git a/src/Pure/General/pretty.ML b/src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML
+++ b/src/Pure/General/pretty.ML
@@ -17,6 +17,10 @@
The stored length of a block is used in breakdist (to treat each inner block as
a unit for breaking).
+
+pretty.scala attempts to mirror this file. Algorithmic changes here should
+also be made there.
+
*)
signature PRETTY =
diff --git a/src/Pure/General/pretty.scala b/src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala
+++ b/src/Pure/General/pretty.scala
@@ -9,15 +9,48 @@
import java.awt.FontMetrics
-
+/** Re-formats [[XML.Body]] instances so that long lines are wrapped
+ * onto multiple lines with human-readable indentation.
+ *
+ * == Overview ==
+ *
+ * The object to be printed is given as a [[XML.Body]] with
+ * indentation and line breaking information. A [[Pretty.Break]]
+ * inserts a newline if the text until the next break is too long to fit on
+ * the current line. After the newline, text is indented to the level of the
+ * enclosing block. Normally, if a block is broken then all enclosing blocks
+ * will also be broken.
+ *
+ * The algortihm used is loosely based on D. C. Oppen, Pretty Printing,
+ * ''ACM Transactions on Programming Languages and Systems'' (1980), 465-483.
+ *
+ * == Implementation ==
+ *
+ * All units, unless other specificed, are measured in space-widths (or
+ * simply, spaces), where one space-width is defined to be the width of
+ * a single space character. For example, in some fonts a wide character such
+ * as `w` would have width of `1.2`, while a narrow character such as `i`
+ * would have a width of `0.8`. In a fixed-width font, most characters will
+ * have a width of precisely `1.0` or `2.0`.
+ *
+ * This file is attempts to closely mirror `pretty.ML`; algorithmic changes here
+ * should be reflected in the other.
+ */
object Pretty
{
- /* spaces */
+ /*
+ * Spaces
+ */
val space =
private val static_spaces = space * 4000
+ /** Creates a string consiting of `k` space characters.
+*
+* If possible, we create a substring out of our existing static_spaces
+* string to avoid allocating large amounts of memory.
+*/
def spaces(k: Int): String =
{
require(k = 0)
@@ -26,10 +59,20 @@
}
- /* markup trees with physical blocks and breaks */
+ /*
+ * Markup trees with physical blocks and breaks.
+ */
+ /** Annotates the input `body` as a simple block with 2 spaces of
+* indentation.
+*/
def block(body: XML.Body): XML.Tree = Block(2, body)
+ /** Annotation indicating that `body` should be indented as a unit.
+*
+* In particular, if a newline is required when printing `body`, all
+* subsequent lines in the block will be indented by `i` spaces.
+*/
object Block
{
def apply(i: Int, body: XML.Body): XML.Tree =
@@ -43,6 +86,10 @@
}
}
+ /** Annotation indicating that either `w` spaces should be printed if
+* possible, or a newline should be printed if there is insufficient space
+* available on the line.
+*/
object Break
{
def apply(w: Int): XML.Tree =
@@ -56,14 +103,29 @@
}
}
+ /** Annotation indicating that a newline should be unconditionally printed. */
val FBreak = XML.Text(\n)
+ /** Annotation indicating a conceptual break between the previous element and
+* the next.
+*
+* Such a Separator could, for instance, be rendered with a vertical gap or
+* line between each of the items to help the user distinguish the
+* individual items.
+*/
val Separator = List(XML.elem(Markup.SEPARATOR, List(XML.Text(space))), FBreak)
+
+ /** Add [[Separator]] annotations between each of the given list of
+* [[XML.Tree]] objects. */
def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
- /* formatted output */
+ /*
+ * Formatted output.
+ */
+ /** Converts multiline text blocks in `body` in multiple single line text
+* blocks. */
def standard_format(body: XML.Body): XML.Body =
body flatMap {
case XML.Wrapped_Elem(markup, body1, body2) =
@@ -72,20 +134,51
Re: [isabelle-dev] [PATCH 0 of 3] Reduce Isabelle/jEdit output window overflow.
On 22/03/13 02:13, Makarius wrote: On Thu, 21 Mar 2013, David Greenaway wrote: Attached is a patch series which attempts to improve the font rendering in the Isabelle/jEdit output window. In particular, it attempts to reduce the number of cases where text is inadvertently rendered off the right-hand-side of the output window, requiring the user to scroll across to see the last few characters. There seem to be one or two important details that you have found out about Java text measuring and rendering, but they are difficult to spot in the mass of changes. I tried my best to ensure that each patch made only a single change, and each such change was well documented in the patch header. Let me try being more succinct: PATCH 1: Document pretty.scala, so future developers require less time to understand what is going on. PATCH 2: When determining how long a string of spaces is, use 'width( ) * n' instead of 'width(mix) * n / 3'. PATCH 3: When measuring strings, use Font.getStringBounds instead of FontMetrics.stringWidth. The latter doesn't take into account anti-aliasing or kerning, while the former is what is actually used when rendering the strings to the screen. Also note that chapter 0 of the implementation manual and README_REPOSITORY give some general explanations how Isabelle sources and changes over sources usually look like. You cannot just define your personal preferred style how things should be done and expect that it is accepted. (If it would, the Isabelle sources would be a huge chaos.) Again, I tried my best to conform to Chapter 0, README_REPOSITORY, the existing Scala code style and the ScalaDoc style guides [1]. If you could be a little more concrete on where I went wrong, I would be happy to reformat the patches. [1]: http://docs.scala-lang.org/style/scaladoc.html * pretty.scala currently uses space-widths as its internal unit. It may be beneficial to refactor this to use an arbitrary unit internally (chosen by the caller) and measure the space strings it generates (also updating pretty.ML to match). This would prevent the current dance of needing to divide out the width of a space everywhere. Can you say more directly what you think that is actually wrong? As long as rounding is done properly (which is not necessarily the case) any unit should work. Java also uses floating point in some interfaces, while integer pixels in other spots. Both can lead to problems, but I prefer to delegate calculations to floating point arithmetic if possible. pretty.scala has no need to know what units it is working in. It should just use the provided measure function to calculate string widths. This would mean the callers can use the most convenient representation for them; presumably pixels for callers who will be rendering to the screen, and number of characters for those working in ASCII. Also I am not suggesting moving away from floating point. In particular, the brave new world of sub-pixel font rendering would still require this. * Rich_Text_Area.print_valid_line and TextAreaPainter.PaintText.paintValidLine use two different text rendering techniques. The current implementation of Rich_Text_Area uses the former to paint text, while the latter to calculate the width of the painted text. This means that a horizontal scrollbar may be enabled when no actual text overflows the right hand side of the screen. We should probably do our own width calculations instead of calling jEdit to paint the text a second time. (It is probably also worth inspecting the implementation of PaintText.paintValidLine to determine if their font-rendering method choices are preferable). * Markup.SEPARATOR, as far as I can tell, is currently ignored when rendering text. It would be nice to have some sort of visual indicator between different blocks of text. For example, in the output of find_theorems, it is hard to determine when one theorem ends and another starts. Ideally, a small vertical gap could be rendered between different blocks. This may be hard in jEdit, which might assume that all lines are of the same height. An alternative would be to have a subtle visual marker, such as a faint line between different blocks. * The jEdit subpixel text rendering option is currently ignored by Rich_Text_Area. It would be nice to add support for this, which may require some rethinking of how the cursor rendering code works. All of that refers to particulars of the jEdit text rendering model. I am struggling with that for several years already, and the quality is already much better than anything I've seen before or elsewhere. Before doing greater changes in any of these respects, one needs to revisit carefully what I've done already (including study of the relevant changesets, which usually document that), and also get
Re: [isabelle-dev] Feature suggestion: apply (meth[1!])
On 08/03/13 23:46, Joachim Breitner wrote: Sometimes, when I’m writing apply-script style proofs, I have wanted a way to modify a proof method foo to “Try foo on the first goal. If it solves the goal, good, if it does not solve it, fail”. [...] I wanted to see if I could implement such a feature myself and came up with the attached patch – maybe it is already sufficient? Sorry to raise this thread again, but what was the outcome of this patch? Was the general concept of a solve tactical rejected, or just the particular choice of syntax / implementation? (If so, how could it be improved?) Or have the core developers just been busy? (I apologise if so!) I know that the conversion moved on how jEdit might additionally assist users in determining where a proof script became broken, but I didn't come to understand why this simple patch would be mutually exclusive to other more elaborate options. Cheers, David The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Community Involvement in Isabelle Development
On 14/03/13 22:37, Makarius wrote: Before we run again into a noisy thread that leads nowhere: the system development process is run by the people doing the actual work. This sounds like a trivial tautology, but is often forgotten. What level of community involvement (i.e., external contributions) in the Isabelle development process, if any, does the core development team desire? I believe there are many people in the Isabelle community willing to do actual work, given the opportunity. Such community members, however, are unlikely to make significant contributions without first being allowed to make smaller contributions. Joachim, for instance, was willing to create a patch and write documentation to solve a particular itch he had. The feature appeared to have some level of community support, and I suspect he would have been more than willing to adjust any implementation concerns, such as his choice of syntax or the ML implementation. When such patches fall on their face, however, it sends a message to the community that there is little point in doing actual work, as the chances of the work being accepted are slim. I must confess that yesterday I knowingly sent a half-baked patch solving the jEdit proof-output wrapping problem to the Isabelle users mailing list. I am more than willing to do the actual work of finishing and polishing the patch---implementing the fix for tooltips and SideKick, refactoring the Pretty class to internally use units of something other than fractions of the width of a space, writing in-code documentation describing what is going on, ensuring my style matches the guide-lines, etc. What stops me is that I am not convinced that my time will be well-spent. If changes will not be accepted into mainline, then it is not worth me doing the actual work of converting my half-baked patch into a proper fix. If, however, there becomes more of a culture of community involvement in the Isabelle development process, then I would be willing to help out. I will submit that patch which refactors build.scala to pull out the ROOT parser so other tools can also use it. I will submit that patch which adds additional in-code documentation to proof_context.ML to help out users trying to learn the internals of the system. I will submit that patch to include helper functions to assist users trying to interface with Isabelle at the ML level. The patches that I initially submit will no doubt be simple, and merely scratching my own itches. But as I submit patches and receive feedback, hopefully I will learn. Perhaps I will start being capable of making more significant changes. And, as time goes on, one day you might even wake up to find a patch in your inbox that scratches one of your itches. For such a community to form, however, it must first be fostered. It must be allowed to focus on the problems that it is facing. Occasionally, it must be humoured. At this point, however, it is not clear to me if external contributions are actively welcomed, merely tolerated, or mostly discouraged. Cheers, David The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature suggestion: apply (meth[1!])
On 10/03/13 07:03, Makarius wrote: On Fri, 8 Mar 2013, Joachim Breitner wrote: Sometimes, when I’m writing apply-script style proofs, I have wanted a way to modify a proof method foo to “Try foo on the first goal. If it solves the goal, good, if it does not solve it, fail”. The Isar proof method language was designed a certain way, to arrive at stilized specifications of some operational aspects in the proof text. It has excluded any kind of programming or sophisticated control structures on purpose. In 1998 it was not clear yet if that would work out, since the big applications of that time (e.g. HOL-Bali) were done differently. In retrospect the Isar method language was more succesful in this respect than I had anticipated. We see big applications today without lots of specialized goal-state manipulation. As a data point, inside the seL4 proof, a largish application of Isabelle, such a solve-or-fail mechanism would have been very helpful. First of all, we found that examples such as that given by Joachim come up quite frequently. Additionally, such syntax would be very helpful in proof maintenance, where you ideally want the proof script to break at the source of an error, instead of 12 lines further down. Liberal use of apply (foo)! in the more complex proof scripts would help maintainers find the source of an error more quickly. Cheers, David -- The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Tracing paused messages undesirably cause proofs running in background to stall
On 21/01/13 23:08, Makarius wrote: After inspecting the Isabelle source a little more, I have seen that there is a jEdit configuration variable: editor_tracing_messages that allows the pause threshold to be adjusted. Setting this value to a large number solves my first problem. The question might be as simple as providing a good default. In Isabelle2013-RC1 it is 100 messages, which is probably about low. How about 1000? Would that make your theories run through unhindered? The longest unification-related tracing messages I witnessed in our proofs were a little under 1500 lines (I saw three such cases). There were tens of proofs producing between 100 and 1000 lines. Testing on my own machine, viewing 10,000 lines of tracing output appears to work without any problems. When I hit a little above the 30,000 mark though, I start to see strange behaviour where the output buffer fails to display any output. I think a value of at least 1000 would be a sensible default; I am not sure what value between 1000 and 10,000 lines would be best, though. Thanks so much, David -- The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Tracing paused messages undesirably cause proofs running in background to stall
Hi all,
I have been locally testing out the current development snapshots of
Isabelle in anticipation of the Isabelle 2013 release. So far, most
things have been very smooth; thanks everyone for your hard work.
One minor problem I am hitting is the Tracing paused messages when
running proofs interactively. More precisely, when a tactic (or similar)
generates too much output using the tracing command, the following
message is displayed:
Tracing paused. Stop, or continue with next 10, 100, 1000 messages?
Clicking on one of the numbers listed in the message allows more tracing
messages to be displayed, and the tactic to continue.
While I can imagine this feature is useful when debugging unification or
simplification problems (to prevent jEdit from being flooded with
tracing messages), it is problematic when attempting to process large
proofs interactively.
In particular, each time a complex tactic attempts to trace too much,
the proof stalls until the user manually brings the file to the
foreground in jEdit, finds the culprit statement, and then clicks one of
the continue buttons. (This potentially must be repeated several times
for each culprit statement, if the tracing output is several thousand
lines long.)
For example, our proofs have quite a few commands which require complex
unifications, giving hundreds of messages from deep within Isabelle such
as:
Enter MATCH
λs x s a. x =?= λa x. ?P73 a x () ()
...
While the unification eventually succeeds, each such proof statement
requires human interaction in order to be processed.
A second related problem is when multi-threaded tactics use tracing,
such as the following:
ML {*
Par_List.map (fn x = (tracing (PolyML.makestring x)))
(1 upto 1000)
*}
In these cases, the user must click continue once for each thread in
the system. (In my case, it requires 16 clicks, despite only having
4 cores).
Is there any way to avoid these two problems?
(I am currently running Isabelle revision '23ed79fc2b4d',
Thu Jan 17 23:00:20 2013 +0100)
Thanks so much,
David
--
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
