Re: [isabelle] sledgehammer in RC4



On 11/14/2013 3:13 PM, Randy Pollack wrote:
The issue is complicated by the fact that I'm running Ubuntu in a VBox
virtual machine. Probably (but I don't know, and haven't been able to
ascertain from VBox documentation) VBox simply spawns guest threads
and leave it to the host OS to schedule them.  That would imply that
no harm is done by telling isabelle the number of hyperthreads rather
than the number of cores.

Unless someone on the list knows about this, experimentation is required.

You probably already know this, but for others who haven't used it, the settings I show are useful to keep VirtualBox from hogging up all the CPUs.

For a machine in VirtualBox, there is the setting "Setting/System/Processor", where you can set the number of processors for a VirtualBox machine.

I attach a screen shot for my dual core laptop. It shows I have it set to 2, but that 4 processors are available. I don't know if I set that, or if that's the default.

Regards,
GB

Attachment: vBox cpus.png
Description: PNG image



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.