From ed06e9754abfe88eb827f03921d8caf342ec3ff6 Mon Sep 17 00:00:00 2001 From: Chris Hathhorn Date: Tue, 14 Oct 2025 13:30:30 -0500 Subject: [PATCH 01/29] copilot-c99: Raise error when compiling empty array or struct. Refs #695. Copilot allows defining empty arrays (i.e., values of type Array 0) and empty structs (i.e., structs with no fields), but using empty arrays or structs in C99 is undefined behavior. Moreover, copilot-c99 will often crash if you attempt to compile a Copilot specification that uses an empty array or struct. This commit raises an appropriate error when attempting to translate a zero-length array or a struct with no fields to C99. Previously, Copilot would either crash with a confusing error or silently translate the offending spec to invalid C99. --- copilot-c99/src/Copilot/Compile/C99/Error.hs | 19 ++++++++++++++++++- copilot-c99/src/Copilot/Compile/C99/Expr.hs | 17 +++++++++++++---- copilot-c99/src/Copilot/Compile/C99/Type.hs | 10 +++++++--- 3 files changed, 38 insertions(+), 8 deletions(-) diff --git a/copilot-c99/src/Copilot/Compile/C99/Error.hs b/copilot-c99/src/Copilot/Compile/C99/Error.hs index f42c794de..8ab2de608 100644 --- a/copilot-c99/src/Copilot/Compile/C99/Error.hs +++ b/copilot-c99/src/Copilot/Compile/C99/Error.hs @@ -5,7 +5,10 @@ -- -- Custom functions to report error messages to users. module Copilot.Compile.C99.Error - ( impossible ) + ( impossible + , errorEmptyStruct + , errorZeroLengthArray + ) where -- | Report an error due to a bug in Copilot. @@ -18,3 +21,17 @@ impossible function package = ++ ". Please file an issue at " ++ "https://github.com/Copilot-Language/copilot/issues" ++ " or email the maintainers at " + +-- | Report an error when attempting to compile a zero-length array to C99. +-- C99 does not support zero-length arrays, so Copilot cannot compile +-- specifications that use them. +errorZeroLengthArray :: a +errorZeroLengthArray = + error "copilot-c99: Cannot compile zero-length arrays to C99.\n" + +-- | Report an error when attempting to compile an empty struct to C99. +-- C99 does not support empty structs, so Copilot cannot compile +-- specifications that use them. +errorEmptyStruct :: a +errorEmptyStruct = + error "copilot-c99: Cannot compile empty structs to C99.\n" diff --git a/copilot-c99/src/Copilot/Compile/C99/Expr.hs b/copilot-c99/src/Copilot/Compile/C99/Expr.hs index 14e129be9..fec731fbf 100644 --- a/copilot-c99/src/Copilot/Compile/C99/Expr.hs +++ b/copilot-c99/src/Copilot/Compile/C99/Expr.hs @@ -18,7 +18,7 @@ import Copilot.Core ( Array, Expr (..), Field (..), Op1 (..), Op2 (..), arrayElems, toValues, typeLength, typeSize ) -- Internal imports -import Copilot.Compile.C99.Error ( impossible ) +import Copilot.Compile.C99.Error ( impossible, errorEmptyStruct, errorZeroLengthArray ) import Copilot.Compile.C99.Name ( exCpyName, streamAccessorName ) import Copilot.Compile.C99.Type ( transLocalVarDeclType, transType, transTypeName ) @@ -371,14 +371,23 @@ constFieldInit (Value ty (Field val)) = C.InitItem Nothing $ constInit ty val -- | Transform a Copilot Struct, based on the struct fields, into a list of C99 -- initializer values. +-- +-- Raises an error if the struct is empty, as C99 does not support structs with +-- no fields. constStruct :: [Value a] -> NonEmpty.NonEmpty C.InitItem -constStruct val = NonEmpty.fromList $ map constFieldInit val +constStruct val = case val of + [] -> errorEmptyStruct + _ -> NonEmpty.fromList $ map constFieldInit val -- | Transform a Copilot Array, based on the element values and their type, -- into a list of C99 initializer values. +-- +-- Raises an error if the array is empty, as C99 does not support zero-length +-- arrays. constArray :: Type a -> [a] -> NonEmpty.NonEmpty C.InitItem -constArray ty = - NonEmpty.fromList . map (C.InitItem Nothing . constInit ty) +constArray ty xs = case xs of + [] -> errorZeroLengthArray + _ -> NonEmpty.fromList $ map (C.InitItem Nothing . constInit ty) xs -- | Explicitly cast a C99 value to a type. explicitTy :: Type a -> C.Expr -> C.Expr diff --git a/copilot-c99/src/Copilot/Compile/C99/Type.hs b/copilot-c99/src/Copilot/Compile/C99/Type.hs index 78777617b..525fccea9 100644 --- a/copilot-c99/src/Copilot/Compile/C99/Type.hs +++ b/copilot-c99/src/Copilot/Compile/C99/Type.hs @@ -12,7 +12,9 @@ module Copilot.Compile.C99.Type import qualified Language.C99.Simple as C -- Internal imports: Copilot -import Copilot.Core ( Type (..), typeLength, typeName ) +import Copilot.Core ( Struct (..), Type (..), typeLength, + typeName ) +import Copilot.Compile.C99.Error ( errorEmptyStruct, errorZeroLengthArray ) -- | Translate a Copilot type to a C99 type. transType :: Type a -> C.Type @@ -28,10 +30,12 @@ transType ty = case ty of Word64 -> C.TypeSpec $ C.TypedefName "uint64_t" Float -> C.TypeSpec C.Float Double -> C.TypeSpec C.Double - Array ty' -> C.Array (transType ty') len + Array ty' | typeLength ty == 0 -> errorZeroLengthArray + | otherwise -> C.Array (transType ty') len where len = Just $ C.LitInt $ fromIntegral $ typeLength ty - Struct s -> C.TypeSpec $ C.Struct (typeName s) + Struct s | null (toValues s) -> errorEmptyStruct + | otherwise -> C.TypeSpec $ C.Struct (typeName s) -- | Translate a Copilot type to a valid (local) variable declaration C99 type. -- From dc96eacc8caaa07e298d695dbfe8c5b3f3acce01 Mon Sep 17 00:00:00 2001 From: Chris Hathhorn Date: Mon, 16 Feb 2026 22:21:14 -0600 Subject: [PATCH 02/29] copilot-c99: Test for error when compiling empty array or struct. Refs #695. Copilot allows defining empty arrays (i.e., values of type Array 0) and empty structs (i.e., structs with no fields), but using empty arrays or structs in C99 is undefined behavior. Moreover, copilot-c99 will often crash if you attempt to compile a Copilot specification that uses an empty array or struct. A prior commit introduced a solution for this problem that makes the C99 backend detect these undesired struct or array types. This commit adds a test to check that attempting to compile specs containing zero-length arrays or empty structs to C99 raises an appropriate error. --- copilot-c99/tests/Test/Copilot/Compile/C99.hs | 69 ++++++++++++++++++- 1 file changed, 66 insertions(+), 3 deletions(-) diff --git a/copilot-c99/tests/Test/Copilot/Compile/C99.hs b/copilot-c99/tests/Test/Copilot/Compile/C99.hs index 60276e870..b02fc23ae 100644 --- a/copilot-c99/tests/Test/Copilot/Compile/C99.hs +++ b/copilot-c99/tests/Test/Copilot/Compile/C99.hs @@ -8,10 +8,11 @@ module Test.Copilot.Compile.C99 -- External imports import Control.Arrow ((&&&)) -import Control.Exception (IOException, catch) -import Control.Monad (when) +import Control.Exception (ErrorCall (..), IOException, catch, + try) +import Control.Monad (unless, when) import Data.Bits (Bits, complement) -import Data.List (intercalate) +import Data.List (intercalate, isSubsequenceOf) import Data.Type.Equality (testEquality) import Data.Typeable (Proxy (..), (:~:) (Refl)) import GHC.TypeLits (KnownNat, natVal) @@ -24,7 +25,9 @@ import System.Posix.Temp (mkdtemp) import System.Process (callProcess, readProcess) import System.Random (Random) import Test.Framework (Test, testGroup) +import Test.Framework.Providers.HUnit (testCase) import Test.Framework.Providers.QuickCheck2 (testProperty) +import Test.HUnit (Assertion, assertFailure) import Test.QuickCheck (Arbitrary, Gen, Property, arbitrary, choose, elements, forAll, forAllBlind, frequency, @@ -50,6 +53,7 @@ tests = , testProperty "Compile specification in custom dir" testCompileCustomDir , testProperty "Run specification" testRun , testProperty "Run and compare results" testRunCompare + , testCase "Reject empty arrays and structs" testRejectEmpties ] -- * Individual tests @@ -137,6 +141,65 @@ testCompileCustomDir = ioProperty $ do args = [] +data Empty = Empty + +instance Struct Empty where + typeName _ = "" + toValues _ = [] + +instance Typed Empty where + typeOf = Struct Empty + +-- | Test that compiling a spec with an empty array or struct raises an error. +-- C99 does not support zero-length arrays or structs without fields, so Copilot +-- should report an error during compilation. +testRejectEmpties :: Assertion +testRejectEmpties = do + tmpDir <- getTemporaryDirectory + setCurrentDirectory tmpDir + + r1 <- try (compile "copilot_test" $ spec t1) :: IO (Either ErrorCall ()) + unless (isErrZeroArray r1) $ assertFailure "Const zero-length array" + + r2 <- try (compile "copilot_test" $ spec t2) :: IO (Either ErrorCall ()) + unless (isErrZeroArray r2) $ assertFailure "Extern zero-length array" + + r3 <- try (compile "copilot_test" $ spec t3) :: IO (Either ErrorCall ()) + unless (isErrEmptyStruct r3) $ assertFailure "Const empty struct" + + r4 <- try (compile "copilot_test" $ spec t4) :: IO (Either ErrorCall ()) + unless (isErrEmptyStruct r4) $ assertFailure "Extern empty struct" + + where + + spec a = Spec streams observers (triggers a) properties + + streams = [] + observers = [] + triggers a = [ Trigger "trig" (Const Bool True) a ] + properties = [] + + t1 = [ UExpr arrTy (Const arrTy (array [])) ] + t2 = [ UExpr arrTy (ExternVar arrTy "arrs" Nothing) ] + t3 = [ UExpr structTy (Const structTy Empty) ] + t4 = [ UExpr structTy (ExternVar structTy "structs" Nothing) ] + + arrTy :: Type (Array 0 Bool) + arrTy = Array Bool + + structTy :: Type Empty + structTy = Struct Empty + + isErrZeroArray :: Either ErrorCall a -> Bool + isErrZeroArray e = case e of + Left (ErrorCall msg) -> "zero-length array" `isSubsequenceOf` msg + _ -> False + + isErrEmptyStruct :: Either ErrorCall a -> Bool + isErrEmptyStruct e = case e of + Left (ErrorCall msg) -> "empty struct" `isSubsequenceOf` msg + _ -> False + -- | Test compiling a spec and running the resulting program. -- -- The actual behavior is ignored. From a0126958b9899c2c26ae7907aa66a6aad17e6750 Mon Sep 17 00:00:00 2001 From: Chris Hathhorn Date: Mon, 16 Feb 2026 22:28:22 -0600 Subject: [PATCH 03/29] copilot-c99: Document changes in CHANGELOG. Refs #695. --- copilot-c99/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-c99/CHANGELOG b/copilot-c99/CHANGELOG index 7a2ef8da6..7e5b7d15d 100644 --- a/copilot-c99/CHANGELOG +++ b/copilot-c99/CHANGELOG @@ -1,3 +1,6 @@ +2026-02-16 + * Raise error when compiling empty arrays or structs. (#695) + 2026-01-07 * Version bump (4.6.1). (#705) From b1e21ae35dcae6fb9fda63e462ae11bd411cec90 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 22:56:55 -0800 Subject: [PATCH 04/29] copilot-verifier: Relax version constraints on what4. Refs #716. In order to keep Copilot effectively working in the current Haskell ecosystem, as well as new versions of GHC, we need to extend the versions of dependencies that Copilot can be installed with. For example, ogma-extra has seen release 1.12, but copilot-visualizer needs versions strictly lower than 1.10. This commit relaxes the version constrains on `what4` for the `copilot-verifier` package. --- copilot-verifier/copilot-verifier.cabal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot-verifier/copilot-verifier.cabal b/copilot-verifier/copilot-verifier.cabal index f77ebfcaf..691216ecc 100644 --- a/copilot-verifier/copilot-verifier.cabal +++ b/copilot-verifier/copilot-verifier.cabal @@ -62,7 +62,7 @@ common bldflags text, transformers, vector, - what4 >= 1.6.1 && < 1.7 + what4 >= 1.6.1 && < 1.8 library import: bldflags From e740fdd1e8babf2b1136b603cde4a9361a75b2d4 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 22:57:14 -0800 Subject: [PATCH 05/29] copilot-visualizer: Relax version constraints on ogma-extra. Refs #716. In order to keep Copilot effectively working in the current Haskell ecosystem, as well as new versions of GHC, we need to extend the versions of dependencies that Copilot can be installed with. For example, ogma-extra has seen release 1.12, but copilot-visualizer needs versions strictly lower than 1.10. This commit relaxes the version constrains on `ogma-extra` for the `copilot-visualizer` package. --- copilot-visualizer/copilot-visualizer.cabal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot-visualizer/copilot-visualizer.cabal b/copilot-visualizer/copilot-visualizer.cabal index c481a8d00..a8b3b9511 100644 --- a/copilot-visualizer/copilot-visualizer.cabal +++ b/copilot-visualizer/copilot-visualizer.cabal @@ -61,7 +61,7 @@ library filepath >= 1.4.2 && < 1.6, hint >= 0.9.0 && < 1.10, pretty >= 1.0 && < 1.2, - ogma-extra >= 1.6.0 && < 1.10, + ogma-extra >= 1.6.0 && < 1.13, text >= 1.2.3.1 && < 2.2, websockets >= 0.12.7 && < 0.14, From 2fa1c2d93071b941fecd10400b68a36b6a4280e0 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 23:01:07 -0800 Subject: [PATCH 06/29] copilot-verifier: Document changes in CHANGELOG. Refs #716. --- copilot-verifier/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-verifier/CHANGELOG b/copilot-verifier/CHANGELOG index ca8740289..ec8c2c738 100644 --- a/copilot-verifier/CHANGELOG +++ b/copilot-verifier/CHANGELOG @@ -1,3 +1,6 @@ +2026-03-07 + * Relax version constraints on what4. (#716) + 2026-01-07 * Version bump (4.6.1). (#705) From e3a02223f273ae89b6616fac7c4ac33994346be8 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 23:01:40 -0800 Subject: [PATCH 07/29] copilot-visualizer: Document changes in CHANGELOG. Refs #716. --- copilot-visualizer/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-visualizer/CHANGELOG b/copilot-visualizer/CHANGELOG index 85bc41739..3bbc45cc2 100644 --- a/copilot-visualizer/CHANGELOG +++ b/copilot-visualizer/CHANGELOG @@ -1,3 +1,6 @@ +2026-03-07 + * Relax version constraints on ogma-extra. (#716) + 2026-01-07 * Version bump (4.6.1). (#705) From de96e47d79e1c26ab0424c159d91e235dac337a7 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 19:59:22 -0800 Subject: [PATCH 08/29] copilot-core: Version bump (4.7). Refs #714. --- copilot-core/copilot-core.cabal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot-core/copilot-core.cabal b/copilot-core/copilot-core.cabal index 336db0f26..6d99e77d6 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.6.1 +version: 4.7 synopsis: An intermediate representation for Copilot. description: Intermediate representation for Copilot. From ad0d904a089ac7c5c63d09aead59aab32d3adbda Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 19:59:22 -0800 Subject: [PATCH 09/29] copilot-bluespec: Version bump (4.7). Refs #714. --- copilot-bluespec/copilot-bluespec.cabal | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/copilot-bluespec/copilot-bluespec.cabal b/copilot-bluespec/copilot-bluespec.cabal index b727af7fa..3ac0839cf 100644 --- a/copilot-bluespec/copilot-bluespec.cabal +++ b/copilot-bluespec/copilot-bluespec.cabal @@ -1,6 +1,6 @@ cabal-version : >= 1.10 name : copilot-bluespec -version : 4.6.1 +version : 4.7 synopsis : A compiler for Copilot targeting FPGAs. description : This package is a back-end from Copilot to FPGAs in Bluespec. @@ -51,8 +51,8 @@ library , ieee754 >= 0.8.0 && < 0.9 , pretty >= 1.1.2 && < 1.2 - , copilot-core >= 4.6.1 && < 4.7 - , language-bluespec >= 0.1 && < 0.2 + , copilot-core >= 4.7 && < 4.8 + , language-bluespec >= 0.1 && < 0.2 exposed-modules : Copilot.Compile.Bluespec From fb6b1821826bd8f961af141cc391f779f7efcfe8 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 19:59:22 -0800 Subject: [PATCH 10/29] copilot-c99: Version bump (4.7). Refs #714. --- copilot-c99/copilot-c99.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-c99/copilot-c99.cabal b/copilot-c99/copilot-c99.cabal index 40407cec2..0567e9416 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.6.1 +version : 4.7 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.6.1 && < 4.7 + , copilot-core >= 4.7 && < 4.8 , language-c99 >= 0.2.0 && < 0.3 , language-c99-simple >= 0.3 && < 0.4 From 7710ae216956eb372e9a3d667a39d5ac32ffd1e8 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 19:59:22 -0800 Subject: [PATCH 11/29] copilot-prettyprinter: Version bump (4.7). Refs #714. --- copilot-prettyprinter/copilot-prettyprinter.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-prettyprinter/copilot-prettyprinter.cabal b/copilot-prettyprinter/copilot-prettyprinter.cabal index b303db95f..f6f5fcc57 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.6.1 +version: 4.7 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.6.1 && < 4.7 + copilot-core >= 4.7 && < 4.8 exposed-modules: From 750f585d516dfec7bb1ae25c26ce0d3cfe196595 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 19:59:22 -0800 Subject: [PATCH 12/29] copilot-interpreter: Version bump (4.7). Refs #714. --- copilot-interpreter/copilot-interpreter.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-interpreter/copilot-interpreter.cabal b/copilot-interpreter/copilot-interpreter.cabal index 7395226ab..9ef09f117 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.6.1 +version: 4.7 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.6.1 && < 4.7 + copilot-core >= 4.7 && < 4.8 exposed-modules: From 41194365d25a1eac86a3e8cbfdd563f85084dae7 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 19:59:22 -0800 Subject: [PATCH 13/29] copilot-theorem: Version bump (4.7). Refs #714. --- copilot-theorem/copilot-theorem.cabal | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal index 173e90eca..f8b4ff57e 100644 --- a/copilot-theorem/copilot-theorem.cabal +++ b/copilot-theorem/copilot-theorem.cabal @@ -14,7 +14,7 @@ description: . -version : 4.6.1 +version : 4.7 license : BSD3 license-file : LICENSE maintainer : Ivan Perez @@ -62,8 +62,8 @@ library , xml >= 1.3 && < 1.4 , what4 >= 1.3 && < 1.8 - , copilot-core >= 4.6.1 && < 4.7 - , copilot-prettyprinter >= 4.6.1 && < 4.7 + , copilot-core >= 4.7 && < 4.8 + , copilot-prettyprinter >= 4.7 && < 4.8 exposed-modules : Copilot.Theorem , Copilot.Theorem.Prove From 65ef8e6332b2f5bf2ccb2ccbc318ddfda416b060 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 19:59:22 -0800 Subject: [PATCH 14/29] copilot-language: Version bump (4.7). Refs #714. --- copilot-language/copilot-language.cabal | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/copilot-language/copilot-language.cabal b/copilot-language/copilot-language.cabal index 0b65b5798..740bb2b8c 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.6.1 +version: 4.7 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.6.1 && < 4.7 - , copilot-interpreter >= 4.6.1 && < 4.7 - , copilot-theorem >= 4.6.1 && < 4.7 + , copilot-core >= 4.7 && < 4.8 + , copilot-interpreter >= 4.7 && < 4.8 + , copilot-theorem >= 4.7 && < 4.8 exposed-modules: Copilot.Language , Copilot.Language.Operators.BitWise From 0133c62e635713ec46f19cc04a7d42f6b798128e Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 19:59:22 -0800 Subject: [PATCH 15/29] copilot-libraries: Version bump (4.7). Refs #714. --- copilot-libraries/copilot-libraries.cabal | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/copilot-libraries/copilot-libraries.cabal b/copilot-libraries/copilot-libraries.cabal index c864c9cda..e194daf78 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.6.1 +version: 4.7 synopsis: Libraries for the Copilot language. description: Libraries for the Copilot language. @@ -38,10 +38,10 @@ library build-depends: base >= 4.9 && < 5 - , containers >= 0.4 && < 0.9 - , mtl >= 2.0 && < 2.4 - , parsec >= 2.0 && < 3.2 - , copilot-language >= 4.6.1 && < 4.7 + , containers >= 0.4 && < 0.9 + , mtl >= 2.0 && < 2.4 + , parsec >= 2.0 && < 3.2 + , copilot-language >= 4.7 && < 4.8 exposed-modules: Copilot.Library.Libraries From 3d9d882fcd9922aa4880d02bfc7b70c36a8cfa41 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 19:59:22 -0800 Subject: [PATCH 16/29] copilot-verifier: Version bump (4.7). Refs #714. --- copilot-verifier/copilot-verifier.cabal | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/copilot-verifier/copilot-verifier.cabal b/copilot-verifier/copilot-verifier.cabal index 691216ecc..c7bf36a10 100644 --- a/copilot-verifier/copilot-verifier.cabal +++ b/copilot-verifier/copilot-verifier.cabal @@ -1,6 +1,6 @@ Cabal-version: 2.2 Name: copilot-verifier -Version: 4.6.1 +Version: 4.7 Author: Galois Inc. Maintainer: rscott@galois.com Copyright: (c) Galois, Inc 2021-2024 @@ -45,9 +45,9 @@ common bldflags bv-sized >= 1.0.0 && < 1.1, bytestring, containers >= 0.5.9.0, - copilot-c99 >= 4.6.1 && < 4.7, - copilot-core >= 4.6.1 && < 4.7, - copilot-theorem >= 4.6.1 && < 4.7, + copilot-c99 >= 4.7 && < 4.8, + copilot-core >= 4.7 && < 4.8, + copilot-theorem >= 4.7 && < 4.8, crucible >= 0.7.1 && < 0.8, crucible-llvm >= 0.7 && < 0.8, crux >= 0.7.1 && < 0.8, @@ -80,10 +80,10 @@ library copilot-verifier-examples hs-source-dirs: examples build-depends: case-insensitive, - copilot >= 4.6.1 && < 4.7, - copilot-language >= 4.6.1 && < 4.7, - copilot-libraries >= 4.6.1 && < 4.7, - copilot-prettyprinter >= 4.6.1 && < 4.7, + copilot >= 4.7 && < 4.8, + copilot-language >= 4.7 && < 4.8, + copilot-libraries >= 4.7 && < 4.8, + copilot-prettyprinter >= 4.7 && < 4.8, copilot-verifier exposed-modules: Copilot.Verifier.Examples From c59f73ce7f29c6ab7e420b65f09b0fb41ce47110 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 19:59:22 -0800 Subject: [PATCH 17/29] copilot-visualizer: Version bump (4.7). Refs #714. --- copilot-visualizer/copilot-visualizer.cabal | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/copilot-visualizer/copilot-visualizer.cabal b/copilot-visualizer/copilot-visualizer.cabal index a8b3b9511..0500c1b43 100644 --- a/copilot-visualizer/copilot-visualizer.cabal +++ b/copilot-visualizer/copilot-visualizer.cabal @@ -1,6 +1,6 @@ cabal-version: >= 1.10 name: copilot-visualizer -version: 4.6.1 +version: 4.7 synopsis: Visualizer for Copilot. description: Visualizer for Copilot. @@ -65,10 +65,10 @@ library text >= 1.2.3.1 && < 2.2, websockets >= 0.12.7 && < 0.14, - copilot >= 4.6.1 && < 4.7, - copilot-core >= 4.6.1 && < 4.7, - copilot-interpreter >= 4.6.1 && < 4.7, - copilot-language >= 4.6.1 && < 4.7 + copilot >= 4.7 && < 4.8, + copilot-core >= 4.7 && < 4.8, + copilot-interpreter >= 4.7 && < 4.8, + copilot-language >= 4.7 && < 4.8 exposed-modules: @@ -121,7 +121,7 @@ executable tikz-example build-depends: base >= 4.9 && < 5, - copilot >= 4.6.1 && < 4.7, + copilot >= 4.7 && < 4.8, copilot-visualizer if flag(examples) From ff624408e746be0de496c4bd8b95d8976b909744 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 19:59:22 -0800 Subject: [PATCH 18/29] copilot: Version bump (4.7). Refs #714. --- copilot/copilot.cabal | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/copilot/copilot.cabal b/copilot/copilot.cabal index 66304a0f8..68ff811ec 100644 --- a/copilot/copilot.cabal +++ b/copilot/copilot.cabal @@ -1,5 +1,5 @@ name: copilot -version: 4.6.1 +version: 4.7 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.6.1 && < 4.7 - , copilot-theorem >= 4.6.1 && < 4.7 - , copilot-language >= 4.6.1 && < 4.7 - , copilot-libraries >= 4.6.1 && < 4.7 - , copilot-c99 >= 4.6.1 && < 4.7 - , copilot-prettyprinter >= 4.6.1 && < 4.7 + , copilot-core >= 4.7 && < 4.8 + , copilot-theorem >= 4.7 && < 4.8 + , copilot-language >= 4.7 && < 4.8 + , copilot-libraries >= 4.7 && < 4.8 + , copilot-c99 >= 4.7 && < 4.8 + , copilot-prettyprinter >= 4.7 && < 4.8 exposed-modules: Language.Copilot, Language.Copilot.Main From 58a46b16c9aa34e452f2b5e1d732aff17aa8f87f Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 20:00:57 -0800 Subject: [PATCH 19/29] copilot-core: Document changes in CHANGELOG. Refs #714. --- copilot-core/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index c00db088a..671e39ef6 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,3 +1,6 @@ +2026-03-07 + * Version bump (4.7). (#714) + 2026-01-07 * Version bump (4.6.1). (#705) From 1da71446819d71af33b469a9d1475500e3125231 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 20:00:57 -0800 Subject: [PATCH 20/29] copilot-bluespec: Document changes in CHANGELOG. Refs #714. --- copilot-bluespec/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG index 9235a2a27..9072a0a43 100644 --- a/copilot-bluespec/CHANGELOG +++ b/copilot-bluespec/CHANGELOG @@ -1,3 +1,6 @@ +2026-03-07 + * Version bump (4.7). (#714) + 2026-01-07 * Version bump (4.6.1). (#705) * Disable test suite via newly added manual cabal flag. (#673) From 186daf5724c48f38100d9efbaaf5dd1dbafa816f Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 20:00:57 -0800 Subject: [PATCH 21/29] copilot-c99: Document changes in CHANGELOG. Refs #714. --- copilot-c99/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-c99/CHANGELOG b/copilot-c99/CHANGELOG index 7e5b7d15d..856d51497 100644 --- a/copilot-c99/CHANGELOG +++ b/copilot-c99/CHANGELOG @@ -1,4 +1,5 @@ -2026-02-16 +2026-03-07 + * Version bump (4.7). (#714) * Raise error when compiling empty arrays or structs. (#695) 2026-01-07 From 3149bcc1ab290f0281fc23bb23367aec974793fd Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 20:00:57 -0800 Subject: [PATCH 22/29] copilot-prettyprinter: Document changes in CHANGELOG. Refs #714. --- copilot-prettyprinter/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-prettyprinter/CHANGELOG b/copilot-prettyprinter/CHANGELOG index ed0b61ad9..efa6ccf51 100644 --- a/copilot-prettyprinter/CHANGELOG +++ b/copilot-prettyprinter/CHANGELOG @@ -1,3 +1,6 @@ +2026-03-07 + * Version bump (4.7). (#714) + 2026-01-07 * Version bump (4.6.1). (#705) From e5b1bc27c302d663b5ebb94e2f76ab675b6311df Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 20:00:57 -0800 Subject: [PATCH 23/29] copilot-interpreter: Document changes in CHANGELOG. Refs #714. --- copilot-interpreter/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-interpreter/CHANGELOG b/copilot-interpreter/CHANGELOG index 1827da72f..c2920d179 100644 --- a/copilot-interpreter/CHANGELOG +++ b/copilot-interpreter/CHANGELOG @@ -1,3 +1,6 @@ +2026-03-07 + * Version bump (4.7). (#714) + 2026-01-07 * Version bump (4.6.1). (#705) From 0ee707328bf1b4996208af713931b08a503fc913 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 20:00:57 -0800 Subject: [PATCH 24/29] copilot-theorem: Document changes in CHANGELOG. Refs #714. --- copilot-theorem/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index f3dd23d68..4aaf2cf97 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,3 +1,6 @@ +2026-03-07 + * Version bump (4.7). (#714) + 2026-01-07 * Version bump (4.6.1). (#705) * Relax version constraint on containers, random. (#603) From 680467e4a8a74a33c169b421801ddbe5b23f6259 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 20:00:57 -0800 Subject: [PATCH 25/29] copilot-language: Document changes in CHANGELOG. Refs #714. --- copilot-language/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-language/CHANGELOG b/copilot-language/CHANGELOG index eca064537..4751f7061 100644 --- a/copilot-language/CHANGELOG +++ b/copilot-language/CHANGELOG @@ -1,3 +1,6 @@ +2026-03-07 + * Version bump (4.7). (#714) + 2026-01-07 * Version bump (4.6.1). (#705) * Relax version constraint on containers. (#603) From 9d3605a597bcdf130d3f9ec291681d21a2dcc2a5 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 20:00:57 -0800 Subject: [PATCH 26/29] copilot-libraries: Document changes in CHANGELOG. Refs #714. --- copilot-libraries/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG index 6ae010b91..171b9b7d7 100644 --- a/copilot-libraries/CHANGELOG +++ b/copilot-libraries/CHANGELOG @@ -1,3 +1,6 @@ +2026-03-07 + * Version bump (4.7). (#714) + 2026-01-07 * Version bump (4.6.1). (#705) * Relax version constraint on containers. (#603) From 7d651deafe18dec7f88516040e91841f16df010a Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 20:00:57 -0800 Subject: [PATCH 27/29] copilot-verifier: Document changes in CHANGELOG. Refs #714. --- copilot-verifier/CHANGELOG | 1 + 1 file changed, 1 insertion(+) diff --git a/copilot-verifier/CHANGELOG b/copilot-verifier/CHANGELOG index ec8c2c738..049ec2243 100644 --- a/copilot-verifier/CHANGELOG +++ b/copilot-verifier/CHANGELOG @@ -1,4 +1,5 @@ 2026-03-07 + * Version bump (4.7). (#714) * Relax version constraints on what4. (#716) 2026-01-07 From b4f0c279c1a6b5f288f865d830303fd37ca7a58f Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 20:00:57 -0800 Subject: [PATCH 28/29] copilot-visualizer: Document changes in CHANGELOG. Refs #714. --- copilot-visualizer/CHANGELOG | 1 + 1 file changed, 1 insertion(+) diff --git a/copilot-visualizer/CHANGELOG b/copilot-visualizer/CHANGELOG index 3bbc45cc2..402ec34d5 100644 --- a/copilot-visualizer/CHANGELOG +++ b/copilot-visualizer/CHANGELOG @@ -1,4 +1,5 @@ 2026-03-07 + * Version bump (4.7). (#714) * Relax version constraints on ogma-extra. (#716) 2026-01-07 From cdbcdac2f56db48cac22ee0ef225b0396c2a4929 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Mar 2026 20:00:57 -0800 Subject: [PATCH 29/29] copilot: Document changes in CHANGELOG. Refs #714. --- copilot/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index 15678af71..dd34bc70f 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,3 +1,6 @@ +2026-03-07 + * Version bump (4.7). (#714) + 2026-01-07 * Version bump (4.6.1). (#705) * Relax version constraint on optparse-applicative. (#603)