Various small documentation and error changes (#566)

* Remove references to LSS in intTests

Fixes #493.

* Remove obsolete note about globals and unsoundness

Fixes #563

* Point users at `enable_{deprecated,experimental}`

Fixes #496.

intTests/test0012_jss_aig/README

@@ -4,10 +4,10 @@ The tests in 'test.saw' only make sense for the SAW backend; the
 default backend encodes the arguments and results in a different
 way.
 
-There used to be a bug in JSS and LSS where multiple AIG writes
-interacted, causing the number of input bits in the AIG to grow with
-each write. So in 'test.sh' we are careful to check that the number of
-input bits is always 16.
+There used to be a bug in JSS where multiple AIG writes interacted,
+causing the number of input bits in the AIG to grow with each write. So
+in 'test.sh' we are careful to check that the number of input bits is
+always 16.
 
 Besides checking predicates, where the input encoding does not matter,
 and the output is a single bit, we also check the input and output

intTests/test0015_sawscript_aig/README

@@ -3,9 +3,8 @@ Test AIG generation in SAWScript.
 These examples provide some documentation of the SAWScript AIG
 encoding.
 
-Note that, compared to LSS and JSS, the arguments here are reversed:
-for functions '\x -> \y -> e' the arguments are packed as 'x # y'
-here, but as 'y # x' for LSS and JSS. However, in LSS and JSS you
-don't actually write the arguments explicitly -- rather, open terms
-are closed over the symbolic variables in scope -- so I'm not sure the
-comparison is fair.
+Note that, compared to JSS, the arguments here are reversed: for
+functions '\x -> \y -> e' the arguments are packed as 'x # y' here, but
+as 'y # x' for JSS. However, in JSS you don't actually write the
+arguments explicitly -- rather, open terms are closed over the symbolic
+variables in scope -- so I'm not sure the comparison is fair.

intTests/test0015_sawscript_aig/test.saw

@@ -9,13 +9,12 @@ write_aig "tmp/yy.aig"    {{ \(x:[8]) -> \(y:[8]) -> y + y }};
 write_aig "tmp/2y.aig"    {{ \(x:[8]) -> \(y:[8]) -> 2 * y }};
 
 // The code below is very similar to '../test0012_jss_aig/test.saw'
-// and '../test0014_lss_aig/test.saw'.
 
 // Many of these Cryptol functions have types more specific than
 // necessary. The point is to document the behavior of SAWScript
 // AIG generation.
 let {{
-  // Arguments are reversed, compared to LSS and JSS.
+  // Arguments are reversed, compared to JSS.
 
   run_pred : ([16] -> [1]) -> [8] -> [8] -> [1]
   run_pred f x y = f (((zero # x) <<< 8) + (zero # y))

src/SAWScript/Interpreter.hs

@@ -2001,9 +2001,7 @@ primitives = Map.fromList
     Current
     [ "Return a SetupValue representing the value of the initializer of a named"
     , "global. The String should be the name of a global value."
-    , "Note that initializing global variables may be unsound in the presence"
-    , "of compositional verification (see GaloisInc/saw-script#203)."
-    ] -- TODO: There should be a section in the manual about global-unsoundness.
+    ]
 
   , prim "crucible_term"
     "Term -> SetupValue"

src/SAWScript/MGU.hs

@@ -473,7 +473,11 @@ inferE (ln, expr) = case expr of
     do env <- TI $ asks typeEnv
        case M.lookup x env of
          Nothing -> do
-           recordError $ "unbound variable: " ++ show x
+           recordError $ unlines
+             [ "Unbound variable: " ++ show x
+             , "Note that some built-in commands are available only after running"
+             , "either `enable_deprecated` or `enable_experimental`."
+             ]
            t <- newType
            return (Var x, t)
          Just (Forall as t) -> do