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?Mario On Mon, Dec 16, 2019 at 6:56 PM Norman Megill <[email protected]> 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/88ec959b-90d2-4805-b4e9-6a5e898cfdad%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/88ec959b-90d2-4805-b4e9-6a5e898cfdad%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSvVPT3pL1p1bR3HTV5eab%3DD5GnvE4RRs%2BfuC8dLa0NHkA%40mail.gmail.com.
