(Switching to new topic; was: Re: Proven: Fourier series convergence, #76)
On Monday, December 16, 2019 at 9:17:04 PM UTC-5, Mario Carneiro wrote:
>
> Wouldn't running the program with sleeps in it or with a scheduling
> setting ("nice" / process priority) such that it only consumes X% of the
> CPU resolve the "running hot" problem? Also it could be broken into smaller
> pieces and run multithreaded or on multiple computers to compensate. How
> hard would it be to break up the workload?
>
Well, metamath.exe could in principle be modified with periodic sleeps in
the minimize algorithm. Also there is a program (I'd have to look it up)
that I used on an old overheating Windows XP laptop to have the CPU idle
every other clock cycle or something, but regular usage became annoyingly
slow. As for breaking it up into smaller pieces, each theorem can be
minimized separately. Within a theorem (a few large proofs take a day or
more to minimize) the minimize can be broken down into ranges of statements.
So yes, there are various things that can be done if the computer is not
designed for continuous CPU usage, like many laptops apparently. Even my
current i5 laptop overheats with maxed out CPU. In the end though, wasting
time going through hoops to prevent overheating seems like a thankless
task, when a desktop with decently designed cooling can probably handle
continuous CPU usage with no hassle.
The only desktop I have is the us2 server, which I'd prefer not to risk
burning out its CPU. Interestingly, though, I just learned that 'cat
/sys/class/hwmon/hwmon0/temp[2-5]_input' shows the temperature of its 4
cores in milli-Celcius. When I get a chance maybe I will max out its CPU
to see how hot it gets, and if it seems safe I can let 'minimize' run in
the background for several weeks.
Norm
> Mario
>
> On Mon, Dec 16, 2019 at 6:56 PM Norman Megill wrote:
>
>> On Monday, December 16, 2019 at 4:43:01 PM UTC-5, Benoit wrote:
>> ...
>>
>>>
>>>> > unfortunately I miss some of the features of metamath.exe , because I
>>>> use mmj2 only (but I'm really intrigued by Thierry's plugin for Eclipse, I
>>>> hope I will soon have time to take a closer look at it).
>>>> > If I'm not mistaken, Normann periodically runs a "minimize" on the
>>>> all set.mm, and that will help.
>>>>
>>>> Yes, but I think "periodically" used to be once a year, but a bit less
>>>> now, and I'm not sure it looks at the mathboxes. Anyway, minimizing is
>>>> not
>>>> a requirement.
>>>>
>>>
>> The last global minimize run was about 2 years ago, volunteered by Dylan
>> Houlihan who ran it on some powerful servers he had available, over a
>> period of maybe a couple of weeks.
>>
>> The last one I did myself was around 3 years ago, using a laptop with a
>> powerful i7 processor maxed out with 8 threads. The CPU ran quite hot
>> (Speccy reported around 90-95C even with a new fan), and it died near the
>> end. I finished it on another computer.
>>
>> Since then I've become somewhat afraid of maxing out the CPU for long
>> periods, and I don't have a plan to do it again soon. If anyone wants to
>> volunteer (or several people each working on a range), that would of course
>> be welcome.
>>
>> We can make 'minimize' look at other (earlier) mathboxes with
>> '/include_mathboxes', but the output should be carefully vetted due to
>> occasional matches to overly specialized theorems that we don't want to
>> import.
>>
>>
>>>> I think that the objective of "minimize" is precisely what you're
>>>> asking for: you do not have to remember all the labels, and only use the
>>>> basic jca, sylibr, etc. And once the proof is done, "minimize" will
>>>> optimize them, using sylanbrc, etc
>>>>
>>>
>> Yes, that is the intent, and it will optimize many such cases of
>> inefficient "glue logic".
>>
>> Norm
>>
>
--
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/3d752a35-d2db-47b9-a5cb-c41fb59b82f3%40googlegroups.com.
