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

> They are just identifiers and I don't think they are computed with. > However, I don't intend to change formalization beyond a global > implementation of int by some fixed size integers, if that can be done > easily. Otherwise we live with the increase in runtime from 7:20 to 8:20. Hence a

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

On 16/11/2017 12:43, Florian Haftmann wrote: Dear all, The idea above is to provide an option for the HOL codegen that is used specifically for applications like Flyspeck-Tame. It is mainly a question to codegen experts, if that can be done easily. streamlining execution of Flyspeck-Tame

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

Dear all, > The idea above is to provide an option for the HOL codegen that is used > specifically for applications like Flyspeck-Tame. It is mainly a > question to codegen experts, if that can be done easily. streamlining execution of Flyspeck-Tame without risking its integrity is a struggle

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

If there are fixed-size integers in ML that raise an exception on overflow, it should be possible to just do appropriate code_printing setup similar to what Code_Target_Numeral does. We already have to somehow magically map Isabelle's "int" type to ML's "IntInf" type, so all we have to do is to

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

On 08/11/2017 14:13, Makarius wrote: On 08/11/17 12:35, Tobias Nipkow wrote: On 07/11/2017 23:13, Makarius wrote: 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

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

Hi Makarius, On 08/11/17 14:13, Makarius wrote: On 08/11/17 12:35, Tobias Nipkow wrote: On 07/11/2017 23:13, Makarius wrote: 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.

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

On 08/11/17 12:35, Tobias Nipkow wrote: > > On 07/11/2017 23:13, Makarius wrote: >> 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

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

On 07/11/2017 23:13, Makarius wrote: 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. Just as for Isabelle

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

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 >>

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

On 04/11/17 19:30, David Matthews wrote: > > I've had a look at this and pushed a change to IntInf.pow to Poly/ML > master (c2a2961).  It now uses Word.andb rather than IntInf.andb which > avoids a call into the run-time system (RTS). > > However, this code hadn't changed since 5.6 and when I

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

On 03/11/2017 19:07, Makarius wrote: 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) =

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

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

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

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

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

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))

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

> 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 >>

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

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,

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

> We are presently testing Poly/ML 5.7.1 by default (see > Isabelle/aefaaef29c58) and there are already interesting performance > figures, e.g. see: > > http://isabelle.in.tum.de/devel/build_status > http://isabelle.in.tum.de/devel/build_status/Linux_A >

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

I should have sent the message below also to isabelle-dev, sorry about that. Has anything changed about integers in Poly/ML 5.7.1? Lorenz_C0 did slow down by a factor of 5, which I find quite extreme. Best, Fabian > Am 28.10.2017 um 23:57 schrieb Fabian Immler : > > Lorenz_C0

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

On 28/10/17 22:26, Makarius wrote: > > I still have some ideas for "isabelle build" in the pipeline (for > several years) to skip building intermediate heaps in the first place. > Then AFP (without the "slow" sessions) could shrink to 50% .. 20% build > time. > > Until that emerges, AFP

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

On 29/10/2017 21:52, Makarius wrote: On 28/10/17 22:26, Makarius wrote: Overall, performance is mostly the same as in Poly/ML 5.6 from Isabelle2017, but there are some dropouts. In particular, loading heap images has become relatively slow: this impacts long heap chains like HOL-Analysis or

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

On 28/10/17 22:26, Makarius wrote: > > Overall, performance is mostly the same as in Poly/ML 5.6 from > Isabelle2017, but there are some dropouts. In particular, loading heap > images has become relatively slow: this impacts long heap chains like > HOL-Analysis or big applications in AFP. E.g.

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

On 28/10/17 22:26, Makarius wrote: > We are presently testing Poly/ML 5.7.1 by default (see > Isabelle/aefaaef29c58) and there are already interesting performance > figures, e.g. see: > > http://isabelle.in.tum.de/devel/build_status > http://isabelle.in.tum.de/devel/build_status/Linux_A >