From c120306476357b867eaca98fe2d99f6d91b47dc6 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sun, 19 Mar 2023 20:43:03 -0400 Subject: [PATCH 1/4] Bump submodules in preparation for supporting CVC5 The main payload of this commit is to bump the `what4` submodule to bring in the changes from GaloisInc/what4#204. This also brings in a variety of other submodule changes to accommodate this: * GaloisIns/crucible#1068, which ensures that everything can build against `tasty-sugar >= 2.0` (the version of the library that `what4-1.4` depends on). * GaloisInc/cryptol#1504, which adapts Cryptol to CVC5. This adjusts the lower and upper version bounds on SBV in Cryptol, so I do the same here in `saw-core.sbv.cabal` and `saw-script.cabal`. * GaloisInc/language-sally#12, which performs a similar `what4` adaptation. * GaloisInc/macaw#328, which performs a similar `what4` adaptation. --- deps/crucible | 2 +- deps/cryptol | 2 +- deps/language-sally | 2 +- deps/macaw | 2 +- deps/what4 | 2 +- saw-core-sbv/saw-core-sbv.cabal | 2 +- saw-script.cabal | 2 +- 7 files changed, 7 insertions(+), 7 deletions(-) diff --git a/deps/crucible b/deps/crucible index 4b8e481f98..f4145fbed9 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 4b8e481f986e2ba2125032edf05dda407dbb57b8 +Subproject commit f4145fbed96245f385a91ef3a32e6737df1075ff diff --git a/deps/cryptol b/deps/cryptol index 4b89554988..9382d52754 160000 --- a/deps/cryptol +++ b/deps/cryptol @@ -1 +1 @@ -Subproject commit 4b89554988e1f755b6d8f49e6be08027aadbaacf +Subproject commit 9382d527543db70068b71fe3a327cd07fe0b36c8 diff --git a/deps/language-sally b/deps/language-sally index a217a9f661..24d53a963c 160000 --- a/deps/language-sally +++ b/deps/language-sally @@ -1 +1 @@ -Subproject commit a217a9f661caabd7858a17c2b556217fc39a946e +Subproject commit 24d53a963c2a2d11a118cfaa98956a69f5c8c6d5 diff --git a/deps/macaw b/deps/macaw index 88d024990b..0686e5d86b 160000 --- a/deps/macaw +++ b/deps/macaw @@ -1 +1 @@ -Subproject commit 88d024990b97292f4d3d0fe0bf9c08e75c12c3ce +Subproject commit 0686e5d86bfd802e04dd94cf8836127127232f8f diff --git a/deps/what4 b/deps/what4 index 6f5e0fe9be..6c462cd46e 160000 --- a/deps/what4 +++ b/deps/what4 @@ -1 +1 @@ -Subproject commit 6f5e0fe9bef58234603ccf6914c32ea1ba2f9766 +Subproject commit 6c462cd46e0ea9ebbfbd6b6ea237984eeb3dc72a diff --git a/saw-core-sbv/saw-core-sbv.cabal b/saw-core-sbv/saw-core-sbv.cabal index 1cc5448ab4..386a740dde 100644 --- a/saw-core-sbv/saw-core-sbv.cabal +++ b/saw-core-sbv/saw-core-sbv.cabal @@ -20,7 +20,7 @@ library lens, mtl, saw-core, - sbv >= 8.10 && < 9.1, + sbv >= 9.1 && < 9.3, text, transformers, vector diff --git a/saw-script.cabal b/saw-script.cabal index c3e726c100..cff9ea9dc1 100644 --- a/saw-script.cabal +++ b/saw-script.cabal @@ -80,7 +80,7 @@ library , saw-core-coq , saw-core-sbv , saw-core-what4 - , sbv >= 8.10 && < 9.1 + , sbv >= 9.1 && < 9.3 , split , temporary , template-haskell From 5167b2959094212785069d2658b7fd7fe03fef2f Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sun, 19 Mar 2023 22:21:07 -0400 Subject: [PATCH 2/4] Add support for CVC5 This adds basic support for the CVC5 SMT solver by adding `cvc5` and related proof scripts. I hae added a `test_cvc5` integration test to kick the tires. This addresses one part of #1706. --- .github/ci.sh | 3 +- CHANGES.md | 5 +++ doc/manual/manual.md | 8 +++- doc/tutorial/tutorial.md | 2 +- intTests/test_cvc5/test.saw | 9 +++++ intTests/test_cvc5/test.sh | 3 ++ .../python/saw_client/proofscript.py | 11 ++++++ saw-remote-api/src/SAWServer/ProofScript.hs | 7 ++++ src/SAWScript/Builtins.hs | 16 ++++++++ src/SAWScript/Interpreter.hs | 38 +++++++++++++++++++ src/SAWScript/Prover/SBV.hs | 2 +- src/SAWScript/Prover/What4.hs | 8 +++- 12 files changed, 106 insertions(+), 6 deletions(-) create mode 100644 intTests/test_cvc5/test.saw create mode 100755 intTests/test_cvc5/test.sh diff --git a/.github/ci.sh b/.github/ci.sh index fb6acf2018..6d86bb867d 100755 --- a/.github/ci.sh +++ b/.github/ci.sh @@ -80,7 +80,7 @@ install_system_deps() { cp $BIN/yices_smt2$EXT $BIN/yices-smt2$EXT export PATH="$BIN:$PATH" echo "$BIN" >> "$GITHUB_PATH" - is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" yices + is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" cvc5 && is_exe "$BIN" yices } build_cryptol() { @@ -127,6 +127,7 @@ zip_dist_with_solvers() { # dependencies) as the SAW binaries. cp "$BIN/abc" dist/bin/ cp "$BIN/cvc4" dist/bin/ + cp "$BIN/cvc5" dist/bin/ cp "$BIN/yices" dist/bin/ cp "$BIN/yices-smt2" dist/bin/ # Z3 4.8.14 has been known to nondeterministically time out with the AWSLC diff --git a/CHANGES.md b/CHANGES.md index 686d137c21..9717a5fa5a 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -90,6 +90,11 @@ allows verification certain kinds of simple loops by using a user-provided loop invariant. +* Add a `cvc5` family of proof scripts that use the CVC5 SMT solver. + (Note that the `sbv_cvc5` and `sbv_unint_cvc5` are non-functional + on Windows at this time due to a downstream issue with CVC5 1.0.4 and + earlier.) + # Version 0.9 ## New Features diff --git a/doc/manual/manual.md b/doc/manual/manual.md index 967b438949..beb6047c2c 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -1131,7 +1131,7 @@ sawscript> sat_print abc {{ \(x:[8]) -> x+x == x*2 }} Sat: [x = 0] ~~~~ -In addition to these, the `boolector`, `cvc4`, `mathsat`, and `yices` +In addition to these, the `boolector`, `cvc4`, `cvc5`, `mathsat`, and `yices` provers are available. The internal decision procedure `rme`, short for Reed-Muller Expansion, is an automated prover that works particularly well on the Galois field operations that show up, for example, in AES. @@ -1199,6 +1199,8 @@ named subterms should be represented as uninterpreted functions. * `unint_cvc4 : [String] -> ProofScript ()` +* `unint_cvc5 : [String] -> ProofScript ()` + * `unint_yices : [String] -> ProofScript ()` * `unint_z3 : [String] -> ProofScript ()` @@ -1218,6 +1220,8 @@ library to represent and solve SMT queries: * `sbv_unint_cvc4 : [String] -> ProofScript ()` +* `sbv_unint_cvc5 : [String] -> ProofScript ()` + * `sbv_unint_yices : [String] -> ProofScript ()` * `sbv_unint_z3 : [String] -> ProofScript ()` @@ -1226,6 +1230,8 @@ The `w4_`-prefixed tactics make use of the What4 library instead of SBV: * `w4_unint_cvc4 : [String] -> ProofScript ()` +* `w4_unint_cvc5 : [String] -> ProofScript ()` + * `w4_unint_yices : [String] -> ProofScript ()` * `w4_unint_z3 : [String] -> ProofScript ()` diff --git a/doc/tutorial/tutorial.md b/doc/tutorial/tutorial.md index 9580829897..62412f7ee2 100644 --- a/doc/tutorial/tutorial.md +++ b/doc/tutorial/tutorial.md @@ -296,7 +296,7 @@ passes the given term through unchanged, because it might be used for either satisfiability or validity checking. The SMT-Lib export capabilities in SAWScript make use of the Haskell -SBV package, and support ABC, Boolector, CVC4, MathSAT, Yices, and Z3. +SBV package, and support ABC, Boolector, CVC4, CVC5, MathSAT, Yices, and Z3. \newpage diff --git a/intTests/test_cvc5/test.saw b/intTests/test_cvc5/test.saw new file mode 100644 index 0000000000..58d54ea3fa --- /dev/null +++ b/intTests/test_cvc5/test.saw @@ -0,0 +1,9 @@ +let +{{ +add_mul_lemma : Integer -> Integer -> Integer -> Integer -> Bit +add_mul_lemma m n p q = + (0 <= m /\ 0 <= n /\ 0 <= p /\ 0 <= q /\ n < q /\ p < m) ==> + (m * n + p < m * q) +}}; + +prove (w4_unint_cvc5 []) {{ add_mul_lemma }}; diff --git a/intTests/test_cvc5/test.sh b/intTests/test_cvc5/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_cvc5/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/saw-remote-api/python/saw_client/proofscript.py b/saw-remote-api/python/saw_client/proofscript.py index 960e31bdbb..853cee7d32 100644 --- a/saw-remote-api/python/saw_client/proofscript.py +++ b/saw-remote-api/python/saw_client/proofscript.py @@ -45,6 +45,10 @@ class CVC4(UnintProver): def __init__(self, unints : List[str]) -> None: super().__init__("w4-cvc4", unints) +class CVC5(UnintProver): + def __init__(self, unints : List[str]) -> None: + super().__init__("w4-cvc5", unints) + class Yices(UnintProver): def __init__(self, unints : List[str]) -> None: super().__init__("w4-yices", unints) @@ -57,6 +61,10 @@ class CVC4_SBV(UnintProver): def __init__(self, unints : List[str]) -> None: super().__init__("sbv-cvc4", unints) +class CVC5_SBV(UnintProver): + def __init__(self, unints : List[str]) -> None: + super().__init__("sbv-cvc5", unints) + class Yices_SBV(UnintProver): def __init__(self, unints : List[str]) -> None: super().__init__("sbv-yices", unints) @@ -121,6 +129,9 @@ def to_json(self) -> Any: def cvc4(unints : List[str]) -> ProofTactic: return UseProver(CVC4(unints)) +def cvc5(unints : List[str]) -> ProofTactic: + return UseProver(CVC5(unints)) + def yices(unints : List[str]) -> ProofTactic: return UseProver(Yices(unints)) diff --git a/saw-remote-api/src/SAWServer/ProofScript.hs b/saw-remote-api/src/SAWServer/ProofScript.hs index dd570ec031..be68202fb9 100644 --- a/saw-remote-api/src/SAWServer/ProofScript.hs +++ b/saw-remote-api/src/SAWServer/ProofScript.hs @@ -57,6 +57,7 @@ data Prover | SBV_ABC_SMTLib | SBV_Boolector [String] | SBV_CVC4 [String] + | SBV_CVC5 [String] | SBV_MathSAT [String] | SBV_Yices [String] | SBV_Z3 [String] @@ -64,6 +65,7 @@ data Prover | W4_ABC_Verilog | W4_Boolector [String] | W4_CVC4 [String] + | W4_CVC5 [String] | W4_Yices [String] | W4_Z3 [String] @@ -87,11 +89,13 @@ instance FromJSON Prover where "abc" -> pure W4_ABC_SMTLib "boolector" -> SBV_Boolector <$> unints "cvc4" -> SBV_CVC4 <$> unints + "cvc5" -> SBV_CVC5 <$> unints "mathsat" -> SBV_MathSAT <$> unints "rme" -> pure RME "sbv-abc" -> pure SBV_ABC_SMTLib "sbv-boolector" -> SBV_Boolector <$> unints "sbv-cvc4" -> SBV_CVC4 <$> unints + "sbv-cvc5" -> SBV_CVC5 <$> unints "sbv-mathsat" -> SBV_MathSAT <$> unints "sbv-yices" -> SBV_Yices <$> unints "sbv-z3" -> SBV_Z3 <$> unints @@ -99,6 +103,7 @@ instance FromJSON Prover where "w4-abc-verilog" -> pure W4_ABC_Verilog "w4-boolector" -> W4_Boolector <$> unints "w4-cvc4" -> W4_CVC4 <$> unints + "w4-cvc5" -> W4_CVC5 <$> unints "w4-yices" -> W4_Yices <$> unints "w4-z3" -> W4_Z3 <$> unints "yices" -> SBV_Yices <$> unints @@ -273,6 +278,7 @@ interpretProofScript (ProofScript ts) = go ts SBV_ABC_SMTLib -> return $ SB.proveABC_SBV SBV_Boolector unints -> return $ SB.proveUnintBoolector unints SBV_CVC4 unints -> return $ SB.proveUnintCVC4 unints + SBV_CVC5 unints -> return $ SB.proveUnintCVC5 unints SBV_MathSAT unints -> return $ SB.proveUnintMathSAT unints SBV_Yices unints -> return $ SB.proveUnintYices unints SBV_Z3 unints -> return $ SB.proveUnintZ3 unints @@ -280,6 +286,7 @@ interpretProofScript (ProofScript ts) = go ts W4_ABC_Verilog -> return $ SB.w4_abc_verilog W4_Boolector unints -> return $ SB.w4_unint_boolector unints W4_CVC4 unints -> return $ SB.w4_unint_cvc4 unints + W4_CVC5 unints -> return $ SB.w4_unint_cvc5 unints W4_Yices unints -> return $ SB.w4_unint_yices unints W4_Z3 unints -> return $ SB.w4_unint_z3 unints go [Trivial] = return $ SB.trivial diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 224debfd04..005214fcae 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -1005,6 +1005,9 @@ proveZ3 = proveSBV SBV.z3 proveCVC4 :: ProofScript () proveCVC4 = proveSBV SBV.cvc4 +proveCVC5 :: ProofScript () +proveCVC5 = proveSBV SBV.cvc5 + proveMathSAT :: ProofScript () proveMathSAT = proveSBV SBV.mathSAT @@ -1020,6 +1023,9 @@ proveUnintZ3 = proveUnintSBV SBV.z3 proveUnintCVC4 :: [String] -> ProofScript () proveUnintCVC4 = proveUnintSBV SBV.cvc4 +proveUnintCVC5 :: [String] -> ProofScript () +proveUnintCVC5 = proveUnintSBV SBV.cvc5 + proveUnintMathSAT :: [String] -> ProofScript () proveUnintMathSAT = proveUnintSBV SBV.mathSAT @@ -1040,6 +1046,9 @@ w4_z3 = wrapW4Prover Prover.proveWhat4_z3 [] w4_cvc4 :: ProofScript () w4_cvc4 = wrapW4Prover Prover.proveWhat4_cvc4 [] +w4_cvc5 :: ProofScript () +w4_cvc5 = wrapW4Prover Prover.proveWhat4_cvc5 [] + w4_yices :: ProofScript () w4_yices = wrapW4Prover Prover.proveWhat4_yices [] @@ -1055,6 +1064,9 @@ w4_unint_z3_using tactic = wrapW4Prover (Prover.proveWhat4_z3_using tactic) w4_unint_cvc4 :: [String] -> ProofScript () w4_unint_cvc4 = wrapW4Prover Prover.proveWhat4_cvc4 +w4_unint_cvc5 :: [String] -> ProofScript () +w4_unint_cvc5 = wrapW4Prover Prover.proveWhat4_cvc5 + w4_unint_yices :: [String] -> ProofScript () w4_unint_yices = wrapW4Prover Prover.proveWhat4_yices @@ -1066,6 +1078,10 @@ offline_w4_unint_cvc4 :: [String] -> String -> ProofScript () offline_w4_unint_cvc4 unints path = wrapW4ProveExporter Prover.proveExportWhat4_cvc4 unints path ".smt2" +offline_w4_unint_cvc5 :: [String] -> String -> ProofScript () +offline_w4_unint_cvc5 unints path = + wrapW4ProveExporter Prover.proveExportWhat4_cvc5 unints path ".smt2" + offline_w4_unint_yices :: [String] -> String -> ProofScript () offline_w4_unint_yices unints path = wrapW4ProveExporter Prover.proveExportWhat4_yices unints path ".smt2" diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 9304a0da5c..d13357be39 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -1918,6 +1918,11 @@ primitives = Map.fromList Current [ "Use the CVC4 theorem prover to prove the current goal." ] + , prim "cvc5" "ProofScript ()" + (pureVal proveCVC5) + Current + [ "Use the CVC5 theorem prover to prove the current goal." ] + , prim "z3" "ProofScript ()" (pureVal proveZ3) Current @@ -1947,6 +1952,13 @@ primitives = Map.fromList , "given list of names as uninterpreted." ] + , prim "unint_cvc5" "[String] -> ProofScript ()" + (pureVal proveUnintCVC5) + Current + [ "Use the CVC5 theorem prover to prove the current goal. Leave the" + , "given list of names as uninterpreted." + ] + , prim "unint_yices" "[String] -> ProofScript ()" (pureVal proveUnintYices) Current @@ -1964,6 +1976,11 @@ primitives = Map.fromList Current [ "Use the CVC4 theorem prover to prove the current goal." ] + , prim "sbv_cvc5" "ProofScript ()" + (pureVal proveCVC5) + Current + [ "Use the CVC5 theorem prover to prove the current goal." ] + , prim "sbv_z3" "ProofScript ()" (pureVal proveZ3) Current @@ -1993,6 +2010,13 @@ primitives = Map.fromList , "given list of names as uninterpreted." ] + , prim "sbv_unint_cvc5" "[String] -> ProofScript ()" + (pureVal proveUnintCVC5) + Current + [ "Use the CVC5 theorem prover to prove the current goal. Leave the" + , "given list of names as uninterpreted." + ] + , prim "sbv_unint_yices" "[String] -> ProofScript ()" (pureVal proveUnintYices) Current @@ -2116,6 +2140,13 @@ primitives = Map.fromList , "given list of names as uninterpreted." ] + , prim "w4_unint_cvc5" "[String] -> ProofScript ()" + (pureVal w4_unint_cvc5) + Current + [ "Prove the current goal using What4 (CVC5 backend). Leave the" + , "given list of names as uninterpreted." + ] + , prim "w4_abc_aiger" "ProofScript ()" (pureVal w4_abc_aiger) Current @@ -2161,6 +2192,13 @@ primitives = Map.fromList ," SMT-Lib2 format. Leave the given list of names as uninterpreted." ] + , prim "offline_w4_unint_cvc5" "[String] -> String -> ProofScript ()" + (pureVal offline_w4_unint_cvc5) + Current + [ "Write the current goal to the given file using What4 (CVC5 backend) in" + ," SMT-Lib2 format. Leave the given list of names as uninterpreted." + ] + , prim "split_goal" "ProofScript ()" (pureVal split_goal) Experimental diff --git a/src/SAWScript/Prover/SBV.hs b/src/SAWScript/Prover/SBV.hs index c401330348..3e4d6114ba 100644 --- a/src/SAWScript/Prover/SBV.hs +++ b/src/SAWScript/Prover/SBV.hs @@ -2,7 +2,7 @@ module SAWScript.Prover.SBV ( proveUnintSBV , proveUnintSBVIO , SBV.SMTConfig - , SBV.z3, SBV.cvc4, SBV.yices, SBV.mathSAT, SBV.boolector + , SBV.z3, SBV.cvc4, SBV.cvc5, SBV.yices, SBV.mathSAT, SBV.boolector , prepNegatedSBV ) where diff --git a/src/SAWScript/Prover/What4.hs b/src/SAWScript/Prover/What4.hs index 2ee794f40a..73c4e11047 100644 --- a/src/SAWScript/Prover/What4.hs +++ b/src/SAWScript/Prover/What4.hs @@ -111,7 +111,8 @@ proveExportWhat4_sym solver un hashConsing outFilePath t = -- Assume unsat return (Nothing, stats) -proveWhat4_z3, proveWhat4_boolector, proveWhat4_cvc4, +proveWhat4_z3, proveWhat4_boolector, + proveWhat4_cvc4, proveWhat4_cvc5, proveWhat4_dreal, proveWhat4_stp, proveWhat4_yices, proveWhat4_abc :: Set VarIndex {- ^ Uninterpreted functions -} -> @@ -122,6 +123,7 @@ proveWhat4_z3, proveWhat4_boolector, proveWhat4_cvc4, proveWhat4_z3 = proveWhat4_sym z3Adapter proveWhat4_boolector = proveWhat4_sym boolectorAdapter proveWhat4_cvc4 = proveWhat4_sym cvc4Adapter +proveWhat4_cvc5 = proveWhat4_sym cvc5Adapter proveWhat4_dreal = proveWhat4_sym drealAdapter proveWhat4_stp = proveWhat4_sym stpAdapter proveWhat4_yices = proveWhat4_sym yicesAdapter @@ -141,7 +143,8 @@ proveWhat4_z3_using tactic un hashConsing t = _ <- setOpt z3TacticSetting $ Text.pack tactic return () -proveExportWhat4_z3, proveExportWhat4_boolector, proveExportWhat4_cvc4, +proveExportWhat4_z3, proveExportWhat4_boolector, + proveExportWhat4_cvc4, proveExportWhat4_cvc5, proveExportWhat4_dreal, proveExportWhat4_stp, proveExportWhat4_yices :: Set VarIndex {- ^ Uninterpreted functions -} -> Bool {- ^ Hash-consing of ExportWhat4 terms -}-> @@ -152,6 +155,7 @@ proveExportWhat4_z3, proveExportWhat4_boolector, proveExportWhat4_cvc4, proveExportWhat4_z3 = proveExportWhat4_sym z3Adapter proveExportWhat4_boolector = proveExportWhat4_sym boolectorAdapter proveExportWhat4_cvc4 = proveExportWhat4_sym cvc4Adapter +proveExportWhat4_cvc5 = proveExportWhat4_sym cvc5Adapter proveExportWhat4_dreal = proveExportWhat4_sym drealAdapter proveExportWhat4_stp = proveExportWhat4_sym stpAdapter proveExportWhat4_yices = proveExportWhat4_sym yicesAdapter From 4d3412958a001ee41637040363037af40eac6c95 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 22 Mar 2023 10:32:22 -0400 Subject: [PATCH 3/4] Regenerate cabal.GHC-*.config files --- cabal.GHC-8.10.7.config | 8 +++++--- cabal.GHC-8.8.4.config | 8 +++++--- cabal.GHC-9.2.7.config | 8 +++++--- 3 files changed, 15 insertions(+), 9 deletions(-) diff --git a/cabal.GHC-8.10.7.config b/cabal.GHC-8.10.7.config index 606ffdc455..84f07b3765 100644 --- a/cabal.GHC-8.10.7.config +++ b/cabal.GHC-8.10.7.config @@ -1,5 +1,6 @@ active-repositories: hackage.haskell.org:merge -constraints: any.Cabal ==3.2.1.0, +constraints: any.BoundedChan ==1.0.3.0, + any.Cabal ==3.2.1.0, any.Glob ==0.10.2, any.GraphSCC ==1.0.4, GraphSCC -use-maps, @@ -248,6 +249,7 @@ constraints: any.Cabal ==3.2.1.0, optparse-applicative +process, any.optparse-simple ==0.1.1.4, optparse-simple -build-example, + any.ordered-containers ==0.2.3, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, parameterized-utils +unsafe-operations, @@ -284,7 +286,7 @@ constraints: any.Cabal ==3.2.1.0, s-cargot -build-example, any.safe ==0.3.19, any.safe-exceptions ==0.1.7.3, - any.sbv ==9.0, + any.sbv ==9.2, any.scientific ==0.3.7.0, scientific -bytestring-builder -integer-simple, any.scotty ==0.12.1, @@ -329,7 +331,7 @@ constraints: any.Cabal ==3.2.1.0, any.tasty-hunit ==0.10.0.3, any.tasty-quickcheck ==0.10.2, any.tasty-smallcheck ==0.8.2, - any.tasty-sugar ==1.3.0.2, + any.tasty-sugar ==2.0.1.0, any.template-haskell ==2.16.0.0, any.temporary ==1.3, any.terminal-size ==0.3.3, diff --git a/cabal.GHC-8.8.4.config b/cabal.GHC-8.8.4.config index 316e457bfd..e2415ba6fc 100644 --- a/cabal.GHC-8.8.4.config +++ b/cabal.GHC-8.8.4.config @@ -1,5 +1,6 @@ active-repositories: hackage.haskell.org:merge -constraints: any.Cabal ==3.0.1.0, +constraints: any.BoundedChan ==1.0.3.0, + any.Cabal ==3.0.1.0, any.Glob ==0.10.2, any.GraphSCC ==1.0.4, GraphSCC -use-maps, @@ -249,6 +250,7 @@ constraints: any.Cabal ==3.0.1.0, optparse-applicative +process, any.optparse-simple ==0.1.1.4, optparse-simple -build-example, + any.ordered-containers ==0.2.3, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, parameterized-utils +unsafe-operations, @@ -285,7 +287,7 @@ constraints: any.Cabal ==3.0.1.0, s-cargot -build-example, any.safe ==0.3.19, any.safe-exceptions ==0.1.7.3, - any.sbv ==9.0, + any.sbv ==9.2, any.scientific ==0.3.7.0, scientific -bytestring-builder -integer-simple, any.scotty ==0.12.1, @@ -330,7 +332,7 @@ constraints: any.Cabal ==3.0.1.0, any.tasty-hunit ==0.10.0.3, any.tasty-quickcheck ==0.10.2, any.tasty-smallcheck ==0.8.2, - any.tasty-sugar ==1.3.0.2, + any.tasty-sugar ==2.0.1.0, any.template-haskell ==2.15.0.0, any.temporary ==1.3, any.terminal-size ==0.3.3, diff --git a/cabal.GHC-9.2.7.config b/cabal.GHC-9.2.7.config index 738ac74284..461fe2cb89 100644 --- a/cabal.GHC-9.2.7.config +++ b/cabal.GHC-9.2.7.config @@ -1,5 +1,6 @@ active-repositories: hackage.haskell.org:merge -constraints: any.Cabal ==3.6.3.0, +constraints: any.BoundedChan ==1.0.3.0, + any.Cabal ==3.6.3.0, any.Glob ==0.10.2, any.GraphSCC ==1.0.4, GraphSCC -use-maps, @@ -249,6 +250,7 @@ constraints: any.Cabal ==3.6.3.0, optparse-applicative +process, any.optparse-simple ==0.1.1.4, optparse-simple -build-example, + any.ordered-containers ==0.2.3, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, parameterized-utils +unsafe-operations, @@ -285,7 +287,7 @@ constraints: any.Cabal ==3.6.3.0, s-cargot -build-example, any.safe ==0.3.19, any.safe-exceptions ==0.1.7.3, - any.sbv ==9.0, + any.sbv ==9.2, any.scientific ==0.3.7.0, scientific -bytestring-builder -integer-simple, any.scotty ==0.12.1, @@ -330,7 +332,7 @@ constraints: any.Cabal ==3.6.3.0, any.tasty-hunit ==0.10.0.3, any.tasty-quickcheck ==0.10.2, any.tasty-smallcheck ==0.8.2, - any.tasty-sugar ==1.3.0.2, + any.tasty-sugar ==2.0.1.0, any.template-haskell ==2.18.0.0, any.temporary ==1.3, any.terminal-size ==0.3.3, From b508d121b7e72792b076780cc0a6406456e11e1e Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 23 Mar 2023 17:08:20 -0400 Subject: [PATCH 4/4] CI: Remove action-docker-layer-caching step Sadly, this action is timing out very frequently. I am going to remove it for the sake of getting CI to work. Fixes #1834. --- .github/workflows/ci.yml | 6 ------ 1 file changed, 6 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5b8dd32c2d..8ad4f84484 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -573,9 +573,6 @@ jobs: docker-compose pull grep -h '^FROM' docker/*.dockerfile | sort -u | awk '{print $2}' | xargs -n1 -P8 docker pull - - uses: jpribyl/action-docker-layer-caching@v0.1.1 - continue-on-error: true - - shell: bash name: "make s2n" working-directory: s2nTests @@ -606,9 +603,6 @@ jobs: name: "${{ runner.os }}-bins" path: ./exercises/bin - - uses: jpribyl/action-docker-layer-caching@v0.1.1 - continue-on-error: true - - shell: bash name: "make exercises container" working-directory: exercises