Should we make both discouragement tags mandatory in *OLD and *ALT?

[Norman Megill]

On 2/13/20 9:25 AM EST, Benoit wrote [in the "Full 'minimize' run on set.mm" thread]:

>
> Actually, most *OLD and *ALT should probably have both discouragement
> tags as well, it seems ?
>
> Thanks,
> Benoît

*ALT theorems in the full job logs (not just the suspicious proof size decreases that I posted) are creating unnecessary manual cleanup effort to get  things to a point where I can run the final minimization.

To avoid this problem in the future, I am wondering if it would be acceptable to make Benoit's suggestion mandatory and to have 'verify markup' check for it.

Does anyone see any problem in requiring *OLD and *ALT to have both discouragement tags ["(New usage is discouraged.)", "(Proof modification is discouraged.)"] always? Is there ever any reason for not having these tags? (If in some special case an *ALT could benefit from 'minimize' or a proof revision, we can always use '/override' on a custom basis for that purpose.)

Norm

[Thierry Arnoux]

I would agree that both tags shall be used on *ALT and *OLD theorems.

[Alexander van der Vekens]

To check that both tags are provided for *OLD statements is OK.

I would feel not comfortable, however, if all ALT theorems/definitions must have both tags. "(New usage is discouraged.)" would be OK, but not "(Proof modification is discouraged.)". I think we have two meanings of ALT: alternate proofs or alternate definitions/variants of theorems. For the first case "(Proof modification is discouraged.)" makes sense, but not for the second case: here I would like to have shorter proofs (found automatically) if possible. A solution could be to provide two separate suffixes: ALTP for "alternate proof", ALT for "alternate definitions/variants of theorems".

[Norman Megill]

Since there were no other replies, unfortunately I just updated set.mm with both discouragements on every ALT because of the problems they were creating.  I suppose I could revert and do the analysis all over, but I want to get the minimizations applied soon without unwanted side effects.  How many of your theorems does this affect?

I think our tradition has been to use ALT for alternate proofs, so overwriting the proof with the non-ALT version is undesirable.  Should we even be using ALT for variations of theorems as opposed to alternate proofs?  What is the purpose of having a modified theorem in set.mm if it isn't intended to be used?  Or it if is intended to be used, perhaps a different theorem name like dfss2, dfss3,...

Of course the ALT proof can still be minimized with overrides, after someone analyzes the purpose of the ALT in each case.  Perhaps we should consider the ALT suffix as meaning "avoid" and "needs special handling" in which case both discouragements would be appropriate in general.

Norm

[Alexander van der Vekens]

On Tuesday, February 25, 2020 at 7:00:48 PM UTC+1, Norman Megill wrote:

Since there were no other replies, unfortunately I just updated set.mm with both discouragements on every ALT because of the problems they were creating.  I suppose I could revert and do the analysis all over, but I want to get the minimizations applied soon without unwanted side effects.  How many of your theorems does this affect?

Sorry, I was on a journey over the weekend...

But don't worry, there are some ALT definitions/theorems in my mathbox about magmas/semigroups and graphs which are affected. For these, I can take care by myself.  So if we use ALT for alternate proofs only (in  the future), we could use Alt for "alternate definitions/variants of theorems". Then we can check the tags for *ALT theorems, and will have no checks for *Alt theorems.

[Norman Megill]

Not sure if "Alt" vs. "ALT" will be confusing;  I was going to suggest ALTV for alternate version.  But any suffix will do.  What I propose is that the ALT suffix be treated as a kind of markup keyword that will always require both discouragements, regardless of what it is used for, and anything else like *Alt or *ALTV will be ignored by 'verify markup' i.e. treated as just another label so you can do anything you want with it as far as discouragements.

Basically, then, *OLD and *ALT will be the only "keyword" patterns recognized by 'verify markup' for the time being and will require both discouragements.  It might be useful to add more patterns in the future, but let's keep it simple for now.  The essential difference between OLD and ALT is that OLD will expire and eventually be deleted.  Agreed?

Therefore I won't revert the discouragement commit, and at some point you can change the labels and discouragements in your mathbox per your preference.  I'm not aware of any other such situations outside of your mathbox, but if there are any they can be handled individually as the need arises.

Norm

[Alexander van der Vekens]

On Tuesday, February 25, 2020 at 9:02:25 PM UTC+1, Norman Megill wrote:

On Tuesday, February 25, 2020 at 1:40:54 PM UTC-5, Alexander van der Vekens wrote:

On Tuesday, February 25, 2020 at 7:00:48 PM UTC+1, Norman Megill wrote:

Since there were no other replies, unfortunately I just updated set.mm with both discouragements on every ALT because of the problems they were creating.  I suppose I could revert and do the analysis all over, but I want to get the minimizations applied soon without unwanted side effects.  How many of your theorems does this affect?

Sorry, I was on a journey over the weekend...

But don't worry, there are some ALT definitions/theorems in my mathbox about magmas/semigroups and graphs which are affected. For these, I can take care by myself.  So if we use ALT for alternate proofs only (in  the future), we could use Alt for "alternate definitions/variants of theorems". Then we can check the tags for *ALT theorems, and will have no checks for *Alt theorems.

Not sure if "Alt" vs. "ALT" will be confusing;  I was going to suggest ALTV for alternate version.  But any suffix will do.  What I propose is that the ALT suffix be treated as a kind of markup keyword that will always require both discouragements, regardless of what it is used for, and anything else like *Alt or *ALTV will be ignored by 'verify markup' i.e. treated as just another label so you can do anything you want with it as far as discouragements.

Basically, then, *OLD and *ALT will be the only "keyword" patterns recognized by 'verify markup' for the time being and will require both discouragements.  It might be useful to add more patterns in the future, but let's keep it simple for now.  The essential difference between OLD and ALT is that OLD will expire and eventually be deleted.  Agreed?

Yes, I fully agree!

Therefore I won't revert the discouragement commit, and at some point you can change the labels and discouragements in your mathbox per your preference.  I'm not aware of any other such situations outside of your mathbox, but if there are any they can be handled individually as the need arises.

Also OK for me.