Re: [isabelle-dev] Towards the release

2016-01-15 Thread Makarius 
Current Isabelle/9ca00b65d36c and AFP/2c322507b8a6 appears to be a fairly 
stable state, so I will take this as starting point for Isabelle2016-RC1 
later today.


The main isabelle-dev remains open a few more days for fine-tuning and 
consolidation.



Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Multicore timings

2016-01-15 Thread Makarius 
Just for the record here are some timings on dual Xeon E5-2620v3 2.40GHz 
with 12 threads:


Isabelle/9ca00b65d36c + AFP/2c322507b8a6

ML_OPTIONS="-H 2000 --gcthreads 12"
isabelle build -o threads=12

Finished HOL-Bali (0:00:57 elapsed time, 0:05:26 cpu time, factor 5.71)
Finished HOL-MicroJava (0:01:04 elapsed time, 0:06:32 cpu time, factor 6.12)
Finished Jinja (0:02:24 elapsed time, 0:16:13 cpu time, factor 6.75)
Finished JinjaThreads (0:37:50 elapsed time, 3:55:29 cpu time, factor 6.22)

Finished ConcurrentGC (0:35:25 elapsed time, 3:57:30 cpu time, factor 6.70)
Finished AODV (1:12:09 elapsed time, 11:05:09 cpu time, factor 9.21)


The sessions from Bali to JinjaThreads are historically related; this used 
to be the top-end in resource usage until 1-2 years ago.  About 12 years 
ago, MicroJava was in the range of 1h.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Multicore timings

2016-01-15 Thread Gerwin Klein 
Nice! I distinctly remember the times when MicroJava was a very long session ;-)

Cheers,
Gerwin



> On 15 Jan 2016, at 11:16 AM, Makarius  wrote:
>
> Just for the record here are some timings on dual Xeon E5-2620v3 2.40GHz with 
> 12 threads:
>
> Isabelle/9ca00b65d36c + AFP/2c322507b8a6
>
> ML_OPTIONS="-H 2000 --gcthreads 12"
> isabelle build -o threads=12
>
> Finished HOL-Bali (0:00:57 elapsed time, 0:05:26 cpu time, factor 5.71)
> Finished HOL-MicroJava (0:01:04 elapsed time, 0:06:32 cpu time, factor 6.12)
> Finished Jinja (0:02:24 elapsed time, 0:16:13 cpu time, factor 6.75)
> Finished JinjaThreads (0:37:50 elapsed time, 3:55:29 cpu time, factor 6.22)
>
> Finished ConcurrentGC (0:35:25 elapsed time, 3:57:30 cpu time, factor 6.70)
> Finished AODV (1:12:09 elapsed time, 11:05:09 cpu time, factor 9.21)
>
>
> The sessions from Bali to JinjaThreads are historically related; this used to 
> be the top-end in resource usage until 1-2 years ago.  About 12 years ago, 
> MicroJava was in the range of 1h.
>
>
>   Makarius
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




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] Multicore timings

2016-01-15 Thread Lawrence Paulson 
I do remember. It’s almost a shame how years of work can be executed in minutes.
Larry

> On 15 Jan 2016, at 19:16, Makarius  wrote:
> 
> The sessions from Bali to JinjaThreads are historically related; this used to 
> be the top-end in resource usage until 1-2 years ago.  About 12 years ago, 
> MicroJava was in the range of 1h.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Multicore timings

2016-01-15 Thread Makarius 

On Fri, 15 Jan 2016, Lawrence Paulson wrote:


It’s almost a shame how years of work can be executed in minutes.


Lets say that's the struggle for survival of maintainers behind the scenes 
:-)  Both Intel/AMD contributed a little, but David Matthews also did a 
great job.


For the release, I routinely tried SML/NJ as well, but did not get very 
far.  For more than half of the sessions there is a fatal hit on the 
memory wall.  MicroJava still happens to work (lxbroy10 with AMD Opteron 
6176):


  Finished HOL-MicroJava (6:01:55 elapsed time, 6:00:49 cpu time, factor 0.99)
  Finished HOL-MicroJava (5:28:47 elapsed time, 5:28:02 cpu time, factor 0.99)


Makarius___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev