copilot-theorem 4.1 → 4.2

raw patch · 3 files changed

+11/−6 lines, 3 filesdep ~containersdep ~copilot-coredep ~copilot-prettyprinterPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: containers, copilot-core, copilot-prettyprinter, data-default

API changes (from Hackage documentation)

- Copilot.Theorem.Kind2.Prover: instance Data.Default.Class.Default Copilot.Theorem.Kind2.Prover.Options

- Copilot.Theorem.Prover.SMT: instance Data.Default.Class.Default Copilot.Theorem.Prover.SMT.Options

+ Copilot.Theorem.Kind2.Prover: instance Data.Default.Internal.Default Copilot.Theorem.Kind2.Prover.Options

+ Copilot.Theorem.Prover.SMT: instance Data.Default.Internal.Default Copilot.Theorem.Prover.SMT.Options

Files

CHANGELOG +5/−0
copilot-theorem.cabal +5/−5
src/Copilot/Theorem/What4.hs +1/−1

CHANGELOG view

@@ -1,3 +1,8 @@+2025-01-07+        * Version bump (4.2). (#577)+        * Remove uses of Copilot.Core.Expr.UExpr.uExprType,uExprExpr. (#565)+        * Bump upper constraint on containers, data-default. (#570)+ 2024-11-07         * Version bump (4.1). (#561)         * Standardize changelog format. (#550)

copilot-theorem.cabal view

@@ -14,7 +14,7 @@   <https://copilot-language.github.io>.  -version                   : 4.1+version                   : 4.2 license                   : BSD3 license-file              : LICENSE maintainer                : Ivan Perez <ivan.perezdominguez@nasa.gov>@@ -48,8 +48,8 @@   build-depends           : base                  >= 4.9 && < 5                           , bimap                 (>= 0.3 && < 0.4) || (>= 0.5 && < 0.6)                           , bv-sized              >= 1.0.2 && < 1.1-                          , containers            >= 0.4 && < 0.7-                          , data-default          >= 0.7 && < 0.8+                          , containers            >= 0.4 && < 0.8+                          , data-default          >= 0.7 && < 0.9                           , directory             >= 1.3 && < 1.4                           , libBF                 >= 0.6.2 && < 0.7                           , mtl                   >= 2.0 && < 2.4@@ -63,8 +63,8 @@                           , xml                   >= 1.3 && < 1.4                           , what4                 >= 1.3 && < 1.7 -                          , copilot-core          >= 4.1 && < 4.2-                          , copilot-prettyprinter >= 4.1 && < 4.2+                          , copilot-core          >= 4.2 && < 4.3+                          , copilot-prettyprinter >= 4.2 && < 4.3    exposed-modules         : Copilot.Theorem                           , Copilot.Theorem.Prove

src/Copilot/Theorem/What4.hs view

@@ -324,7 +324,7 @@          args' <- mapM computeArg args          return (nm, guard', args')   where-   computeArg (CE.UExpr { CE.uExprType = tp, CE.uExprExpr = ex }) = do+   computeArg (CE.UExpr tp ex) = do      v <- translateExpr sym mempty ex (RelativeOffset 0)      return (Some tp, v)