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.
