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

[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 \<open>check.sml\<close>
> ML \<open>timeap Check.check (0 upto 7)\<close>
> 
> 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 \<open>
structure IntInf =
struct
  open IntInf
  fun pow (i, n) = Integer.pow n i;
end
\<close>
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


-------------- next part --------------
A non-text attachment was scrubbed...
Name: log1.gz
Type: application/gzip
Size: 14511 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20171103/cecb16e0/attachment.gz>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: log2.gz
Type: application/gzip
Size: 14557 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20171103/cecb16e0/attachment-0001.gz>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: log3.gz
Type: application/gzip
Size: 14718 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20171103/cecb16e0/attachment-0002.gz>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: log4.gz
Type: application/gzip
Size: 14988 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20171103/cecb16e0/attachment-0003.gz>