Fix #6434: new option --no-infer-absurd-clauses

[andreasabel]

Fix #6434: new option --no-infer-absurd-clauses.

This option switches off automatic filtering of absurd clauses in coverage checking (#1086) and case splitting (#3526). Such might make sense to speed up coverage checking.

[nad]

The flag should be included in the following list:

agda/doc/user-manual/tools/command-line-options.rst

Lines 1145 to 1147 in bb3602f

	Agda records the options used when generating an interface file. If
	any of the following options differ when trying to load the interface
	again, the source file is re-typechecked instead:

[andreasabel]

Is everyone happy with the name --performance:absurd-clauses? (UPDATE: This was the original suggestion for the option name.) This implicitly opens a --performance family of options.
Alternative would be --keep-absurd-clauses without dedication to performance.

[jespercockx]

I'd prefer something like --no-infer-absurd-clauses (and also have its counterpart --infer-absurd-clauses)

[andreasabel]

I'd prefer something like --no-infer-absurd-clauses (and also have its counterpart --infer-absurd-clauses)

Fine with me. @nad @plt-amy ?

[nad]

I prefer --no-…noun (like --no-termination-check) to --no-verb… (like --no-save-metas). I can see why we don't use --do-not-save-metas, so I think we should try to come up with an option with a noun.

[plt-amy]

I think I prefer a noun (phrase), too. How about --no-implicit-absurd-clauses?

[jespercockx]

Or --no-absurd-clause-inference

[andreasabel]

I think I prefer a noun (phrase), too. How about --no-implicit-absurd-clauses?

To me, "implicit" is scourged earth. It is way to overloaded, I am trying to avoid it entirely, e.g., only speak either about "hidden" or "instance" arguments (which are both implicit).

Or --no-absurd-clause-inference

Models for --no-infer-absurd-clauses are --no-save-metas, --no-print-pattern-synonyms and --no-import-sorts.
I think I prefer --no-infer-absurd-clauses over --no-absurd-clause-inference since it is more succinct and does not involve the detour of first turning a verb (infer) into a noun (inference).

[nad]

Models for --no-infer-absurd-clauses are --no-save-metas, --no-print-pattern-synonyms and --no-import-sorts.

Do you think that any of these sound good? (I implemented --no-save-metas.)

Perhaps we could replace all noun options with verbs, and use --dont- instead: --check-termination, --dont-check-termination. Another alternative is to have options like --infer-absurd-clauses=yes, --termination-check=no.

[jespercockx]

Perhaps we could replace all noun options with verbs, and use --dont- instead: --check-termination, --dont-check-termination. Another alternative is to have options like --infer-absurd-clauses=yes, --termination-check=no.

I like this, because then we could also have other options for distinguishing between applying an option to the current module and applying it to all modules that depend on it (see #4908)

[andreasabel]

Models for --no-infer-absurd-clauses are --no-save-metas, --no-print-pattern-synonyms and --no-import-sorts.

Do you think that any of these sound good? (I implemented --no-save-metas.)

I think they have meme potential because they sound awkward. All of your bases are belong to us!