By default ignore any statements marked (New usage is discouraged.)

[david-a-wheeler]

By default searches, unifications that add statements, and bottom-up proofs should skip any statement (an axiom or theorem) with a comment that includes the text "(New usage is discouraged.)". This should be a checkbox in "Settings":

(Checkbox) Ignore statements marked with "(New usage is discouraged.)"
(default checked).

If a user hand-adds such statements (say in a justification or as a root of a bottom-up search) then that's fine, and it shouldn't remove them. The point is that the tool should not be automatically adding or reporting them by default.

[expln]

This is partially implemented, but it is not so convenient as you proposed. Could you please review (if not already) the existing feature if it resembles what you described? starting at 2:30, ending at 3:45 in this demo https://drive.google.com/file/d/1haJff_AN1M6HZGrWXsgqzrxq-Di84gmZ/view?t=150

What I am going to change:

1. Add a new setting as you suggested. But it will be not a check box. It will be a regex with an appropriate default value (to skip what you suggested).
2. Both existing setting "Assertions to skip" and the new one will be merged (I mean the sets of assertions produced by them will be merged).
3. Currently usage of a discouraged assertion is a critical error not allowing to proceed. I will change it to a warning so users will see there is a potential problem but they still can work.
4. Currently discouraged assertions are not appearing anywhere including search and bottom-up proofs. I will add a check box to these places "allow discouraged assertions" so users may use them if they wish.

[david-a-wheeler]

The feature described at 2:30 is somewhat similar. However, since discouragement is usually marked in a database with a special comment, I think it's more important to at least directly support that.

Using a regex is definitely more flexible. Having a way to control which statements are considered discrouaged, and control the text used to infer that a statement is discouraged, would certainly do I what I'd like! I think it's important that the default be the exact text sequence already used in set.mm/iset.mm, and that it be enabled by default. Once that happens, proofs won't accidentally use discouraged statements.

There are cases where you want to use a discouraged statement, so I would not make that an error. However, it should require an express selection by the user. Having a checkbox on search and backwards proof to allow them, but skipping them by default, would make that easy. Thanks!

[david-a-wheeler]

We definitely also want to ignore syntax axioms with "new usage is discouraged" - the current fragment selector gets confused because of this :-).

[expln]

Sure, it is also mentioned here #108