> > VM with 64 cores > Neither ACL2 nor underlying gcl makes any use of threads or locks
I assume the 64-core box has adequate memory as well. For me, also on a 64-core box with "only" 128GB RAM, acl2 takes a three-digit number of gigs for itself, ignoring any other processes that are also running on the machine. It keeps doing something nasty, with garbage collection prominently showing in stack traces. On a small box, it also hogs most of the memory for itself, being strongly anti-social, but finishes successfully. On a tiny box that's still fine for building any other package, it OOMs. Meow! -- ⢀⣴⠾⠻⢶⣦⠀ ⣾⠁⢠⠒⠀⣿⡁ If you ponder doing what Jesus did, remember than flipping tables ⢿⡄⠘⠷⠚⠋⠀ and chasing people with a whip is a prime choice. ⠈⠳⣄⠀⠀⠀⠀
