GaloisInc · sauclovian-g · Nov 3, 2025 · Oct 29, 2025 · Oct 23, 2025 · Oct 23, 2025
diff --git a/CHANGES.md b/CHANGES.md
@@ -204,6 +204,12 @@ This release supports [version
 
 ## Bug Fixes
 
+* Under some combinations of circumstances you would sometimes get
+  messages of the form "Subshells not supported" or "Proof subshells
+  not supported" when trying to start an interactive subshell /
+  sub-REPL.
+  This no longer happens.
+
 * `jvm_verify` and `mir_verify` now honor their respective parameters that
   enable or disable path satisfiability checking. As discovered in #2740, these
   parameters had been ignored.

diff --git a/intTests/test1646/test15.log.good b/intTests/test1646/test15.log.good
@@ -293,7 +293,7 @@ set_memoization_incremental : TopLevel ()
 set_min_sharing : Int -> TopLevel ()
 set_solver_cache_path : String -> TopLevel ()
 set_solver_cache_timeout : Int -> TopLevel ()
-sharpSAT : Term -> TopLevel Integer
+sharpSAT : Term -> TopLevel Int
 show : {a} a -> String
 show_cfg : CFG -> String
 show_term : Term -> String

diff --git a/intTests/test2242_2243/README b/intTests/test2242_2243/README
@@ -1,9 +1,3 @@
-Examples from #2242 (scoping regression in proof_subshell) and #2243
-(bindings escape proof_subshell).
-
-It might be better to use test-and-diff.sh here so as to capture the
-output; however, it doesn't work. For a TopLevel subshell, the input
-for the subshell needs to be on stdin, even if you use .isaw files
-with saw -B, and test-and-diff.sh can't do that. For a ProofScript
-subshell, it's even worse: for some reason one gets "Proof subshells
-not supported".
+Examples from #2242 (scoping regression in proof_subshell), #2243
+(bindings escape proof_subshell), and #2306 (bizarre environment
+capturing in the subshell / proof_subshell commands)
diff --git a/intTests/test_parse_errors/lexer005.log.good b/intTests/test_parse_errors/lexer005.log.good
@@ -1,3 +1,6 @@
  Loading file "lexer005.saw"
- Parse error at lexer005.saw:3:20-3:21: Unexpected `}'
+ Stack trace:
+   (builtin) (at top level)
+Parse error at lexer005.saw:3:20-3:21: Unexpected `}'
+
 FAILED
diff --git a/intTests/test_parse_errors/lexer006.log.good b/intTests/test_parse_errors/lexer006.log.good
@@ -1,3 +1,6 @@
  Loading file "lexer006.saw"
- Parse error at lexer006.saw:3:1-3:2: Unexpected `}'
+ Stack trace:
+   (builtin) (at top level)
+Parse error at lexer006.saw:3:1-3:2: Unexpected `}'
+
 FAILED
diff --git a/intTests/test_parse_errors/parser001.log.good b/intTests/test_parse_errors/parser001.log.good
@@ -1,3 +1,6 @@
  Loading file "parser001.saw"
- Parse error at parser001.saw:2:13-2:23: Unexpected `rebindable'
+ Stack trace:
+   (builtin) (at top level)
+Parse error at parser001.saw:2:13-2:23: Unexpected `rebindable'
+
 FAILED
diff --git a/intTests/test_parse_errors/parser002.log.good b/intTests/test_parse_errors/parser002.log.good
@@ -1,3 +1,6 @@
  Loading file "parser002.saw"
- Parse error at parser002.saw:2:36-2:38: Unexpected `in'
+ Stack trace:
+   (builtin) (at top level)
+Parse error at parser002.saw:2:36-2:38: Unexpected `in'
+
 FAILED
diff --git a/intTests/test_parse_errors/parser003.log.good b/intTests/test_parse_errors/parser003.log.good
@@ -1,3 +1,6 @@
  Loading file "parser003.saw"
- Parse error at parser003.saw:2:36-2:38: Unexpected `in'
+ Stack trace:
+   (builtin) (at top level)
+Parse error at parser003.saw:2:36-2:38: Unexpected `in'
+
 FAILED
diff --git a/intTests/test_parse_errors/parser004.log.good b/intTests/test_parse_errors/parser004.log.good
@@ -1,3 +1,6 @@
  Loading file "parser004.saw"
- Parse error at parser004.saw:2:22-2:24: Unexpected `in'
+ Stack trace:
+   (builtin) (at top level)
+Parse error at parser004.saw:2:22-2:24: Unexpected `in'
+
 FAILED
diff --git a/intTests/test_parse_errors/parser005.log.good b/intTests/test_parse_errors/parser005.log.good
@@ -1,3 +1,6 @@
  Loading file "parser005.saw"
- Parse error at parser005.saw:2:5-2:15: Unexpected `rebindable'
+ Stack trace:
+   (builtin) (at top level)
+Parse error at parser005.saw:2:5-2:15: Unexpected `rebindable'
+
 FAILED
diff --git a/intTests/test_parse_errors/parser006.log.good b/intTests/test_parse_errors/parser006.log.good
@@ -1,3 +1,6 @@
  Loading file "parser006.saw"
- Parse error at parser006.saw:3:5-3:15: Unexpected `rebindable'
+ Stack trace:
+   (builtin) (at top level)
+Parse error at parser006.saw:3:5-3:15: Unexpected `rebindable'
+
 FAILED
diff --git a/intTests/test_search/search00.log.good b/intTests/test_search/search00.log.good
@@ -107,4 +107,4 @@ write_saig' : String -> Term -> Int -> TopLevel ()
 6 more matches tagged experimental; use enable_experimental to see them
  --------------------------------
  -- (TopLevel Int)
-No matches.
+sharpSAT : Term -> TopLevel Int
diff --git a/intTests/test_search/search01.log.good b/intTests/test_search/search01.log.good
@@ -7,6 +7,7 @@ llvm_spec_solvers : LLVMSpec -> [String]
  --------------------------------
  -- (_ Int)
 goal_num : ProofScript Int
+sharpSAT : Term -> TopLevel Int
  --------------------------------
  -- JVMSetup
 jvm_alloc_array : Int -> JavaType -> JVMSetup JVMValue

diff --git a/intTests/test_type_errors/err025.log.good b/intTests/test_type_errors/err025.log.good
@@ -1,3 +1,6 @@
  Loading file "err025.saw"
- err025.saw:3:9-3:14: do block must include at least one expression
+ Stack trace:
+   (builtin) (at top level)
+err025.saw:3:9-3:14: do block must include at least one expression
+
 FAILED
diff --git a/intTests/test_type_errors/err026.log.good b/intTests/test_type_errors/err026.log.good
@@ -1,3 +1,6 @@
  Loading file "err026.saw"
- err026.saw:3:9-5:2: do block must end with expression
+ Stack trace:
+   (builtin) (at top level)
+err026.saw:3:9-5:2: do block must end with expression
+
 FAILED
diff --git a/intTests/test_type_errors/err027.log.good b/intTests/test_type_errors/err027.log.good
@@ -1,3 +1,6 @@
  Loading file "err027.saw"
- Parse error at err027.saw:7:10-7:11: Unexpected `]'
+ Stack trace:
+   (builtin) (at top level)
+Parse error at err027.saw:7:10-7:11: Unexpected `]'
+
 FAILED
diff --git a/saw-central/src/SAWCentral/Utils.hs b/saw-central/src/SAWCentral/Utils.hs
@@ -16,7 +16,6 @@ import Control.Monad.State
 import Control.Monad.Trans.Except
 import Control.DeepSeq(rnf, NFData(..))
 import Data.Char(isSpace)
-import Data.Data
 import Data.Function (on)
 import Data.List (sortBy)
 import qualified Data.List.NonEmpty as NE
@@ -43,8 +42,6 @@ import SAWCentral.Position
 bullets :: Char -> [PP.Doc ann] -> PP.Doc ann
 bullets c = PP.vcat . map (PP.hang 2 . (PP.pretty c PP.<+>))
 
-data SSMode = Verify | Blif | CBlif deriving (Eq, Show, Data, Typeable)
-
 -- | Convert a string to a paragraph formatted document.
 ftext :: String -> Doc ann
 ftext msg = fillSep (map pretty $ words msg)
@@ -64,7 +61,7 @@ mapLookupAny keys m = listToMaybe $ catMaybes $ map (\k -> Map.lookup k m) keys
 data ExecException = ExecException Pos          -- Position
                                    (Doc Void)   -- Error message
                                    String       -- Resolution tip
-  deriving (Show, Typeable)
+  deriving (Show)
 
 instance Exception ExecException
 

diff --git a/saw-central/src/SAWCentral/Value.hs b/saw-central/src/SAWCentral/Value.hs
@@ -48,6 +48,8 @@ module SAWCentral.Value (
     -- used by SAWCentral.Builtins, SAWScript.ValueOps, SAWScript.Interpreter,
     -- SAWScript.REPL.Command, SAWScript.REPL.Monad, SAWServer.SAWServer
     Environ(..),
+    -- used by SAWScript.Import
+    RebindableEnv,
     -- used by SAWScript.Interpreter
     pushScope, popScope,
     -- used by SAWCentral.Builtins, SAWScript.ValueOps, SAWScript.Interpreter,
@@ -73,6 +75,8 @@ module SAWCentral.Value (
     rwSetCryptolEnvStack,
     -- used by SAWScript.REPL.Monad, SAWServer.SAWServer, SAWServer.Yosys
     rwModifyCryptolEnv,
+    -- used by SAWScript.Interpreter, and implicitly by SAWScript.REPL and Main
+    TopLevelShellHook, ProofScriptShellHook,
     -- used by SAWScript.Automatch, SAWScript.REPL.*, SAWScript.Interpreter,
     --    SAWServer.SAWServer
     TopLevelRO(..),
@@ -942,6 +946,17 @@ cryptolPop (CryptolEnvStack _ ces) =
         [] -> panic "cryptolPop" ["Cryptol environment scope stack ran out"]
         ce : ces' -> CryptolEnvStack ce ces'
 
+-- | Type for the function to start a new REPL in TopLevel.
+--
+--   Passed down from the REPL code to avoid circular references.
+type TopLevelShellHook = TopLevelRO -> TopLevelRW -> IO TopLevelRW
+
+-- | Type for the function to start a new REPL in ProofScript.
+--
+--   Passed down from the REPL code to avoid circular references.
+type ProofScriptShellHook =
+    TopLevelRO -> TopLevelRW -> ProofState ->
+    IO (TopLevelRW, ProofState)
 
 -- | TopLevel Read-Only Environment.
 data TopLevelRO =
@@ -952,12 +967,12 @@ data TopLevelRO =
   , roProxy         :: AIGProxy
   , roInitWorkDir   :: FilePath
   , roBasicSS       :: SAWSimpset
-  , roSubshell      :: TopLevel ()
+  , roSubshell      :: TopLevelShellHook
     -- ^ An action for entering a subshell.  This
     --   may raise an error if the current execution
     --   mode doesn't support subshells (e.g., the remote API)
 
-  , roProofSubshell :: ProofScript ()
+  , roProofSubshell :: ProofScriptShellHook
     -- ^ An action for entering a subshell in proof mode.  This
     --   may raise an error if the current execution
     --   mode doesn't support subshells (e.g., the remote API)

diff --git a/saw-core/src/SAWCore/Prim.hs b/saw-core/src/SAWCore/Prim.hs
@@ -13,7 +13,6 @@ module SAWCore.Prim where
 
 import qualified Control.Exception as X
 import Data.Bits
-import Data.Typeable (Typeable)
 import Data.Vector (Vector)
 import qualified Data.Vector as V
 import Numeric.Natural (Natural)
@@ -308,7 +307,7 @@ data EvalError
   | DivideByZero
   | UnsupportedPrimitive String String
   | UserError String
-  deriving (Eq, Typeable)
+  deriving (Eq)
 
 instance X.Exception EvalError
 

diff --git a/saw-core/src/SAWCore/Term/Raw.hs b/saw-core/src/SAWCore/Term/Raw.hs
@@ -22,7 +22,6 @@ import Data.Hashable
 import Data.IntMap (IntMap)
 import qualified Data.IntMap as IntMap
 import Data.IntSet (IntSet)
-import Data.Typeable (Typeable)
 
 import Instances.TH.Lift () -- for instance TH.Lift Text
 
@@ -68,7 +67,7 @@ data Term
        -- ^ The underlying 'TermF' that this 'Term' wraps. This field "ties the
        -- knot" of the 'Term'/'TermF' recursion scheme.
      }
-  deriving (Show, Typeable)
+  deriving (Show)
 
 instance Hashable Term where
   -- The hash of an 'STApp' depends on its not-necessarily-unique

diff --git a/saw-script/src/SAWScript/Import.hs b/saw-script/src/SAWScript/Import.hs