From 007e80aabd893a3fa2b57c17f58f6530b00530bf Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 21 Feb 2025 16:22:12 -0500 Subject: [PATCH 1/9] copilot-theorem: Add Props to specProps. Refs #594. `copilot-theorem`'s Kind2 backend takes a proposition and attempts to prove that it is valid at all possible time steps. Currently, this happens regardless of whether the proposition is universally or existentially quantified. This is unsound, and it can lead to valid, existentially quantified properties being incorrectly labeled as invalid. This commit adds information about propositions' quantifiers to the Kind2 backend's implementation so that it may use the quantifiers when translating the properties to Kind2. This is accomplished by updating `specProps` to map each proposition's identifier to its corresponding `copilot-core` `Prop`. --- copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs | 4 ++-- .../src/Copilot/Theorem/TransSys/PrettyPrint.hs | 3 ++- copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs | 4 +++- copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs | 3 ++- copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs | 8 +++++--- 5 files changed, 14 insertions(+), 8 deletions(-) diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs index d8115e893..123f6ed64 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs @@ -65,7 +65,7 @@ trSpec spec predCallsGraph _assumptions checkedProps = K.File preds props preds = map (trNode spec predCallsGraph) (specNodes spec) props = map trProp $ filter ((`elem` checkedProps) . fst) $ - Map.toList (specProps spec) + Map.toList $ Map.map fst $ specProps spec trProp :: (PropId, ExtVar) -> K.Prop trProp (pId, var) = K.Prop pId (trVar . extVarLocalPart $ var) @@ -98,7 +98,7 @@ addAssumptions spec assumptions (K.File {K.filePreds, K.fileProps}) = vars = let bindings = nodeImportedVars (specTopNode spec) - toExtVar a = fromJust $ Map.lookup a (specProps spec) + toExtVar a = fst $ fromJust $ Map.lookup a $ specProps spec toTopVar (ExtVar nId v) = assert (nId == specTopNodeId spec) v in map (varName . toTopVar . toExtVar) assumptions diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs index 89fdc5787..3debe552c 100644 --- a/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs +++ b/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs @@ -27,7 +27,8 @@ pSpec spec = items $$ props items = foldr (($$) . pNode) empty (specNodes spec) props = text "PROPS" $$ Map.foldrWithKey (\k -> ($$) . pProp k) - empty (specProps spec) + empty + (Map.map fst (specProps spec)) pProp pId extvar = quotes (text pId) <+> text "is" <+> pExtVar extvar diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs index d2a953387..e0a297535 100644 --- a/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs +++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs @@ -24,6 +24,8 @@ module Copilot.Theorem.TransSys.Spec , specDependenciesGraph , specTopNode ) where +import qualified Copilot.Core as C + import Copilot.Theorem.TransSys.Type import Copilot.Theorem.TransSys.Operators import Copilot.Theorem.TransSys.Invariants @@ -55,7 +57,7 @@ type PropId = String data TransSys = TransSys { specNodes :: [Node] , specTopNodeId :: NodeId - , specProps :: Map PropId ExtVar } + , specProps :: Map PropId (ExtVar, C.Prop) } -- | A node is a set of variables living in a local namespace and corresponding -- to the 'Var' type. diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs index 79edd2828..e59058496 100644 --- a/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs +++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs @@ -42,7 +42,8 @@ mergeNodes toMergeIds spec = spec { specNodes = newNode : map (updateOtherNode newNodeId toMergeIds renamingExtF) otherNodes - , specProps = Map.map renamingExtF (specProps spec) } + , specProps = + Map.map (\(ev, prop) -> (renamingExtF ev, prop)) (specProps spec) } where nodes = specNodes spec diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs index 68ddb8806..f15162e49 100644 --- a/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs +++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs @@ -96,10 +96,12 @@ translate cspec = cprops :: [C.Property] cprops = C.specProperties cspec - propBindings :: Map PropId ExtVar + propBindings :: Map PropId (ExtVar, C.Prop) propBindings = Map.fromList $ do - pid <- map C.propertyName cprops - return (pid, mkExtVar topNodeId pid) + cprop <- cprops + let pid = C.propertyName cprop + prop = C.propertyProp cprop + return (pid, (mkExtVar topNodeId pid, prop)) ((modelNodes, propNodes), extvarNodesNames) = runTrans $ liftM2 (,) (mapM stream (C.specStreams cspec)) (mkPropNodes cprops) From a007efad3207b6603e46da408ebbd3d60e61018b Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 24 Feb 2025 05:41:21 -0500 Subject: [PATCH 2/9] copilot-theorem: Translate quantifiers correctly in Kind2 backend. Refs #594. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `copilot-theorem`'s Kind2 backend takes a proposition and attempts to prove that it is valid at all possible time steps. Currently, this happens regardless of whether the proposition is universally or existentially quantified. This is unsound, and it can lead to valid, existentially quantified properties being incorrectly labeled as invalid. This commit fixes the translations of propositions to Kind2 (via Kind2's TransSys backend) such that the translated properties respect quantifier information. Specifically, this replaces an unsound use of the `extractProp` function with an analysis that translates the property differently depending on whether it is universally or existentially quantified. Because all TransSys propositions use universal quantification, we convert an existentially quantified property `∃x.P(x)` as `¬(∀x.¬(P(x)))` during the translation to TransSys. --- .../src/Copilot/Theorem/Kind2/Output.hs | 29 +++++++++++++++---- .../src/Copilot/Theorem/Kind2/Prover.hs | 18 +++++++++--- .../src/Copilot/Theorem/TransSys/Spec.hs | 3 +- .../src/Copilot/Theorem/TransSys/Translate.hs | 10 ++++++- 4 files changed, 49 insertions(+), 11 deletions(-) diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs index 42a2f60dc..f80b8170b 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs @@ -8,19 +8,38 @@ import Text.XML.Light hiding (findChild) import Copilot.Theorem.Prove as P import Data.Maybe (fromJust) +import qualified Copilot.Core as C + import qualified Copilot.Theorem.Misc.Error as Err simpleName s = QName s Nothing Nothing -- | Parse output of Kind2. parseOutput :: String -- ^ Property whose validity is being checked. + -> C.Prop -- ^ The property's quantifier. -> String -- ^ XML output of Kind2 -> P.Output -parseOutput prop xml = fromJust $ do +parseOutput propId propQuantifier xml = fromJust $ do root <- parseXMLDoc xml case findAnswer . findPropTag $ root of - "valid" -> return (Output Valid []) - "falsifiable" -> return (Output Invalid []) + "valid" -> case propQuantifier of + -- We encode a universally quantified property P as + -- ∀x.P(x) in Kind2, so the original property is valid + -- iff the Kind2 property is valid. + C.Forall {} -> return (Output Valid []) + -- We encode an existentially quantified property P as + -- ¬(∀x.¬(P(x))) in Kind2, so the original property is + -- invalid iff the Kind2 property is valid. + C.Exists {} -> return (Output Invalid []) + "falsifiable" -> case propQuantifier of + -- We encode a universally quantified property P as + -- ∀x.P(x) in Kind2, so the original property is invalid + -- iff the Kind2 property is invalid. + C.Forall {} -> return (Output Invalid []) + -- We encode an existentially quantified property P as + -- ¬(∀x.¬(P(x))) in Kind2, so the original property is + -- valid iff the Kind2 property is invalid. + C.Exists {} -> return (Output Valid []) s -> err $ "Unrecognized status : " ++ s where @@ -31,10 +50,10 @@ parseOutput prop xml = fromJust $ do let rightElement elt = qName (elName elt) == "Property" && lookupAttr (simpleName "name") (elAttribs elt) - == Just prop + == Just propId in case filterChildren rightElement root of tag : _ -> tag - _ -> err $ "Tag for property " ++ prop ++ " not found" + _ -> err $ "Tag for property " ++ propId ++ " not found" findAnswer tag = case findChildren (simpleName "Answer") tag of diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs index 3931c615b..66db2c346 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs @@ -19,10 +19,12 @@ import Copilot.Theorem.Misc.Utils (openTempFile) import System.Process -import System.Directory -import Data.Default +import System.Directory +import Data.Default +import qualified Data.Map as Map -import qualified Copilot.Theorem.TransSys as TS +import qualified Copilot.Theorem.Misc.Error as Err +import qualified Copilot.Theorem.TransSys as TS -- | Options for Kind2 data Options = Options @@ -68,4 +70,12 @@ askKind2 (ProverST opts spec) assumptions toCheck = do putStrLn kind2Input removeFile tempName - return $ parseOutput (head toCheck) output + + let propId = head toCheck + propQuantifier = case Map.lookup propId (TS.specProps spec) of + Just (_, quantifier) -> + quantifier + Nothing -> + Err.impossible $ + "askKind2: " ++ propId ++ " not in specProps" + return $ parseOutput propId propQuantifier output diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs index e0a297535..b68181ae0 100644 --- a/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs +++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs @@ -53,7 +53,8 @@ type NodeId = String type PropId = String -- | A modular transition system is defined by a graph of nodes and a series --- of properties, each mapped to a variable. +-- of properties, each mapped to a variable and a 'C.Prop' describing how the +-- property is quantified. data TransSys = TransSys { specNodes :: [Node] , specTopNodeId :: NodeId diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs index f15162e49..2659fa6cb 100644 --- a/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs +++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs @@ -141,7 +141,15 @@ streamOfProp :: C.Property -> C.Stream streamOfProp prop = C.Stream { C.streamId = 42 , C.streamBuffer = [] - , C.streamExpr = C.extractProp (C.propertyProp prop) + -- TransSys encodes all properties using universal quantification. + -- Therefore, in order to encode an existentially quantified + -- property ∃x.P(x), we must first convert it to ¬(∀x.¬(P(x))). + -- The `Exists` case below handles the ∀x.¬(P(x)) part by adding + -- an `Op1 Not` around the property. The outermost negation is + -- handled elsewhere (e.g., in Copilot.Theorem.Kind2.Output.parse). + , C.streamExpr = case C.propertyProp prop of + C.Forall p -> p + C.Exists p -> C.Op1 C.Not p , C.streamExprType = C.Bool } stream :: C.Stream -> Trans Node From 3b51c969d863755431cb628de80bc02e0c243a8d Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 7 Mar 2025 07:08:02 -0500 Subject: [PATCH 3/9] copilot-theorem: Document changes in CHANGELOG. Refs #594. --- copilot-theorem/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index d3c2bd464..8416d3a75 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,3 +1,6 @@ +2025-04-17 + * Translate quantifiers correctly in Kind2 backend. (#594) + 2025-03-07 * Version bump (4.3). (#604) * Fix multiple typos in README. (#560) From 03b7adc2bc7d119f1d6214166208071378f43d41 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 21 Apr 2025 09:44:38 -0700 Subject: [PATCH 4/9] copilot-core: Remove deprecated Copilot.Core.Type.uTypeType. Refs #615. The record field uTypeType, part of Copilot.Core.Type.UType, is never really used within the module or in any other part of Copilot or, as far as we know, by any user of Copilot. The record field was deprecated in Copilot 4.1 and no messages have been received requesting that it be kept in this library. As per our internal policy of waiting 3 versions from deprecation until a public interface declaration can be removed, this definition can now be removed. This commit removes the field uTypeType from the definition of Copilot.Core.Type.UType, making the type no longer a record. --- copilot-core/src/Copilot/Core/Type.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/copilot-core/src/Copilot/Core/Type.hs b/copilot-core/src/Copilot/Core/Type.hs index 8d54c82f3..b290810c2 100644 --- a/copilot-core/src/Copilot/Core/Type.hs +++ b/copilot-core/src/Copilot/Core/Type.hs @@ -289,8 +289,7 @@ instance (Typeable t, Typed t, KnownNat n) => Typed (Array n t) where simpleType (Array t) = SArray t -- | A untyped type (no phantom type). -data UType = forall a . Typeable a => UType { uTypeType :: Type a } -{-# DEPRECATED uTypeType "This field is deprecated in Copilot 4.1. Use pattern matching instead." #-} +data UType = forall a . Typeable a => UType (Type a) instance Eq UType where UType ty1 == UType ty2 = typeRep ty1 == typeRep ty2 From 3e0b13d8a1b4f9317759a11fc4a4c65056cb9033 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 21 Apr 2025 09:46:50 -0700 Subject: [PATCH 5/9] copilot-core: Document changes in CHANGELOG. Refs #615. --- copilot-core/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index 371c8c2d9..9ae7dd071 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,3 +1,6 @@ +2025-04-21 + * Remove deprecated Copilot.Core.Type.uTypeType. (#615) + 2025-03-07 * Version bump (4.3). (#604) * Fix typo in documentation. (#587) From bb3a109c682b642eb40343746c255aaa177fbe20 Mon Sep 17 00:00:00 2001 From: kaBeech Date: Fri, 18 Apr 2025 11:11:42 -0700 Subject: [PATCH 6/9] copilot: Update build status URL. Refs #612. Currently the badge for the build status in the README doesn't show up correctly. GitHub has cached the result but it's not providing the resulting image, so we see "Build Status" instead. This commit updates the badge URL to the current "https://api.travis-ci.com/Copilot-Language/copilot.svg?branch=master", which enables the badge to show properly. --- copilot/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot/README.md b/copilot/README.md index efdc58d28..893d6a933 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -2,7 +2,7 @@ # Copilot -[![Build Status](https://travis-ci.com/Copilot-Language/copilot.svg?branch=master)](https://app.travis-ci.com/github/Copilot-Language/copilot) +[![Build Status](https://api.travis-ci.com/Copilot-Language/copilot.svg?branch=master)](https://app.travis-ci.com/github/Copilot-Language/copilot) [![Version on Hackage](https://img.shields.io/hackage/v/copilot.svg)](https://hackage.haskell.org/package/copilot) Copilot is a runtime verification framework for hard real-time systems. From e54f7c0f43b8785a0f478988adea289d76ca634f Mon Sep 17 00:00:00 2001 From: kaBeech Date: Fri, 18 Apr 2025 11:34:58 -0700 Subject: [PATCH 7/9] copilot: Document changes in CHANGELOG. Refs #612. --- copilot/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index abd146bba..e39981d15 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,3 +1,6 @@ +2025-04-18 + * Update build status badge URL. (#612) + 2025-03-07 * Version bump (4.3). (#604) * Include missing dependencies in installation instructions. (#591) From faa9ba72a582da608be6d5d53a351e228cf44bc6 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 7 May 2025 20:21:58 -0700 Subject: [PATCH 8/9] Bump versions and constraints. Refs #618. --- copilot-c99/copilot-c99.cabal | 4 ++-- copilot-core/copilot-core.cabal | 2 +- copilot-interpreter/copilot-interpreter.cabal | 4 ++-- copilot-language/copilot-language.cabal | 8 ++++---- copilot-libraries/copilot-libraries.cabal | 4 ++-- copilot-prettyprinter/copilot-prettyprinter.cabal | 4 ++-- copilot-theorem/copilot-theorem.cabal | 6 +++--- copilot/copilot.cabal | 14 +++++++------- 8 files changed, 23 insertions(+), 23 deletions(-) diff --git a/copilot-c99/copilot-c99.cabal b/copilot-c99/copilot-c99.cabal index 48fc6aa36..dabf04bf0 100644 --- a/copilot-c99/copilot-c99.cabal +++ b/copilot-c99/copilot-c99.cabal @@ -1,6 +1,6 @@ cabal-version : >= 1.10 name : copilot-c99 -version : 4.3 +version : 4.4 synopsis : A compiler for Copilot targeting C99. description : This package is a back-end from Copilot to C. @@ -45,7 +45,7 @@ library , mtl >= 2.2 && < 2.4 , pretty >= 1.1 && < 1.2 - , copilot-core >= 4.3 && < 4.4 + , copilot-core >= 4.4 && < 4.5 , language-c99 >= 0.2.0 && < 0.3 , language-c99-simple >= 0.3 && < 0.4 diff --git a/copilot-core/copilot-core.cabal b/copilot-core/copilot-core.cabal index 1140f129e..daab8383b 100644 --- a/copilot-core/copilot-core.cabal +++ b/copilot-core/copilot-core.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-core -version: 4.3 +version: 4.4 synopsis: An intermediate representation for Copilot. description: Intermediate representation for Copilot. diff --git a/copilot-interpreter/copilot-interpreter.cabal b/copilot-interpreter/copilot-interpreter.cabal index 835f27106..d5b679829 100644 --- a/copilot-interpreter/copilot-interpreter.cabal +++ b/copilot-interpreter/copilot-interpreter.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-interpreter -version: 4.3 +version: 4.4 synopsis: Interpreter for Copilot. description: Interpreter for Copilot. @@ -44,7 +44,7 @@ library base >= 4.9 && < 5, pretty >= 1.0 && < 1.2, - copilot-core >= 4.3 && < 4.4 + copilot-core >= 4.4 && < 4.5 exposed-modules: diff --git a/copilot-language/copilot-language.cabal b/copilot-language/copilot-language.cabal index 53c981618..87d54101d 100644 --- a/copilot-language/copilot-language.cabal +++ b/copilot-language/copilot-language.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-language -version: 4.3 +version: 4.4 synopsis: A Haskell-embedded DSL for monitoring hard real-time distributed systems. description: @@ -42,9 +42,9 @@ library , data-reify >= 0.6 && < 0.7 , mtl >= 2.0 && < 3 - , copilot-core >= 4.3 && < 4.4 - , copilot-interpreter >= 4.3 && < 4.4 - , copilot-theorem >= 4.3 && < 4.4 + , copilot-core >= 4.4 && < 4.5 + , copilot-interpreter >= 4.4 && < 4.5 + , copilot-theorem >= 4.4 && < 4.5 exposed-modules: Copilot.Language , Copilot.Language.Operators.BitWise diff --git a/copilot-libraries/copilot-libraries.cabal b/copilot-libraries/copilot-libraries.cabal index 737a590e7..078d009fd 100644 --- a/copilot-libraries/copilot-libraries.cabal +++ b/copilot-libraries/copilot-libraries.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-libraries -version: 4.3 +version: 4.4 synopsis: Libraries for the Copilot language. description: Libraries for the Copilot language. @@ -41,7 +41,7 @@ library , containers >= 0.4 && < 0.8 , mtl >= 2.0 && < 2.4 , parsec >= 2.0 && < 3.2 - , copilot-language >= 4.3 && < 4.4 + , copilot-language >= 4.4 && < 4.5 exposed-modules: Copilot.Library.Libraries diff --git a/copilot-prettyprinter/copilot-prettyprinter.cabal b/copilot-prettyprinter/copilot-prettyprinter.cabal index 46e8de208..2a4a9578f 100644 --- a/copilot-prettyprinter/copilot-prettyprinter.cabal +++ b/copilot-prettyprinter/copilot-prettyprinter.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-prettyprinter -version: 4.3 +version: 4.4 synopsis: A prettyprinter of Copilot Specifications. description: A prettyprinter of Copilot specifications. @@ -45,7 +45,7 @@ library base >= 4.9 && < 5, pretty >= 1.0 && < 1.2, - copilot-core >= 4.3 && < 4.4 + copilot-core >= 4.4 && < 4.5 exposed-modules: diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal index c6994913f..ad7ab8699 100644 --- a/copilot-theorem/copilot-theorem.cabal +++ b/copilot-theorem/copilot-theorem.cabal @@ -14,7 +14,7 @@ description: . -version : 4.3 +version : 4.4 license : BSD3 license-file : LICENSE maintainer : Ivan Perez @@ -63,8 +63,8 @@ library , xml >= 1.3 && < 1.4 , what4 >= 1.3 && < 1.7 - , copilot-core >= 4.3 && < 4.4 - , copilot-prettyprinter >= 4.3 && < 4.4 + , copilot-core >= 4.4 && < 4.5 + , copilot-prettyprinter >= 4.4 && < 4.5 exposed-modules : Copilot.Theorem , Copilot.Theorem.Prove diff --git a/copilot/copilot.cabal b/copilot/copilot.cabal index a39788ab8..6401ef883 100644 --- a/copilot/copilot.cabal +++ b/copilot/copilot.cabal @@ -1,5 +1,5 @@ name: copilot -version: 4.3 +version: 4.4 cabal-version: >= 1.10 license: BSD3 license-file: LICENSE @@ -52,12 +52,12 @@ library , directory >= 1.3 && < 1.4 , filepath >= 1.4 && < 1.6 - , copilot-core >= 4.3 && < 4.4 - , copilot-theorem >= 4.3 && < 4.4 - , copilot-language >= 4.3 && < 4.4 - , copilot-libraries >= 4.3 && < 4.4 - , copilot-c99 >= 4.3 && < 4.4 - , copilot-prettyprinter >= 4.3 && < 4.4 + , copilot-core >= 4.4 && < 4.5 + , copilot-theorem >= 4.4 && < 4.5 + , copilot-language >= 4.4 && < 4.5 + , copilot-libraries >= 4.4 && < 4.5 + , copilot-c99 >= 4.4 && < 4.5 + , copilot-prettyprinter >= 4.4 && < 4.5 exposed-modules: Language.Copilot, Language.Copilot.Main From 2ff7d9f9e4a5f69c04e88d5b67995e5b28da3cdc Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 7 May 2025 20:23:06 -0700 Subject: [PATCH 9/9] Document changes in CHANGELOG. Refs #618. --- copilot-c99/CHANGELOG | 3 +++ copilot-core/CHANGELOG | 3 ++- copilot-interpreter/CHANGELOG | 3 +++ copilot-language/CHANGELOG | 3 +++ copilot-libraries/CHANGELOG | 3 +++ copilot-prettyprinter/CHANGELOG | 3 +++ copilot-theorem/CHANGELOG | 3 ++- copilot/CHANGELOG | 3 ++- 8 files changed, 21 insertions(+), 3 deletions(-) diff --git a/copilot-c99/CHANGELOG b/copilot-c99/CHANGELOG index 48f275cf7..00f705df8 100644 --- a/copilot-c99/CHANGELOG +++ b/copilot-c99/CHANGELOG @@ -1,3 +1,6 @@ +2025-05-07 + * Version bump (4.4). (#618) + 2025-03-07 * Version bump (4.3). (#604) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index 9ae7dd071..4a0902c21 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,4 +1,5 @@ -2025-04-21 +2025-05-07 + * Version bump (4.4). (#618) * Remove deprecated Copilot.Core.Type.uTypeType. (#615) 2025-03-07 diff --git a/copilot-interpreter/CHANGELOG b/copilot-interpreter/CHANGELOG index 924fa7436..c5f4894c8 100644 --- a/copilot-interpreter/CHANGELOG +++ b/copilot-interpreter/CHANGELOG @@ -1,3 +1,6 @@ +2025-05-07 + * Version bump (4.4). (#618) + 2025-03-07 * Version bump (4.3). (#604) diff --git a/copilot-language/CHANGELOG b/copilot-language/CHANGELOG index 2f729caac..fc28f01f1 100644 --- a/copilot-language/CHANGELOG +++ b/copilot-language/CHANGELOG @@ -1,3 +1,6 @@ +2025-05-07 + * Version bump (4.4). (#618) + 2025-03-07 * Version bump (4.3). (#604) * Fix typo in documentation. (#587) diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG index 228e37a5d..a0c598f54 100644 --- a/copilot-libraries/CHANGELOG +++ b/copilot-libraries/CHANGELOG @@ -1,3 +1,6 @@ +2025-05-07 + * Version bump (4.4). (#618) + 2025-03-07 * Version bump (4.3). (#604) * Remove deprecated function Copilot.Library.Utils.(!!). (#599) diff --git a/copilot-prettyprinter/CHANGELOG b/copilot-prettyprinter/CHANGELOG index caec436ef..360d2e9a0 100644 --- a/copilot-prettyprinter/CHANGELOG +++ b/copilot-prettyprinter/CHANGELOG @@ -1,3 +1,6 @@ +2025-05-07 + * Version bump (4.4). (#618) + 2025-03-07 * Version bump (4.3). (#604) * Update pretty-printing to handle Props. (#254) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index 8416d3a75..f221aec44 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,4 +1,5 @@ -2025-04-17 +2025-05-07 + * Version bump (4.4). (#618) * Translate quantifiers correctly in Kind2 backend. (#594) 2025-03-07 diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index e39981d15..b38dd2c3d 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,4 +1,5 @@ -2025-04-18 +2025-05-07 + * Version bump (4.4). (#618) * Update build status badge URL. (#612) 2025-03-07