packages feed

what4 1.6.2 → 1.6.3

raw patch · 4 files changed

+17/−4 lines, 4 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

- What4.Partial: partialPred :: forall p_a38NA v_a38NB p_a39ai. Lens (Partial p_a38NA v_a38NB) (Partial p_a39ai v_a38NB) p_a38NA p_a39ai
+ What4.Partial: partialPred :: forall p_a38AB v_a38AC p_a38Xj. Lens (Partial p_a38AB v_a38AC) (Partial p_a38Xj v_a38AC) p_a38AB p_a38Xj
- What4.Partial: partialValue :: forall p_a38NA v_a38NB v_a39aj. Lens (Partial p_a38NA v_a38NB) (Partial p_a38NA v_a39aj) v_a38NB v_a39aj
+ What4.Partial: partialValue :: forall p_a38AB v_a38AC v_a38Xk. Lens (Partial p_a38AB v_a38AC) (Partial p_a38AB v_a38Xk) v_a38AC v_a38Xk

Files

CHANGES.md view
@@ -1,3 +1,10 @@+# 1.6.3 (Feb 2025)++* Fixed a bug where `What4.Protocol.SMTLib2.shutdownSolver` would raise+  an exception if the solver process had already terminated. This can occur+  when a solver fails to gracefully time out and the process is killed via+  `What4.Protocol.killSolver`.+ # 1.6.2 (Sep 2024)  * Allow building with GHC 9.10.
src/What4/Protocol/SMTLib2.hs view
@@ -1647,8 +1647,11 @@ shutdownSolver   :: SMTLib2GenericSolver a => a -> SolverProcess t (Writer a) -> IO (Exit.ExitCode, Lazy.Text) shutdownSolver _solver p = do-  -- Tell solver to exit-  writeExit (solverConn p)+  -- Tell solver to exit, if the process is still running+  status <- Streams.getProcessExitCode (solverHandle p)+  case status of+    Just _ -> return ()+    Nothing -> writeExit (solverConn p)   txt <- readAllLines (solverStderr p)   stopHandleReader (solverStderr p)   ec <- solverCleanupCallback p
test/OnlineSolverTest.hs view
@@ -422,7 +422,10 @@                 -- quickly (~0.25s).  This doesn't allow timeout                 -- testing, and the speed suggests an improper                 -- result as well.-                (SolverName "CVC4", SolverVersion v) | "1.7" `elem` words v->+                (SolverName "CVC4", SolverVersion v) | "1.7" `elem` words v ->+                  ignoreTestBecause "solver completes too quickly"+                -- TODO(#278): Maybe the same problem as above?+                (SolverName "CVC4", SolverVersion v) | "1.8" `elem` words v ->                   ignoreTestBecause "solver completes too quickly"                 _ -> id         in maybeSkipTest $ testGroup (snamestr $ testSolverName sti)
what4.cabal view
@@ -1,6 +1,6 @@ Cabal-version: 2.4 Name:          what4-Version:       1.6.2+Version:       1.6.3 Author:        Galois Inc. Maintainer:    rscott@galois.com, kquick@galois.com Copyright:     (c) Galois, Inc 2014-2023