Restructure deprecation semantics

[sauclovian-g]

Currently, when a primitive is marked deprecated, it disappears unless you enable_deprecated. This is not really the right way to do things: when something is marked deprecated it should generate a warning for a while, and only then disappear by default, over the span of releases.

That way the downstream user has a period of time to update their stuff before being forced to as part of updating.

That is, the proper removal process goes something like this:

1. Mark the primitive so uses of it trigger a warning.
2. Mark the primitive so it disappears by default, but can be brought back.
3. Remove the primitive entirely.

where nothing moves more than one step per release, and sometimes less, e.g. for something that had been widely used.

We have apparently been skipping stage 1 in the past.

A simple change would be to drop stage 2 instead; keep the current internal structure but make enable_deprecated the default, perhaps adding a disable_deprecated (although realistically nobody would ever use it). I don't think this is a good idea because I don't think we want the things that are currently in stage 2 to come back to life by default, but I also doubt we're ready to move them to stage 3 (that is, remove them)... although we could be, there are only a few and one refers to Cryptol v1.

I think we want instead to add another internal state for stage 1 and use it for new deprecations. This is easy enough. The hard part is figuring out what to call things -- not the internal state, WarnDeprecated will serve for that, but what user-facing terminology to use.

(Also I think using a visible deprecated item should produce a warning whether or not enable_deprecated is in effect, and I think we should include specific target versions in the warnings for when the item will disappear behind enable_deprecated and when it will be removed entirely. This also requires assessing the current set of deprecated primitives and figuring out a concrete removal plan for them, but we should clearly do that.)

Also the deprecation policy should be spelled out in the manual. Currently the word "deprecate" appears only in three places in the documentation, two of which are copies of the message SAW prints when you refer to an unbound variable. The other is a code snippet that appears to contain references to things that have been removed. I'll file a new issue about that.

[RyanGlScott]

I am on board with your suggestion of implementing stage 1.

Unrelated, but the milestone for this is 2024T3, which seems optimistic given the current date :)

[sauclovian-g]

Yeah, well, that milestone is still pending and this is a blocker for #2183, which is in that milestone... it's all approximate anyway :-)