Re: [isabelle-dev] Slow builds due to excessive heap images

2017-11-03 Thread Makarius 
On 03/11/17 16:36, Fabian Immler wrote:
> 
> 
> I think I could reproduce the problem on lxcisa0 (with ML_OPTIONS="--minheap 
> 1600 --maxheap 4000" if that is relevant).
> Invoked with "isabelle build -d . -othreads=8" for the theory below.
> 
> polyml-test-e8d82343b692/x86_64-linux: (0:02:37 elapsed time, 0:18:11 cpu 
> time, factor 6.94)
> polyml-5.6-1/x86_64-linux: (0:00:30 elapsed time, 0:02:24 cpu time, factor 
> 4.70)
> 
> Both are in isabelle/123670d1cff3
> 
> theory Check
> imports Pure
> begin
> 
> ML_file \check.sml\
> ML \timeap Check.check (0 upto 7)\
> 
> end

Just for the record, here are my test results for this setup: lxcisa0,
x86_64-linux, threads=6.

log1.gz: polyml-5.6-1
Finished Check (0:00:56 elapsed time, 0:03:01 cpu time, factor 3.21)

log2.gz: polyml-test-e8d82343b692
Finished Check (0:02:50 elapsed time, 0:13:25 cpu time, factor 4.72)

log3.gz: polyml-NewTestRegisterSave
Finished Check (0:02:53 elapsed time, 0:13:36 cpu time, factor 4.72)

log4.gz: polyml-test-e8d82343b692
ML \
structure IntInf =
struct
  open IntInf
  fun pow (i, n) = Integer.pow n i;
end
\
Finished Check (0:00:39 elapsed time, 0:02:01 cpu time, factor 3.06)


The logs contain profiling information at the bottom. Here is are the
relevant bits of log2.gz vs. log4.gz (produced with "isabelle
profiling_report):

   229 IntInf.divMod
   256 Check.approx_floatarith
   261 IntSet.mergeLists
   281 Check.map
   306 GARBAGE COLLECTION (total)
   352 Check.divide_inta
   468 Check.float_plus_down
  3155 Check.log2
 33415 IntInf.pow

   234 Check.approx_floatarith
   245 IntSet.mergeLists
   276 Check.divide_inta
   307 GARBAGE COLLECTION (total)
   321 Integer.pow
   323 Check.float_plus_down
  1514 IntInf.divMod
  2946 Check.log2

The problem is de-facto solved by the workaround in Isabelle/17eb23e43630.


Makarius




log1.gz
Description: application/gzip


log2.gz
Description: application/gzip


log3.gz
Description: application/gzip


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

Re: [isabelle-dev] Slow builds due to excessive heap images

2017-11-03 Thread Makarius 
On 03/11/17 19:26, Fabian Immler wrote:
> I looked at it once more: profiling told me that IntInf.pow (in combination 
> with Par_List.map) seems to be the culprit.
> 
> The following snippet shows similar behavior:
> ML ‹
> fun powers [] = []
>  | powers (x::xs) = IntInf.pow (2, x mod 15)::powers xs;
> Par_List.map (fn i => powers (i upto 10 * i)) (0 upto 31)
> ›
> 
> polyml-5.6-1/x86_64-linux: 0:00:08 elapsed time, 0:00:35 cpu time, factor 4.02
> polyml-test-e8d82343b692/x86_64-linux: 0:00:36 elapsed time, 0:03:26 cpu 
> time, factor 5.70
> polyml-5.6-1/x86_64-darwin:  0.570s elapsed time, 1.748s cpu time, 0.000s GC 
> time
> polyml-test-e8d82343b692/x86_64-darwin: 522.080s elapsed time, 568.676s cpu 
> time, 42.602s GC time

I have discovered the same and have now pushed a workaround:
http://isabelle.in.tum.de/repos/isabelle/rev/17eb23e43630

Somehow the IntInf.pow implementation in Poly/ML e8d82343b692 is a bit
wasteful, maybe during the bit vector operation instead of our
IntInf.divMod (_, 2) used here: see
http://isabelle.in.tum.de/repos/isabelle/annotate/17eb23e43630/src/Pure/General/integer.ML#l43

With that little change, I get the following very good timings on lxcisa0:

  ML_PLATFORM="x86_64-linux"
  ML_HOME="/home/isabelle/contrib/polyml-test-e8d82343b692/x86_64-linux"
  ML_SYSTEM="polyml-5.7.1"
  ML_OPTIONS="--minheap 4G --maxheap 32G"

$ isabelle build -d '$AFP' -o threads=8 Lorenz_C0
Building Pure ...
Finished Pure (0:00:16 elapsed time, 0:00:16 cpu time, factor 0.95)
Building HOL ...
Finished HOL (0:03:19 elapsed time, 0:10:54 cpu time, factor 3.28)
Building HOL-Analysis ...
Finished HOL-Analysis (0:05:16 elapsed time, 0:28:08 cpu time, factor 5.33)
Building Ordinary_Differential_Equations ...
Finished Ordinary_Differential_Equations (0:01:59 elapsed time, 0:08:10
cpu time, factor 4.10)
Building HOL-ODE ...
Finished HOL-ODE (0:00:01 elapsed time)
Building HOL-ODE-Refinement ...
Finished HOL-ODE-Refinement (0:03:29 elapsed time, 0:20:08 cpu time,
factor 5.76)
Building HOL-ODE-Numerics ...
Finished HOL-ODE-Numerics (0:18:06 elapsed time, 0:41:23 cpu time,
factor 2.28)
Building Lorenz_Approximation ...
Finished Lorenz_Approximation (0:03:43 elapsed time, 0:07:53 cpu time,
factor 2.12)
Running Lorenz_C0 ...
Finished Lorenz_C0 (0:14:21 elapsed time, 1:49:04 cpu time, factor 7.60)
0:51:01 elapsed time, 3:45:59 cpu time, factor 4.43


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

Re: [isabelle-dev] build -x not working anymore

2017-11-03 Thread Makarius 
On 03/11/17 18:43, Fabio Madge Pimentel wrote:
> Building all of Isabelle including the AFP doesn’t work anymore. This can be 
> reproduced with the latest development versions, as well as the tagged 
> Isabelle2017 versions.
> 
>   ./isabelle build -ad ~/afp-devel/thys/ -x HOL

What is the purpose of option -x HOL here?

BTW, the normal place to discuss observations about Isabelle is the
isabelle-users mailing list.


Makarius




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

Re: [isabelle-dev] Slow builds due to excessive heap images

2017-11-03 Thread Fabian Immler 
I looked at it once more: profiling told me that IntInf.pow (in combination 
with Par_List.map) seems to be the culprit.

The following snippet shows similar behavior:
ML ‹
fun powers [] = []
 | powers (x::xs) = IntInf.pow (2, x mod 15)::powers xs;
Par_List.map (fn i => powers (i upto 10 * i)) (0 upto 31)
›

polyml-5.6-1/x86_64-linux: 0:00:08 elapsed time, 0:00:35 cpu time, factor 4.02
polyml-test-e8d82343b692/x86_64-linux: 0:00:36 elapsed time, 0:03:26 cpu time, 
factor 5.70
polyml-5.6-1/x86_64-darwin:  0.570s elapsed time, 1.748s cpu time, 0.000s GC 
time
polyml-test-e8d82343b692/x86_64-darwin: 522.080s elapsed time, 568.676s cpu 
time, 42.602s GC time


> Am 03.11.2017 um 16:36 schrieb Fabian Immler :
> 
> 
> 
>> Am 03.11.2017 um 14:56 schrieb Fabian Immler :
>> 
>> 
>>> Am 02.11.2017 um 18:00 schrieb Makarius :
>>> 
>>> I am more worried about the factor 5 performance loss of Lorenz_C0: now
>>> (3:26:41 elapsed time, 16:49:16 cpu time, factor 4.88). It is unclear if
>>> the problem is related to Flyspeck-Tame. I did not approach it yet,
>>> because the HOL-ODE tower is really huge.
>>> 
>>> It would greatly help to see the problem in isolated spots. I usually
>>> send David specimens produced by code_runtime_trace.
>> At least on my Mac, there seems to be a problem with (or induced by) 
>> parallelism:
>> The attached check.sml is the code extracted from Lorenz_C0.
>> "Check.check xs" does a Par_List.forall on the list xs and Par_list.map in 
>> the computation for individual elements.
>> 
>> With isabelle/fc87d3becd69 and polyml-test-e8d82343b692/x86_64-darwin, 
>> something goes very wrong: a slowdown by a factor of more than 50, compared 
>> to Isabelle2017 .
>> 
>> This seems to be related to parallelism:
>> In check_seq.sml, I replaced Par_List.forall/Par_list.map with list_all/map. 
>> In this case isabelle/fc87d3becd69 behaves more or less like Isabelle2017.
>> 
>> I also tried isabelle/fc87d3becd69 with polyml-5.6-1/x86_64-darwin: this 
>> behaves for both parallel and sequential computations like Isabelle2017.
>> 
>> Unfortunately, I failed to reproduce this behavior on Linux.
> 
> I think I could reproduce the problem on lxcisa0 (with ML_OPTIONS="--minheap 
> 1600 --maxheap 4000" if that is relevant).
> Invoked with "isabelle build -d . -othreads=8" for the theory below.
> 
> polyml-test-e8d82343b692/x86_64-linux: (0:02:37 elapsed time, 0:18:11 cpu 
> time, factor 6.94)
> polyml-5.6-1/x86_64-linux: (0:00:30 elapsed time, 0:02:24 cpu time, factor 
> 4.70)
> 
> Both are in isabelle/123670d1cff3
> 
> --
> 
> theory Check
> imports Pure
> begin
> 
> ML_file \check.sml\
> ML \timeap Check.check (0 upto 7)\
> 
> end
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] build -x not working anymore

2017-11-03 Thread Fabio Madge Pimentel 
Building all of Isabelle including the AFP doesn’t work anymore. This can be 
reproduced with the latest development versions, as well as the tagged 
Isabelle2017 versions.

./isabelle build -ad ~/afp-devel/thys/ -x HOL

Fabio


signature.asc
Description: Message signed with OpenPGP
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Slow builds due to excessive heap images

2017-11-03 Thread Fabian Immler 


> Am 03.11.2017 um 14:56 schrieb Fabian Immler :
> 
> 
>> Am 02.11.2017 um 18:00 schrieb Makarius :
>> 
>> I am more worried about the factor 5 performance loss of Lorenz_C0: now
>> (3:26:41 elapsed time, 16:49:16 cpu time, factor 4.88). It is unclear if
>> the problem is related to Flyspeck-Tame. I did not approach it yet,
>> because the HOL-ODE tower is really huge.
>> 
>> It would greatly help to see the problem in isolated spots. I usually
>> send David specimens produced by code_runtime_trace.
> At least on my Mac, there seems to be a problem with (or induced by) 
> parallelism:
> The attached check.sml is the code extracted from Lorenz_C0.
> "Check.check xs" does a Par_List.forall on the list xs and Par_list.map in 
> the computation for individual elements.
> 
> With isabelle/fc87d3becd69 and polyml-test-e8d82343b692/x86_64-darwin, 
> something goes very wrong: a slowdown by a factor of more than 50, compared 
> to Isabelle2017 .
> 
> This seems to be related to parallelism:
> In check_seq.sml, I replaced Par_List.forall/Par_list.map with list_all/map. 
> In this case isabelle/fc87d3becd69 behaves more or less like Isabelle2017.
> 
> I also tried isabelle/fc87d3becd69 with polyml-5.6-1/x86_64-darwin: this 
> behaves for both parallel and sequential computations like Isabelle2017.
> 
> Unfortunately, I failed to reproduce this behavior on Linux.

I think I could reproduce the problem on lxcisa0 (with ML_OPTIONS="--minheap 
1600 --maxheap 4000" if that is relevant).
Invoked with "isabelle build -d . -othreads=8" for the theory below.

polyml-test-e8d82343b692/x86_64-linux: (0:02:37 elapsed time, 0:18:11 cpu time, 
factor 6.94)
polyml-5.6-1/x86_64-linux: (0:00:30 elapsed time, 0:02:24 cpu time, factor 4.70)

Both are in isabelle/123670d1cff3

--

theory Check
imports Pure
begin

ML_file \check.sml\
ML \timeap Check.check (0 upto 7)\

end




smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] the new "imports" semantics

2017-11-03 Thread Lawrence Paulson 
This makes sense. Many thanks!
Larry

> On 3 Nov 2017, at 13:13, Makarius  wrote:
> 
> * Only the most fundamental theory names are global, usually the entry
> points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
> FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
> formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
> 

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

Re: [isabelle-dev] the new "imports" semantics

2017-11-03 Thread Makarius 
On 02/11/17 19:13, Lawrence Paulson wrote:
> It’s nice that global theories don’t have to be qualified. But it’s a bit 
> strange that it's forbidden to qualify them.

I have checked this again in the history, e.g. Isabelle/db1827610513.
Global theories in regular application sessions were merely a left-over
from early exploration of the possibilities. Only Probability and SPARK
were still remaining.

In NEWS of Isabelle/2c2a346cfe70 the situation is now explained as follows:


*** General ***

* Only the most fundamental theory names are global, usually the entry
points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".


*** Prover IDE -- Isabelle/Scala/jEdit ***

* Completion supports theory header imports, using theory base name.
E.g. "Prob" is completed to "HOL-Probability.Probability".


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