'minimize' runs

[Norman Megill]

(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

[Norman Megill]

(Switching to the mininmize thread)

On Tuesday, December 17, 2019 at 12:46:30 PM UTC-5, David A. Wheeler wrote:

>The last one I did myself was around 3 years ago, using a laptop with a
>powerful i7 processor maxed out with 8 threads.

Can metamath automatically use all the CPUs available when doing a minimize run?

metamath.exe can only use one core, and as FL said you have to run separate processes, doing it in pieces.  (I'm not sure how that would be done in the program, but I would guess it would involve system-specific calls, making it non-ANSI.)
 

> The CPU ran quite hot
>(Speccy reported around 90-95C even with a new fan), and it died near
>the end.

All systems have temperature measures that should prevent any permanent damage and automatically slow down as necessary. Also, some modern computers are designed to run absurdly hot. Yes, some systems have defects in their temperature measurement systems, but those should be relatively rare. So you should not be afraid to run a minimization.

The laptop was an HP 8570p.  IIRC the CPU was spec'ed to run up to 100C, so it probably was throttling.  However, keeping that high continuously for weeks may have shortened its life.  I think I've seen a recommendation to keep CPUs under 80C for long life.

I just checked out the us2 server, and maxing the CPU (4 processes) raised the temperature to 83C (in a cool room at 18C), which seems high and makes me uncomfortable.  It may have a bad fan, but I would have to shut down us2 to find out and fix.  When I ran one process (such as the site build), the temperature increased to only 50C, so I can postpone looking into this until there's a slow period for contributions.
 

I might be able to run minimization on a useful beefy system, but I'll have to check first.

I'll update the script I gave to Dylan Houlihan and post it somewhere, and people can do whatever parts they want, with some informal coordination with me.

The basic idea is to run 'minimize */a */n ax-*' on each proof and send the results (in a log file) to me, without saving the proof.  After I collect all the results, I will create a one-off script to do the actual proof updating.  The actual updating is fast because 'minimize' is run against single theorems, and it will be a one-time change to set.mm.

There's no rush for doing this.  Even if set.mm changes in the interim, worst case it just means some minimizations may not happen, but they will catch up in the next year's round.

I'll wait until the proposed moves of mm100 theorems etc. to the main set.mm are completed so it can be as accurate as possible.

Norm

[Benoit]

The basic idea is to run 'minimize */a */n ax-*' on each proof and send the results (in a log file) to me, without saving the proof.

Maybe add the options /VERBOSE /TIME to have all the information possible.

Benoît

[Norman Megill]

Yes, I forgot to include /time, which was also used in the runs 2 years ago.  I had in mind finding a function that correlated proof size and set.mm position to run time (at least roughly) to help plan jobs with more predictable run times, but I never got around to it.  I still have the data, though.

No, /verbose is primarily for me to help with debugging.  I think it might confuse the current script that assembles all the log files into the final minimize run.

Norm