On Tue, 18 Feb 2020 12:16:22 -0800, Mario Carneiro <[email protected]> wrote: > All of the jobs I have run thus far are on AWS, on a single instance. So > while it may not have been on a single physical machine, it is unlikely to > vary significantly. It's a linux machine, and I compiled it using DAW's > script (I didn't check but I hope it compiled with optimizations!).
Yes, it compiles with optimizations. If you run "scripts/build-metamath" as recommended, that in turn runs "autoconf -i" and the generated "./configure" file. Normally that will turn on a variety of optimizations, in particular it will enable -O3 (level 3 = top level) optimizations. I just reran this on Cygwin, and it shows a number of optimizations: -O3 -funroll-loops -finline-functions -fomit-frame-pointer -DINLINE=inline Exactly what options this enables depends on a variety of factors, but it's optimizing for speed of execution (which is what you want). --- David A. Wheeler -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1j4CbX-0002ww-9U%40rmmprod07.runbox.
