Re: [polyml] Testing Poly/ML 5.8

2019-03-10 Thread Makarius
On 10/03/2019 20:28, Rob Arthan wrote: > > After the "git pull", I've rebuilt Poly/ML and ProofPower and had no problems > with any > combination of --enable-intinf-asint, --enable-compact32bit and MacOS v. > Fedora. > > Poly/ML compiled with --enable-compact32bit gives me 5-8% improvement in

Re: [polyml] Testing Poly/ML 5.8

2019-03-10 Thread Rob Arthan
David, After the "git pull", I've rebuilt Poly/ML and ProofPower and had no problems with any combination of --enable-intinf-asint, --enable-compact32bit and MacOS v. Fedora. Poly/ML compiled with --enable-compact32bit gives me 5-8% improvement in execution times and 30-40% improvement in the

Re: [polyml] Testing Poly/ML 5.8

2019-03-10 Thread David Matthews
On 09/03/2019 21:10, Rob Arthan wrote: OK. Is there a way of telling whether poly has been built with --enable-compact32bit? (So you can check whether you got what you wanted.) > PolyML.architecture(); val it = "X86_64_32": string > Word.wordSize; val it = 31: int > LargeWord.wordSize; val it

Re: [polyml] Testing Poly/ML 5.8

2019-03-10 Thread David Matthews
Rob, Phil and everyone else, I'm in the process of putting together the 5.8 release and as part of that I've pushed an updated pre-built compiler for X64/32 for Linux, Mac OS etc. That means that for that platform only, for the moment, it is no longer necessary to run "make compiler", althoug

Re: [polyml] Testing Poly/ML 5.8

2019-03-10 Thread Phil Clayton
Rob, On 09/03/19 21:10, Rob Arthan wrote: On 9 Mar 2019, at 16:59, David Matthews wrote: 3) On MacOS with —disable-intinf-asint and —enable-compact32bit, the ProofPower build fails like this: Assertion failed: (space != 0), function ScanObjectAddress, file quick_gc.cpp, line 414. 4) On Fedor