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