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

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

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

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

[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

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

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

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