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

[Makarius]

On 02/11/17 18:00, Makarius wrote:
> On 02/11/17 16:11, Lars Hupel wrote:
>>
>> Tobias and me have discovered an interesting discrepancy between your
>> AFP slow setup and our AFP slow setup. They run on identical hardware
>> with the only difference of 6 vs 8 threads. On 6 threads, it runs
>> significantly faster. For example, Flyspeck-Tame requires 9:44:16
>> (elapsed time on 8 threads) vs 8:50:55 (elapsed time on 6 threads).
> 
> It was merely my intuition about the virtual hardware that using less
> resources than allocated might help. But I did not make any measurements
> with 8 vs. 6 threads, so that guess might be still wrong.
> 
> The main observation so far: it works quite well and measurements are
> reasonably stable.

Here are current and more detailed results (see dump.csv), from the
following database query:

SELECT log_name, pull_date, timing_elapsed, timing_cpu, timing_factor,
ml_timing_elapsed, ml_timing_cpu, ml_timing_gc, ml_timing_factor,
threads, "ML_SYSTEM", "ML_PLATFORM", "ML_OPTIONS"
FROM isabelle_build_log
WHERE session_name = 'Flyspeck-Tame' AND (build_host = 'lrzcloud1' OR
build_engine = 'jenkins') AND pull_date > now() - INTERVAL '20 days'
ORDER BY log_name

An SQLite snapshot of that data is here:
http://isabelle.in.tum.de/devel/build_log.db -- note that SQLite lacks
advanced date functions like INTERVAL above.

Charts are here: http://isabelle.in.tum.de/devel/build_status


David Matthews has already done a great job in tuning current the
performance of Poly/ML 5.7.1 test versions, so most AFP slow sessions
have become significantly faster. Current polyml-test-fb4f42af00fa from
Isabelle/ce6454669360 looks like a very good release candidate.

For Flyspeck-Tame a small performance loss remains. It might be worth
trying to configure the Isabelle/HOL codegen to use FixedInt instead of
regular (unbounded) Int. Thus it could become faster with Poly/ML 5.7.1
than with 5.6.


	Makarius
-------------- next part --------------
A non-text attachment was scrubbed...
Name: dump.csv
Type: text/csv
Size: 8405 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20171107/4adec3ab/attachment-0002.csv>