copilot-verifier 4.4 → 4.5
raw patch · 3 files changed
+37/−25 lines, 3 filesdep ~copilotdep ~copilot-c99dep ~copilot-coresetup-changednew-uploaderPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: copilot, copilot-c99, copilot-core, copilot-language, copilot-libraries, copilot-prettyprinter, copilot-theorem
API changes (from Hackage documentation)
Files
- CHANGELOG +27/−17
- Setup.hs +2/−0
- copilot-verifier.cabal +8/−8
CHANGELOG view
@@ -1,40 +1,50 @@+2025-07-07+ * Version bump (4.5). (#642)+ * Include `copilot-verifier` in mainline `copilot` repo. (#622)+ 2025-05-08- * Version bump (4.4). (#85)+ * Version bump (4.4). (copilot-verifier#85) 2025-03-10- * Version bump (4.3). (#82)- * Add `smtSolver` option to `VerifierOptions`. (#78)- * Add `smtFloatMode` option to `VerifierOptions`. (#79)+ * Version bump (4.3). (copilot-verifier#82)+ * Add `smtSolver` option to `VerifierOptions`. (copilot-verifier#78)+ * Add `smtFloatMode` option to `VerifierOptions`. (copilot-verifier#79) 2025-01-20- * Version bump (4.2). (#76)- * Reject specs that use multiple triggers with the same name. (#74)+ * Version bump (4.2). (copilot-verifier#76)+ * Reject specs that use multiple triggers with the same name.+ (copilot-verifier#74) 2024-11-08- * Version bump (4.1). (#72)+ * Version bump (4.1). (copilot-verifier#72) 2024-09-09- * Version bump (4.0). (#69)- * Support verifying programs that use array updates. (#63)- * Support verifying programs that use struct updates. (#57)+ * Version bump (4.0). (copilot-verifier#69)+ * Support verifying programs that use array updates.+ (copilot-verifier#63)+ * Support verifying programs that use struct updates.+ (copilot-verifier#57) 2024-08-03- * Support building with `crucible-llvm-0.7` and `crux-llvm-0.9`. (#64)- * Support GHC 9.4 through 9.8. (#65)+ * Support building with `crucible-llvm-0.7` and `crux-llvm-0.9`.+ (copilot-verifier#64)+ * Support GHC 9.4 through 9.8. (copilot-verifier#65) 2024-07-30 * When using `Noisy` verbosity, always log proof goals related to the- core correspondence proof, even if the goals are trivial. (#51)+ core correspondence proof, even if the goals are trivial.+ (copilot-verifier#51) * When using `Noisy` verbosity, log more information about which proof- goals arise before or after calling the `step()` function. (#52)+ goals arise before or after calling the `step()` function.+ (copilot-verifier#52) 2024-07-11- * Version bump (3.20). (#58)+ * Version bump (3.20). (copilot-verifier#58) 2024-03-08- * Version bump (3.19). (#53)+ * Version bump (3.19). (copilot-verifier#53) * Provide more detailed feedback upon a successful run of the verifier.- * Make the examples build with Copilot 3.19. (#53)+ * Make the examples build with Copilot 3.19. (copilot-verifier#53) 2024-02-06 * Initial release of `copilot-verifier`.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
copilot-verifier.cabal view
@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name: copilot-verifier-Version: 4.4+Version: 4.5 Author: Galois Inc. Maintainer: rscott@galois.com Copyright: (c) Galois, Inc 2021-2024@@ -45,9 +45,9 @@ bv-sized >= 1.0.0 && < 1.1, bytestring, containers >= 0.5.9.0,- copilot-c99 >= 4.4 && < 4.5,- copilot-core >= 4.4 && < 4.5,- copilot-theorem >= 4.4 && < 4.5,+ copilot-c99 >= 4.5 && < 4.6,+ copilot-core >= 4.5 && < 4.6,+ copilot-theorem >= 4.5 && < 4.6, crucible >= 0.7.1 && < 0.8, crucible-llvm >= 0.7 && < 0.8, crux >= 0.7.1 && < 0.8,@@ -80,10 +80,10 @@ hs-source-dirs: examples build-depends: case-insensitive,- copilot >= 4.4 && < 4.5,- copilot-language >= 4.4 && < 4.5,- copilot-libraries >= 4.4 && < 4.5,- copilot-prettyprinter >= 4.4 && < 4.5,+ copilot >= 4.5 && < 4.6,+ copilot-language >= 4.5 && < 4.6,+ copilot-libraries >= 4.5 && < 4.6,+ copilot-prettyprinter >= 4.5 && < 4.6, copilot-verifier exposed-modules: Copilot.Verifier.Examples