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 > execution times > and 30-40% improvement in the size of saved states on some typical ProofPower > examples.
After some weeks with --enable-compact32bit, which Isabelle is already using by default, here is my wrap-up of it: * The underlying architecture is x86_64, so we can discontinue the old x86 platform: it has become increasingly difficult to use that on Linux and macOS, potentially also Windows within the next few years. * Overall stability is better than x86, which often ran into the VM boundary of less than 4GB. * Applications that require substantial heap space run faster, sometimes much faster -- on current hardware with 8 GB RAM or more, e.g. see https://isabelle.sketis.net/devel/build_status/Mac_OS_X_10.14_High_Sierra_4_threads/index.html after 21-Feb-2019. * Old hardware with only 4GB can get into problems, with slightly degraded performance, e.g. see the particular the routine AFP measurements that are run on really ancient server machines, see https://isabelle.sketis.net/devel/build_status/AFP/index.html Overall great work by David Matthews. We are ready for the next 10 years. We merely need to do the final testing of big applications for the official release. Makarius _______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
