Since these things are hard to enforce, maybe we could make clear the following guidelines for contributors (e.g., in ~conventions and mmset.html): - when adding theorems to Main (be it direct addition or moving from a mathbox) running MINIMIZE_WITH is required; - when adding a theorem to one's mathbox, running MINIMIZE_WITH is strongly recommended, - if for some reason, this is not possible, then you should add to its comment "(Minimization pending.)". If minimization is not desirable, add the tag "(Proof modification is discouraged.)" preceded by a short explanation why this is so (or: which property of the proof should be kept). Failure to do so will cause the spirit of Metamath to haunt you for seven years.
An idea for bulk minimization: let A be the set of all theorems of Main added/modified since the previous bulk minimization; then run "minimize_with *" on all theorems in A, and run "minimize_with A" on all other theorems in Main. Alexander: I'm pleasantly surprised that ~bj-eleq2w allows a minimization (probably avoiding a use of ~cv, compared to ~eleq2 ?). Its main goal is to reduce axiom dependencies (actually, that section of my mathbox shows how dependency on ~ax-ext, among others, can be removed from several dozens theorems --- yes, ~ax-ext is used in the eliminability theorem, but this is still interesting). If Norm agrees and you don't mind, I'll move it to Main, to its place, which is right after df-clel. Side note: ~bj-eleq2w actually uses fewer axioms than ~eleq2, since the latter does "morally" use ax-5--9 and ax-ext, as bj-dfclel and bj-dfcleq show. Benoît On Saturday, December 12, 2020 at 6:32:06 PM UTC+1 David A. Wheeler wrote: > > > On Dec 11, 2020, at 10:13 PM, Norman Megill <[email protected]> wrote: > > > > Benoît suggested that we require proofs to be minimized before > submission. > > I think we should encourage that. I think requiring is too strong, but > simply making that request clear is reasonable enough. > > > I propose we add a temporary tag to recent set.mm proofs that lets us > know whether or not "minimize_with" has been run. Volunteers can, at their > leisure, minimize the proofs that haven't been. .,.. > > I'd like to hear opinions or suggestions. > > I disagree. It does not really help. Minimization is often enabled by > adding something *else* later, so such tags would be misleading. In > addition, adding them would be a pain & create a lot of useless fluff. > > > In the past, every year or two we would run "minimize_with" on the > entire set.mm. But as set.mm has grown, doing this has become a somewhat > large project. > > To me the solution is clear: automation. When we started last time almost > nothing was automated. I ended up writing some scripts to automate parts of > it, but that was done on the fly *during* the minimization. Instead, let’s > play on letting the computers do all the work. If it’s going to happen > annually, then let’s treat it as something that automatically happens > annually. > > --- David A. Wheeler > > -- 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/52e84154-003c-4065-9362-227a842b2c66n%40googlegroups.com.
