Bump cryptol submodule, update withSolver calls.

Update simple-smt version and enable `-threaded` runtime. This tracks the changes from GaloisInc/cryptol#1225 The threaded runtime is necessary to keep `waitForProcess` from stalling all threads in simple-smt.
GaloisInc · Jul 23, 2021 · 58d3648 · 58d3648
1 parent a3b0e53
commit 58d3648
Show file tree

Hide file tree

Showing 9 changed files with 12 additions and 12 deletions.
diff --git a/cabal.GHC-8.10.3.config b/cabal.GHC-8.10.3.config
@@ -267,7 +267,7 @@ constraints: any.Cabal ==3.2.1.0,
              any.simple-get-opt ==0.4,
              any.simple-sendfile ==0.2.30,
              simple-sendfile +allow-bsd,
-             any.simple-smt ==0.9.5,
+             any.simple-smt ==0.9.7,
              any.smallcheck ==1.2.1,
              any.split ==0.2.3.4,
              any.splitmix ==0.1.0.3,

diff --git a/cabal.GHC-8.10.4.config b/cabal.GHC-8.10.4.config
@@ -277,7 +277,7 @@ constraints: any.Cabal ==3.2.1.0,
              any.simple-get-opt ==0.4,
              any.simple-sendfile ==0.2.30,
              simple-sendfile +allow-bsd,
-             any.simple-smt ==0.9.5,
+             any.simple-smt ==0.9.7,
              any.smallcheck ==1.2.1,
              any.split ==0.2.3.4,
              any.splitmix ==0.1.0.3,

diff --git a/cabal.GHC-8.8.4.config b/cabal.GHC-8.8.4.config
@@ -269,7 +269,7 @@ constraints: any.Cabal ==3.0.1.0,
              any.simple-get-opt ==0.4,
              any.simple-sendfile ==0.2.30,
              simple-sendfile +allow-bsd,
-             any.simple-smt ==0.9.5,
+             any.simple-smt ==0.9.7,
              any.smallcheck ==1.2.1,
              any.split ==0.2.3.4,
              any.splitmix ==0.1.0.3,

diff --git a/cryptol-saw-core/css/Main.hs b/cryptol-saw-core/css/Main.hs
@@ -95,7 +95,7 @@ cssMain css [inputModule,name] | cssMode css == NormalMode = do
     modEnv <- CM.initialModuleEnv
     let minp = CM.ModuleInput True (pure defaultEvalOpts) BS.readFile modEnv
     (e,warn) <-
-      SMT.withSolver (meSolverConfig modEnv) $ \s ->
+      SMT.withSolver (return ()) (meSolverConfig modEnv) $ \s ->
       CM.loadModuleByPath inputModule (minp s)
     mapM_ (print . pp) warn
     case e of
@@ -136,7 +136,7 @@ extractCryptol sc modEnv input = do
       Right x -> return x
   let minp = CM.ModuleInput True (pure defaultEvalOpts) BS.readFile modEnv
   (exprResult, exprWarnings) <-
-    SMT.withSolver (meSolverConfig modEnv) $ \s ->
+    SMT.withSolver (return ()) (meSolverConfig modEnv) $ \s ->
     CM.checkExpr pexpr (minp s)
   mapM_ (print . pp) exprWarnings
   ((_, expr, schema), _modEnv') <-

diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
@@ -493,7 +493,7 @@ resolveIdentifier env nm =
   nameEnv = getNamingEnv env
 
   doResolve pnm =
-    SMT.withSolver (meSolverConfig modEnv) $ \s ->
+    SMT.withSolver (return ()) (meSolverConfig modEnv) $ \s ->
     do let minp = MM.ModuleInput True (pure defaultEvalOpts) ?fileReader modEnv
        (res, _ws) <- MM.runModuleM (minp s) $
           MM.interactive (MB.rename interactiveName nameEnv (MR.renameVar MR.NameUse pnm))
@@ -653,7 +653,7 @@ liftModuleM ::
   ME.ModuleEnv -> MM.ModuleM a -> IO (a, ME.ModuleEnv)
 liftModuleM env m =
   do let minp = MM.ModuleInput True (pure defaultEvalOpts) ?fileReader env
-     SMT.withSolver (meSolverConfig env) $ \s ->
+     SMT.withSolver (return ()) (meSolverConfig env) $ \s ->
        MM.runModuleM (minp s) m >>= moduleCmdResult
 
 defaultEvalOpts :: E.EvalOpts

diff --git a/deps/cryptol b/deps/cryptol
diff --git a/saw-script.cabal b/saw-script.cabal
@@ -216,13 +216,13 @@ executable saw
     , cryptol-saw-core
     , aig
 
-  GHC-options: -O2 -Wall -Werror -fno-ignore-asserts -fno-spec-constr-count
+  GHC-options: -O2 -Wall -Werror -threaded -fno-ignore-asserts -fno-spec-constr-count
 
 test-suite integration_tests
   type: exitcode-stdio-1.0
   hs-source-dirs: intTests
 
-  ghc-options: -Wall
+  ghc-options: -Wall -threaded
   default-language: Haskell2010
 
   main-is: IntegrationTest.hs

diff --git a/src/SAWScript/AutoMatch/Cryptol.hs b/src/SAWScript/AutoMatch/Cryptol.hs
@@ -36,7 +36,7 @@ getDeclsCryptol path = do
    modEnv <- M.initialModuleEnv
    let minp = M.ModuleInput True (pure evalOpts) BS.readFile modEnv
    (result, warnings) <-
-     SMT.withSolver (meSolverConfig modEnv) $ \s ->
+     SMT.withSolver (return ()) (meSolverConfig modEnv) $ \s ->
      M.loadModuleByPath path (minp s)
    return $ do
       forM_ warnings $ liftF . flip Warning () . pretty

diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
@@ -1311,7 +1311,7 @@ defaultTypedTerm :: Options -> SharedContext -> C.SolverConfig -> TypedTerm -> I
 defaultTypedTerm opts sc cfg tt@(TypedTerm (TypedTermSchema schema) trm)
   | null (C.sVars schema) = return tt
   | otherwise = do
-  mdefault <- C.withSolver cfg (\s -> C.defaultReplExpr s undefined schema)
+  mdefault <- C.withSolver (return ()) cfg (\s -> C.defaultReplExpr s undefined schema)
   let inst = do (soln, _) <- mdefault
                 mapM (`lookup` soln) (C.sVars schema)
   case inst of
+15 −3		.github/ci.sh
+34 −17		.github/workflows/ci.yml
+6 −0		CHANGES.md
+1 −1		cabal.GHC-8.10.2.config
+1 −1		cabal.GHC-8.10.3.config
+1 −1		cabal.GHC-8.6.5.config
+1 −1		cabal.GHC-8.8.4.config
+5 −0		cryptol-remote-api/python/CHANGELOG.md
+0 −8		cryptol-remote-api/python/cryptol/connection.py
+1 −1		cryptol-remote-api/python/pyproject.toml
+4 −1		cryptol-remote-api/src/CryptolServer.hs
+2 −1		cryptol.cabal
+33 −6		docs/CryptolPrims.md
+ −		docs/CryptolPrims.pdf
+ −		docs/ProgrammingCryptol.pdf
+152 −105		docs/ProgrammingCryptol/appendices/Syntax.tex
+57 −43		docs/RefMan/RefMan.rst
+ −		docs/Semantics.pdf
+31 −15		docs/Syntax.md
+ −		docs/Syntax.pdf
+8 −8		lib/Cryptol.cry
+5 −3		src/Cryptol/Eval.hs
+60 −16		src/Cryptol/Eval/Reference.lhs
+6 −1		src/Cryptol/ModuleSystem/Renamer.hs
+21 −4		src/Cryptol/REPL/Monad.hs
+6 −5		src/Cryptol/TypeCheck/Solver/SMT.hs
+25 −2		src/Cryptol/TypeCheck/TypeOf.hs
+8 −0		tests/issues/issue1240.cry
+1 −0		tests/issues/issue1240.icry
+3 −0		tests/issues/issue1240.icry.stdout