Re: [isabelle-dev] code abbreviation for mapping over a fixed range

2015-11-07 Thread Bertram Felgenhauer
Hi Florian,
> > This email refers to the following commit:
> > 
> >   http://isabelle.in.tum.de/repos/isabelle/rev/7d1127ac2251
> > 
> >   code abbreviation for mapping over a fixed range
> > 
> > Is there a specific reason for this code equation:
> > 
> >   "map_range f (Suc n) = map_range f n @ [f n]"
> > 
> > It seems rather inefficient. Anyway, what's the purpose of "map_range".
> 
> the idea of map_range is to avoid building a list first and then mapping it.

Please don't forget about this.

The new definition actually causes *more* allocation than the original
one, except for very short lists, because every call of @ copies its
first argument. Note that the code equation for [_..<_] is

  lemma upt_rec[code]: "[i..

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

2015-11-07 Thread Makarius

On Fri, 6 Nov 2015, Makarius wrote:


On Wed, 4 Nov 2015, Clemens Ballarin wrote:


 On 30 October, 2015 20:02 CET, Makarius  wrote:

>  Standard batch build prints relatively few terms, so this is not yet
>  significant as a test.
> 
>  The following change prints every intermediate Isar toplevel state. 
>  With

>  that I get timeouts or interrupts due to out-of-memory situation in
>  various sessions, e.g. HOL-Nominal-Examples or Jinja.

 Unfortunately this already fails without my patch, so it cannot be used as
 a test.


Odd. I am in the process of looking more closely what really happens here, 
both with and without your change.


These tests always take very long, but there is probably not much behind 
it.  Printing requires a lot of resources (space and time) and the 
timeouts are just that: the session takes very long and is interrupted.  I 
have increased some timeouts manually to get more sessions through.


Included is a slightly refined change for testing: it avoids producing a 
lot of big strings.



Since the actual change to src/Pure/Isar/generic_target.ML is so small, we 
should just go ahead with it -- after a full test with AFP.



Makarius# HG changeset patch
# User wenzelm
# Date 1446936258 -3600
#  Sat Nov 07 23:44:18 2015 +0100
# Node ID 8fab417a5955afbe2d211cb45d6138dd2fb880f5
# Parent  15952a05133c8b05eeadd7697333a6e70f58aeeb
test

diff -r 15952a05133c -r 8fab417a5955 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML Sat Nov 07 20:04:09 2015 +0100
+++ b/src/Pure/Isar/toplevel.ML Sat Nov 07 23:44:18 2015 +0100
@@ -588,6 +588,8 @@
 val opt_err' = opt_err |> Option.map
   (fn Runtime.EXCURSION_FAIL exn_info => exn_info
 | exn => (Runtime.exn_context (try context_of st) exn, at_command tr));
+val _ = writeln (command_msg "" tr);
+val _ = writeln (string_of_int (length (pretty_state st')));
 val _ = get_hooks () |> List.app (fn f => (try (fn () => f tr st st') (); 
()));
   in (st', opt_err') end;
 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev