Hi,
Thank you for narrowing the error down. It should now be fixed.
There were a lot of cases where code that worked correctly on the native
address versions failed in the 32-in-64 version and had to be modified.
I'm sure there are still some cases that haven't been tested.
Regards,
David
O
Hello.
I localized the error finally. Whew!
Yes, it is *only* on 32-in-64 and it is reproducible with 100% on
FreeBSD and CentOS.
I prepared simple code for reproduce the error.
It is FFI callback.
> cat callback.c
void foo ( int n, void (*fn) (int) ) {
int i = 1;
while (n--) {
On 23/01/2019 08:42, Chun Tian (binghe) wrote:
>
> P. S. I think PolyML is already fast enough for HOL4, especially when you see
> how slow the Moscow ML builds are:) In Isabelle, every time when the user
> click inside the JEdit editor, it may trigger some computation at the PolyML
> side, I
Hi David,
the short answer is, comparing with 5.7.1 release, both the latest master and
the 32-in-64 option make the difference, but actually not that big as I
reported yesterday.
Here are the test steps (of each round):
1. I do a full build of HOL4 in my working branch (in which the probabili
Thanks, that's interesting. Have you tried the latest master with
native 64-bits? It would be useful to know whether it's the 32-in-64
that makes the difference for HOL4 or the changes to the code-generator.
Regards,
David
On 22/01/2019 11:42, Chun Tian (binghe) wrote:
I observed about 10%
Thanks for the report. Did you see anything similar with the native
code version? It could be a code-generator problem which would affect
other versions or it could be something specific to 32-in-64.
Unfortunately the stack trace doesn't tell me much other than that it
looks as though it fail
I observed about 10% performance improvements in HOL4, between 5.7.1 release
(x86_64) and latest master with the --enable-compact32bit option.
—Chun
> Il giorno 20 gen 2019, alle ore 19:17, David Matthews
> ha scritto:
>
> I've now merged a major piece of development work into GitHub master.
Hello.
I got one error with compact32bit on 64bit:
(gdb) bt
#0 0x821f5400 in ?? ()
#1 0xff9ab2b0 in ?? ()
#2 0xff9ab2b2 in ?? ()
#3 0x000d021fff10 in ?? ()
#4 0x000d821f9e1c in ?? ()
#5 0x000d821f9f00 in ?? ()
#6 0x000d021fff38 in ?? ()
#7 0x
I've now merged a major piece of development work into GitHub master.
This is a variant of 64-bit mode that uses 32-bit values. It was
triggered by the observation that Isabelle often peformed better with
the 32-bit version than the 64-bit despite the 64-bit version allowing a
much larger heap
