I'm unclear about what prompted this and why it is considered a problem. I don't see why we should care whether someone wants to use dummylink or idi for whatever reason. They are harmless, and all they do is make the proof slightly less efficient. It is a trivial and temporary cosmetic issue that will go away when 'minimize' is run. I would prefer not to have 'discouraged' tags, because it will make these a nuisance to use in the occasional cases where they are useful.
BTW the eimm program generates a script for MM-PA that uses 'assign' commands to rebuild a partial proof from an mmj2 worksheet, using dummylink to connect isolated subproofs in the mmj2 proof. If dummylink is 'discouraged', the proof building will corrupted unless the user first issues a global 'set discouragement off', defeating the purpose of 'discouraged'. And it will be another thing for the user to learn or be unpleasantly surprised by. Benoit mentioned an earlier discussion in PR#1105 where a 'minimize' did not remove idi, and it was because of 'discouraged' tags in theorems referenced by the proof. Normally this will not be an issue - if a theorem is 'discouraged', it normally shouldn't be used in a new proof to begin with. But in any case, 'minimize' has '/override' that will allow it to try 'discouraged' theorems, and that is fine to use as long as you carefully inspect what it did. On Sunday, January 12, 2020 at 9:15:44 PM UTC-5, David A. Wheeler wrote: > > On Sun, 12 Jan 2020 18:02:14 -0800 (PST), Norman Megill wrote: > > > > > Alan Sare's tool "completeusersproof" appears to make use of idi, at > least > > it appears in his C code and is referenced extensively in the program > > comments. Although this program probably has a very small user base, I > > think we should leave in idi and also not mark it discouraged so that > > proofs generated by the code won't be rejected. Any idi usage in the > > generated proofs will be removed by 'minimize'. > > We could just ask people to use 'minimize' before submitting proofs > generated > by that tool. The redundant idi's will be removed when we run a global minimization, so it's not strictly necessary. They don't take up much space in the proof. More importantly, I don't know how the tool works, and having a discouraged idi might unnecessarily increase risk of something going wrong, like with eimm. In any case, of course it is nice when people 'minimize' before they submit, and I encourage people to do that. But a long time ago I asked people to do that and got complaints it was too much trouble. So I've given up on that. So we do global minimizations to take care of it. Norm > > But if that's not convincing enough, that's fine. > I couldn't think of a reason *not* to do this, but I didn't know about > those > other situations. You learn something every day!! > > If idi won't be marked like this, I'll probably propose to Mario > that this RunParms.txt line: > ProofAsstUnifySearchExclude,biigb,xxxid,dummylink > be changed to: > ProofAsstUnifySearchExclude,dummylink,idi > I think that for mmj2 users it would have a similar effect. > > --- 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/8317e6be-cc17-4de8-821d-38c27a78fd22%40googlegroups.com.
