Document the deprecation process.

Also add some glaringly missing text about REPL actions (e.g. :q) and
then about enable_experimental and enable_deprecated as context.

Part of #2184.

doc/manual/manual.md

@@ -499,6 +499,64 @@ command and prints out the time it took to execute.
 original result of the timed command and the time taken to execute it
 (in milliseconds), without printing anything in the process.
 
+## REPL Actions
+
+There is an additional class of things that one may type at the REPL
+for interactive use:
+
+* `:cd` changes the REPL's current directory.
+
+* `:pwd` prints the REPL's current directory.
+
+* `:env` displays the values and types of all currently bound
+variables, including built-in functions and commands.
+
+* `:tenv` displays the expansions of all currently defined type
+aliases, including those that are built in.
+
+* `:type` or `:t` checks and prints the type of an arbitrary SAWScript
+expression:
+~~~~
+sawscript> :t show
+{a.0} a.0 -> String
+~~~~
+
+* `:help` or `:h` prints the help text for a built-in function or
+command:
+~~~~
+sawscript> :h show
+Description
+-----------
+
+    show : {a} a -> String
+
+Convert the value of the given expression to a string.
+~~~~
+
+* `:quit` or `:q` exits the program.
+
+## Further built-in functions and commands
+
+SAW contains many built-in operations, referred to as "primitives."
+These appear in SAWScript as built-in functions and commands.
+The following sections of the manual will introduce many of these.
+
+## Experimental and deprecated functions and commands
+
+Some of the primitives available in SAW at any given time are
+experimental.
+These may be incomplete, unfinished, use at your own risk, etc.
+The functions and commands associated with these are unavailable
+by default; they can be made visible with the `enable_experimental`
+command.
+
+Other primitives are considered deprecated.
+Some of these, as the
+[deprecation process]("formal-deprecation-process") proceeds, are
+unavailable by default.
+
+They can be made visible with the `enable_deprecated` command.
+
 # The Term Type
 
 Perhaps the most important type in SAWScript, and the one most unlike
@@ -4994,3 +5052,42 @@ For now, the `prove_bisim` command has a couple limitations:
   function `g_lhs` calls `f_lhs`, and `prove_bisim` is invoked with a
   `BisimTheorem` proving that `f_lhs` is bisimilar to `f_rhs`, then `g_lhs` may
   call `f_lhs` at most once.
+
+# Formal Deprecation Process
+
+SAW primitives, and thus their associated SAWScript built-ins, sometimes
+become obsolete or are found inadequate and replaced.
+The process by which that happens has three steps, as follows:
+
+1. The decision is made to deprecate and eventually remove the objects
+in question.
+This can happen at the level of individual built-in elements (for example,
+when replacing a function with an awkward interface or unfortunate name) or
+at the level of internal units of functionality with possibly multiple
+built-ins affected.
+At this step the built-ins in question are marked for a deprecation warning.
+They remain available by default, but referring to them will trigger a
+warning.
+
+1. The objects in question are made invisible by default.
+Now, referring to the affected built-ins will fail unless the
+`enable_deprecated` command is used.
+In that case referring to them will still produce a warning.
+
+1. The objects in question are removed entirely and are no longer
+available.
+
+In general any object or group of objects will move only one step per
+release; that is, something first marked deprecated (so it warns) in
+saw-script 1.2 will not disappear by default before saw-script 1.3 and
+not be removed entirely before saw-script 1.4.
+The time frame may be longer depending on the needs of downstream
+users, the complexity of migration, and the cost/impact of keeping the
+deprecated code in the system.
+
+We may move faster if circumstances dictate, but hope not to need to.
+
+Objects that have never appeared in a release, or that have never
+moved past experimental may be removed without first being deprecated.
+However, we aim to avoid this in cases where the objects in question
+have gotten substantial use despite their formal status.