From 5de4a7bb82e9671b7961b8b0b4c222e0738a1bc3 Mon Sep 17 00:00:00 2001 From: Chris Hathhorn Date: Tue, 9 Jun 2026 13:53:43 -0500 Subject: [PATCH 001/118] copilot-theorem: Extend range of versions of Kind2. Refs #734. In order to keep Copilot effectively working in the current software ecosystem, we need to extend the versions of dependencies that Copilot can be installed with. kind2 has seen release 2.3.0, but copilot-theorem requires kind2 0.7.2. This commit updates the copilot-theorem Kind2 native-format backend to produce output targeting modern releases of Kind2. It has been tested with Kind2 v2.3, the latest at the time of this commit. --- copilot-theorem/copilot-theorem.cabal | 2 +- .../src/Copilot/Theorem/Kind2/AST.hs | 51 +++++-- .../src/Copilot/Theorem/Kind2/Output.hs | 117 +++++++++------ .../src/Copilot/Theorem/Kind2/PrettyPrint.hs | 49 ++++-- .../src/Copilot/Theorem/Kind2/Prover.hs | 16 +- .../src/Copilot/Theorem/Kind2/Translate.hs | 140 +++++------------- 6 files changed, 196 insertions(+), 179 deletions(-) diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal index cd9d2e00e..1c809e3c9 100644 --- a/copilot-theorem/copilot-theorem.cabal +++ b/copilot-theorem/copilot-theorem.cabal @@ -51,6 +51,7 @@ library , containers >= 0.4 && < 0.9 , data-default >= 0.7 && < 0.9 , directory >= 1.3 && < 1.4 + , extra >= 1.7 && < 1.9 , fp-ieee >= 0.1 && < 0.2 , libBF >= 0.6.2 && < 0.7 , mtl >= 2.0 && < 2.4 @@ -60,7 +61,6 @@ library , process >= 1.6 && < 1.7 , random >= 1.1 && < 1.4 , transformers >= 0.5 && < 0.7 - , xml >= 1.3 && < 1.4 , what4 >= 1.3 && < 1.8 , copilot-core >= 4.7.1 && < 4.8 diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs index e69cda8d0..efd493a6d 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs @@ -1,27 +1,54 @@ {-# LANGUAGE Safe #-} --- | Abstract syntax tree of Kind2 files. +-- | Abstract syntax tree of Kind2 native input files. +-- +-- This represents the native transition system input format supported by +-- Kind2 1.0 and newer (@--input_format native@), in which a file is a +-- sequence of @define-node@ forms, each declaring a state transition system +-- by means of an initial state predicate and a transition relation predicate. +-- The last node defined in a file is the top system analyzed by Kind2, and +-- the properties to check are attached to it. +-- +-- The native input format is largely undocumented, and Kind2's user +-- documentation only covers its Lustre frontend. The best available +-- references for the native format are the parser in the Kind2 sources +-- ([nativeInput.ml] +-- (https://github.com/kind2-mc/kind2/blob/v3.0.0/src/nativeInput.ml)), +-- which includes a sketch of the grammar in a comment near the end of the +-- file) and the example file +-- [two_counters.kind2] +-- (https://github.com/kind2-mc/kind2/blob/develop/examples/two_counters.kind2). module Copilot.Theorem.Kind2.AST where --- | A file is a sequence of predicates and propositions. +-- | A file is a sequence of node definitions, together with a distinguished +-- top node and a series of propositions about the top node. +-- +-- Kind2 analyzes the last node defined in a file as the top system, so the +-- top node is always printed after all the other nodes. data File = File - { filePreds :: [PredDef] - , fileProps :: [Prop] } + { fileNodes :: [Node] -- ^ Nodes other than the top node, in dependency + -- order (a node may only refer to nodes defined + -- before it). + , fileTopNode :: Node -- ^ The top node, which the propositions are + -- attached to. + , fileProps :: [Prop] -- ^ Propositions about the top node. + } -- | A proposition is defined by a term. data Prop = Prop { propName :: String , propTerm :: Term } --- | A predicate definition. -data PredDef = PredDef - { predId :: String -- ^ Identifier for the predicate. - , predStateVars :: [StateVarDef] -- ^ Variables identifying the states in the - -- underlying state transition system. - , predInit :: Term -- ^ Predicate that holds for initial +-- | A node definition. +data Node = Node + { nodeId :: String -- ^ Identifier for the node. + , nodeStateVars :: [StateVarDef] -- ^ Variables identifying the states in + -- the underlying state transition system. + , nodeInit :: Term -- ^ Predicate that holds for initial -- states. - , predTrans :: Term -- ^ Predicate that holds for two states, if - -- there is state transition between them. + , nodeTrans :: Term -- ^ Predicate that holds for two states, + -- if there is a state transition between + -- them. } -- | A definition of a state variable. diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs index f80b8170b..8a1d29c28 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs @@ -4,66 +4,97 @@ -- | Parse output of Kind2. module Copilot.Theorem.Kind2.Output (parseOutput) where -import Text.XML.Light hiding (findChild) -import Copilot.Theorem.Prove as P -import Data.Maybe (fromJust) +import Data.List.Extra (isInfixOf, splitOn, stripInfix, trim) +import Data.Maybe (mapMaybe) + +import Copilot.Theorem.Prove as P import qualified Copilot.Core as C import qualified Copilot.Theorem.Misc.Error as Err -simpleName s = QName s Nothing Nothing - -- | Parse output of Kind2. +-- +-- The output is expected to be in XML format, as produced by Kind2's @-xml@ +-- flag and documented at +-- . +-- Note that this function does not parse the output as XML: when given a +-- system in the native transition system format, Kind2 produces output that +-- is not always well-formed XML (e.g., counterexamples to invariant +-- properties cannot be printed for systems in that format -- the +-- counterexample printing functions in Kind2's @src/inputSystem.ml@ fail with +-- an internal error for native input -- and Kind2 reports the error in the +-- middle of the XML output). Instead, this function looks for the +-- @\@ tag for the given property and extracts the answers in the +-- @\@ tags it contains. parseOutput :: String -- ^ Property whose validity is being checked. -> C.Prop -- ^ The property's quantifier. -> String -- ^ XML output of Kind2 -> P.Output -parseOutput propId propQuantifier xml = fromJust $ do - root <- parseXMLDoc xml - case findAnswer . findPropTag $ root of - "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 +parseOutput propId propQuantifier xml + | "valid" `elem` answers = quantified (Output Valid []) + (Output Invalid []) + | "falsifiable" `elem` answers = quantified (Output Invalid []) + (Output Valid []) + | "unknown" `elem` answers = Output Unknown [] + | null answers = err $ "Answer for property " ++ propId ++ " not found" + | otherwise = err $ "Unrecognized status : " ++ unwords answers where - searchForRuntimeError = undefined + -- Pick an output based on the quantifier of the property. The first + -- argument is returned when the property Kind2 was asked about is valid, + -- and the second one when it is invalid. + -- + -- 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. + -- + -- 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. + quantified ifValid ifInvalid = case propQuantifier of + C.Forall {} -> ifValid + C.Exists {} -> ifInvalid + + -- All the answers reported for the property, in the order in which they + -- appear in the output. A conclusive answer (valid or falsifiable), if + -- any, takes precedence over inconclusive (unknown) ones, which Kind2 may + -- also report when the analysis terminates without an answer for all + -- properties. + answers = mapMaybe answerText + $ filter isRightProperty + $ propertyElems xml - findPropTag root = - let rightElement elt = - qName (elName elt) == "Property" - && lookupAttr (simpleName "name") (elAttribs elt) - == Just propId - in case filterChildren rightElement root of - tag : _ -> tag - _ -> err $ "Tag for property " ++ propId ++ " not found" + -- Substrings of the output following a @\ - case onlyText (elContent answTag) of - answ : _ -> cdData answ - _ -> err "Invalid 'Answer' attribute" - _ -> err "Attribute 'Answer' not found" + -- True if the given property element has the name of the property this + -- function looks for. + isRightProperty elem' = + ("name=\"" ++ escapeAttr propId ++ "\"") `isInfixOf` openingTag + where + openingTag = takeWhile (/= '>') elem' + + -- The contents of the first @\@ tag in the given element, if + -- any. + answerText elem' = do + (_, rest) <- stripInfix "" rest + let answer = trim $ takeWhile (/= '<') rest' + if null answer then Nothing else Just answer err :: forall a . String -> a err msg = Err.fatal $ "Parse error while reading the Kind2 XML output : \n" ++ msg ++ "\n\n" ++ xml + +-- | Escape a string for use as an XML attribute value. +escapeAttr :: String -> String +escapeAttr = concatMap escapeChar + where + escapeChar '&' = "&" + escapeChar '<' = "<" + escapeChar '>' = ">" + escapeChar '"' = """ + escapeChar c = [c] diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs index 6851d46fa..92d158a1c 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs @@ -1,6 +1,8 @@ {-# LANGUAGE Safe #-} --- | Pretty print a Kind2 file defining predicates and propositions. +-- | Pretty print a Kind2 file defining nodes and propositions, in the native +-- transition system input format supported by Kind2 1.0 and newer (see +-- "Copilot.Theorem.Kind2.AST" for pointers to references on the format). module Copilot.Theorem.Kind2.PrettyPrint ( prettyPrint ) where import Copilot.Theorem.Misc.SExpr @@ -15,6 +17,14 @@ type SSExpr = SExpr String -- | Reserved keyword prime. kwPrime = "prime" +-- | Dummy position attached to the properties of the file. +-- +-- Kind2 requires a position (in the format @file:row-col@) for properties +-- declared with the @:user@ source annotation, and reports that position back +-- in its output. +propPosition :: String +propPosition = "copilot:1-1" + -- | Pretty print a Kind2 file. prettyPrint :: File -> String prettyPrint = @@ -29,30 +39,41 @@ shouldIndent (List [Atom a, Atom _]) = a `notElem` [kwPrime] shouldIndent _ = True -- | Convert a file into a sequence of expressions. +-- +-- The top node is printed last, since Kind2 analyzes the last node of the +-- file as the top system. The properties of the file are attached to it. ppFile :: File -> [SSExpr] -ppFile (File preds props) = map ppPredDef preds ++ ppProps props +ppFile (File nodes top props) = + map (`ppNode` []) nodes ++ [ppNode top (ppProps props)] --- | Convert a sequence of propositions into command to check each of them. +-- | Convert a sequence of propositions into a props field. ppProps :: [Prop] -> [SSExpr] -ppProps ps = [ node "check-prop" [ list $ map ppProp ps ] ] +ppProps [] = [] +ppProps ps = [ node "props" [ list $ map ppProp ps ] ] -- | Convert a proposition into an expression. ppProp :: Prop -> SSExpr -ppProp (Prop n t) = list [atom n, ppTerm t] +ppProp (Prop n t) = list [atom n, ppTerm t, atom ":user", atom propPosition] --- | Convert a predicate into an expression. -ppPredDef :: PredDef -> SSExpr -ppPredDef pd = - list [ atom "define-pred" - , atom (predId pd) - , list . map ppStateVarDef . predStateVars $ pd - , node "init" [ppTerm $ predInit pd] - , node "trans" [ppTerm $ predTrans pd] ] +-- | Convert a node, together with optional extra fields, into an expression. +ppNode :: Node -> [SSExpr] -> SSExpr +ppNode n extraFields = + list $ [ atom "define-node" + , atom (nodeId n) + , list . map ppStateVarDef . nodeStateVars $ n + , node "init" [ppTerm $ nodeInit n] + , node "trans" [ppTerm $ nodeTrans n] ] + ++ extraFields -- | Convert a state variable definition into an expression. ppStateVarDef :: StateVarDef -> SSExpr ppStateVarDef svd = - list [atom (varId svd), ppType (varType svd)] + list $ [atom (varId svd), ppType (varType svd)] + ++ map ppStateVarFlag (varFlags svd) + +-- | Convert a state variable option into an expression. +ppStateVarFlag :: StateVarFlag -> SSExpr +ppStateVarFlag FConst = atom ":const" -- | Convert a type into an expression. ppType :: Type -> SSExpr diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs index 4bb52322e..a79ede4f6 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs @@ -28,7 +28,8 @@ import qualified Copilot.Theorem.TransSys as TS -- | Options for Kind2 data Options = Options { bmcMax :: Int -- ^ Upper bound on the number of unrolling that base and - -- step will perform. A value of 0 means /unlimited/. + -- step will perform (passed to Kind2 via its + -- @--unroll_max@ option). A value of 0 means /unlimited/. } -- | Default options with unlimited unrolling for base and step. @@ -41,7 +42,10 @@ data ProverST = ProverST -- | A prover backend based on Kind2. -- --- The executable @kind2@ must exist and its location be in the @PATH@. +-- The executable @kind2@ must exist and its location be in the @PATH@. Kind2 +-- version 1.0 or newer is required: the native input format and the +-- command-line options this prover uses were introduced in Kind2 1.0, and +-- remain supported as of Kind2 3.0. kind2Prover :: Options -> Prover kind2Prover opts = Prover { proverName = "Kind2" @@ -50,24 +54,22 @@ kind2Prover opts = Prover , closeProver = const $ return () } kind2Prog = "kind2" -kind2BaseOptions = ["--input-format", "native", "-xml"] +kind2BaseOptions = ["--input_format", "native", "-xml"] askKind2 :: ProverST -> [PropId] -> [PropId] -> IO Output askKind2 (ProverST opts spec) assumptions toCheck = do - let kind2Input = prettyPrint . toKind2 Inlined assumptions toCheck $ spec + let kind2Input = prettyPrint . toKind2 assumptions toCheck $ spec (tempName, tempHandle) <- openTempFile "." "out" "kind" hPutStr tempHandle kind2Input hClose tempHandle let kind2Options = - kind2BaseOptions ++ ["--bmc_max", show $ bmcMax opts, tempName] + kind2BaseOptions ++ ["--unroll_max", show $ bmcMax opts, tempName] (_, output, _) <- readProcessWithExitCode kind2Prog kind2Options "" - putStrLn kind2Input - removeFile tempName let propId = head toCheck diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs index 123f6ed64..d59aaae24 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs @@ -1,68 +1,44 @@ -{-# LANGUAGE GADTs #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE Safe #-} -{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE Safe #-} -- | Convert modular transition systems ('TransSys') into Kind2 file -- specifications. module Copilot.Theorem.Kind2.Translate ( toKind2 - , Style (..) ) where import Copilot.Theorem.TransSys import qualified Copilot.Theorem.Kind2.AST as K -import Control.Exception.Base (assert) - import Data.Function (on) import Data.Maybe (fromJust) -import Data.List (sort, sortBy) -import Data.Map (Map, (!)) +import Data.List (partition, sort, sortBy) +import Data.Map ((!)) import qualified Data.Map as Map import qualified Data.Bimap as Bimap --- The following properties MUST hold for the given transition system : --- * Nodes are sorted by topological order --- * Nodes are `completed`, which means the dependency graph is transitive --- and each node imports all the local variables of its dependencies --- - -type DepGraph = Map NodeId [NodeId] - --- | Style of the Kind2 files produced: modular (with multiple separate nodes), --- or all inlined (with only one node). --- --- In the modular style, the graph is simplified to remove cycles by collapsing --- all nodes participating in a strongly connected components. --- --- In the inlined style, the structure of the modular transition system is --- discarded and the graph is first turned into a /non-modular transition/ --- /system/ with only one node, which can be then converted into a Kind2 file. -data Style = Inlined | Modular - -- | Produce a Kind2 file that checks the properties specified. -toKind2 :: Style -- ^ Style of the file (modular or inlined). - -> [PropId] -- ^ Assumptions +toKind2 :: [PropId] -- ^ Assumptions -> [PropId] -- ^ Properties to be checked -> TransSys -- ^ Modular transition system holding the system spec -> K.File -toKind2 style assumptions checkedProps spec = - addAssumptions spec assumptions - $ trSpec (complete spec') predCallsGraph assumptions checkedProps +toKind2 assumptions checkedProps spec = + addAssumptions spec' assumptions $ trSpec spec' checkedProps where - predCallsGraph = specDependenciesGraph spec' - spec' = case style of - Inlined -> inline spec - Modular -> removeCycles spec + spec' = inline spec -trSpec :: TransSys -> DepGraph -> [PropId] -> [PropId] -> K.File -trSpec spec predCallsGraph _assumptions checkedProps = K.File preds props +trSpec :: TransSys -> [PropId] -> K.File +trSpec spec checkedProps = K.File otherNodes topNode props where - preds = map (trNode spec predCallsGraph) (specNodes spec) + (topNode, otherNodes) = + case partition ((== specTopNodeId spec) . K.nodeId) nodes of + ([top], others) -> (top, others) + _ -> error $ "Kind2.Translate: top node " + ++ specTopNodeId spec ++ " not found" + nodes = map (trNode spec) (specNodes spec) props = map trProp $ filter ((`elem` checkedProps) . fst) $ Map.toList $ Map.map fst $ specProps spec @@ -70,37 +46,30 @@ trSpec spec predCallsGraph _assumptions checkedProps = K.File preds props trProp :: (PropId, ExtVar) -> K.Prop trProp (pId, var) = K.Prop pId (trVar . extVarLocalPart $ var) -trNode :: TransSys -> DepGraph -> Node -> K.PredDef -trNode spec predCallsGraph node = - K.PredDef { K.predId, K.predStateVars, K.predInit, K.predTrans } - where - predId = nodeId node - predStateVars = gatherPredStateVars spec node - predInit = mkConj $ initLocals node - ++ map (trExpr False) (nodeConstrs node) - ++ predCalls True spec predCallsGraph node - predTrans = mkConj $ transLocals node - ++ map (trExpr True) (nodeConstrs node) - ++ predCalls False spec predCallsGraph node - +trNode :: TransSys -> Node -> K.Node +trNode spec node = K.Node + { K.nodeId = nodeId node + , K.nodeStateVars = gatherPredStateVars spec node + , K.nodeInit = mkConj $ initLocals node + ++ map (trExpr False) (nodeConstrs node) + , K.nodeTrans = mkConj $ transLocals node + ++ map (trExpr True) (nodeConstrs node) + } + +-- | Add the assumptions to the top node of the file by conjoining the +-- corresponding property variables to its initial state and transition +-- relation predicates. addAssumptions :: TransSys -> [PropId] -> K.File -> K.File -addAssumptions spec assumptions (K.File {K.filePreds, K.fileProps}) = - K.File (changeTail aux filePreds) fileProps +addAssumptions spec assumptions file = + file { K.fileTopNode = aux (K.fileTopNode file) } where - changeTail f (reverse -> l) = case l of - [] -> error "impossible" - x : xs -> reverse $ f x : xs - - aux pred = - let init' = mkConj ( K.predInit pred : map K.StateVar vars ) - trans' = mkConj ( K.predTrans pred : map K.PrimedStateVar vars ) - in pred { K.predInit = init', K.predTrans = trans' } + aux node = + let init' = mkConj ( K.nodeInit node : map K.StateVar vars ) + trans' = mkConj ( K.nodeTrans node : map K.PrimedStateVar vars ) + in node { K.nodeInit = init', K.nodeTrans = trans' } - vars = - let bindings = nodeImportedVars (specTopNode 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 + toExtVar a = fst $ fromJust $ Map.lookup a $ specProps spec + vars = map (varName . extVarLocalPart . toExtVar) assumptions -- The ordering really matters here because the variables -- have to be given in this order in a pred call @@ -169,39 +138,6 @@ transLocals node = Expr e -> [mkEquality (trPrimedVar v) (trExpr True e)] Constrs cs -> map (trExpr True) cs -predCalls :: Bool -> TransSys -> DepGraph -> Node -> [K.Term] -predCalls isInitCall spec predCallsGraph node = - map mkCall toCall - where - nid = nodeId node - toCall = predCallsGraph ! nid - nodesMap = Map.fromList [(nodeId n, n) | n <- specNodes spec] - - nodeLocals n = - map (ExtVar n) . sort . Map.keys - . nodeLocalVars $ (nodesMap ! n) - - mkCall callee - | isInitCall = - K.PredApp callee K.Init (argsSeq trVar) - | otherwise = - K.PredApp callee K.Trans (argsSeq trVar ++ argsSeq trPrimedVar) - where - - calleeLocals = nodeLocals callee - calleeImported = - (concatMap nodeLocals . sort . nodeDependencies) $ nodesMap ! callee - - localAlias trVarF ev = - case Bimap.lookupR ev $ nodeImportedVars node of - Nothing -> error $ - "This spec is not complete : " - ++ show ev ++ " should be imported in " ++ nid - Just v -> trVarF v - - argsSeq trVarF = - map (localAlias trVarF) (calleeLocals ++ calleeImported) - trExpr :: Bool -> Expr t -> K.Term trExpr primed = tr where From 8258eb4968490d46bcb651c870b64d73398c7adb Mon Sep 17 00:00:00 2001 From: Chris Hathhorn Date: Mon, 22 Jun 2026 14:26:39 -0500 Subject: [PATCH 002/118] copilot-theorem: Update README for Kind2 backend changes. Refs #734. In order to keep Copilot effectively working in the current software ecosystem, we need to extend the versions of dependencies that Copilot can be installed with. kind2 has seen release 2.3.0, but copilot-theorem requires kind2 0.7.2. This commit updates copilot-theorem's README to reflect updates required to the Kind2 backend for supporting newer versions of Kind2 (e.g., the renaming Kind2's "--bmc_max" flag to "--unroll_max"). --- copilot-theorem/README.md | 40 +++++++++++++++++++++++++-------------- 1 file changed, 26 insertions(+), 14 deletions(-) diff --git a/copilot-theorem/README.md b/copilot-theorem/README.md index 64cce8995..47a4b6081 100644 --- a/copilot-theorem/README.md +++ b/copilot-theorem/README.md @@ -31,7 +31,8 @@ properties on Copilot programs. It includes: * The *copilot-core* and *copilot-prettyprinter* Haskell libraries * The *Yices2* SMT-solver: `yices-smt2` must be in your `$PATH` * The *Z3* SMT-solver: `z3` must be in your `$PATH` -* The *Kind2* model checker: `kind2` must be in your `$PATH` +* The *Kind2* model checker (version 1.0 or newer): `kind2` must be in your + `$PATH` To build it, just install the Copilot library as described in the top-level README. @@ -87,7 +88,9 @@ configuration. The *Kind2* prover uses the model checker with the same name, from the University of Iowa. It translates the Copilot specification into a *modular transition system* (the Kind2 native format) and then calls the `kind2` -executable. +executable. Kind2 version 1.0 or newer is required: the native input format +and the command-line options used by this prover were introduced in Kind2 +1.0, and remain supported as of Kind2 3.0. It is provided by the `Copilot.Theorem.Kind2` module, which exports a `kind2Prover :: Options -> Prover` where the `Options` type is defined as @@ -95,7 +98,7 @@ It is provided by the `Copilot.Theorem.Kind2` module, which exports a `kind2Prov ```haskell data Options = Options { bmcMax :: Int } ``` -and where `bmcMax` corresponds to the `--bmc_max` option of *kind2* and is +and where `bmcMax` corresponds to the `--unroll_max` option of *kind2* and is equivalent to the `maxK` option of the K-Induction prover. Its default value is 0, which stands for infinity. @@ -335,11 +338,16 @@ process. The transition system obtained by the `TransSys.Translate` module is perfectly consistent. However, it can't be directly translated into the *Kind2 native -file format*. Indeed, it is natural to bind each node to a predicate but the -Kind2 file format requires that each predicate only uses previously defined -predicates. However, some nodes in our transition system could be mutually -recursive. Therefore, the goal of the `removeCycles :: Spec -> Spec` function, -defined in `TransSys.Transform`, is to remove such dependency cycles. +file format*. The native input format of Kind2 (version 1.0 and newer) does +not support predicate calls inside the initial state and transition relation +predicates of a node, so the modular structure of the transition system cannot +be expressed directly in it. Therefore, the system is first turned into an +equivalent non-modular transition system with only one node by the +`inline :: Spec -> Spec` function, defined in `TransSys.Transform`: +```haskell +inline :: Spec -> Spec +inline spec = mergeNodes [nodeId n | n <- specNodes spec] spec +``` This function relies on the `mergeNodes :: [NodeId] -> Spec -> Spec` function, whose signature is self-explicit. The latter solves name conflicts by using the @@ -516,10 +524,14 @@ in the Kind2 SMT solver. #### Displaying counterexamples Counterexamples are not displayed with the Kind2 prover because Kind2 doesn't -support XML output of counterexamples. If the last feature is provided, it -should be easy to implement displaying of counterexamples in *copilot-theorem*. -For this, we recommend keeping some information about *observers* in -`TransSys.Spec` and to add one variable per observer in the Kind2 output file. +support the output of counterexamples for systems expressed in its native input +format (the counterexample printing functions in Kind2's +[`src/inputSystem.ml`](https://github.com/kind2-mc/kind2/blob/v3.0.0/src/inputSystem.ml) +fail with an internal error for native input). If Kind2 adds this feature, it +should be easy to implement displaying of counterexamples in +*copilot-theorem*. For this, we recommend keeping some information about +*observers* in `TransSys.Spec` and to add one variable per observer in the +Kind2 output file. #### Bad handling of non-linear operators and external functions @@ -569,14 +581,14 @@ architecture of Kind2. It is true that the code of `TransSys` is quite complex. In fact, it would be really straightforward to produce a flattened transition system and then a -Kind2 file with just a single *top* predicate. In fact, It would be as easy as +Kind2 file with just a single *top* node. In fact, It would be as easy as producing an *IL* specification. To be honest, I'm not sure producing a modular *Kind2* output is worth the complexity added. It's especially true at the time I write this in the sense that: -* Each predicate introduced is used only one time (which is true because +* Each node introduced is used only one time (which is true because Copilot doesn't handle functions or parameterized streams like Lustre does and everything is inlined during the reification process). * A similar form of structure could be obtained from a flattened Kind2 native From b8ff2fbaa16abac1441d172fa557e727d4380e66 Mon Sep 17 00:00:00 2001 From: Chris Hathhorn Date: Tue, 9 Jun 2026 13:54:17 -0500 Subject: [PATCH 003/118] copilot-theorem: Document changes in CHANGELOG. Refs #734. --- copilot-theorem/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index 03facaf36..fd4dea25b 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,3 +1,6 @@ +2026-06-09 + * Extend range of versions of Kind2. (#734) + 2026-05-07 * Version bump (4.7.1). (#730) * Handle special Float values correctly for counterexamples. (#697) From 423e4bd95130c1148a0a8ab826d732892ee25468 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 004/118] copilot-core: Version bump (4.8). Refs #745. --- 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 ee463977c..541cad1e3 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.7.1 +version: 4.8 synopsis: An intermediate representation for Copilot. description: Intermediate representation for Copilot. From 068fb4dd5f9f4be6457b722666674fd8d1ee0ad4 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 005/118] copilot-bluespec: Version bump (4.8). Refs #745. --- 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 ffaadaca2..2cff39b37 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.7.1 +version : 4.8 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.7.1 && < 4.8 - , language-bluespec >= 0.1 && < 0.2 + , copilot-core >= 4.8 && < 4.9 + , language-bluespec >= 0.1 && < 0.2 exposed-modules : Copilot.Compile.Bluespec From e89270da21a828c45ddb39d73c02931f4973ffa2 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 006/118] copilot-c99: Version bump (4.8). Refs #745. --- 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 d9802bd42..d3defea3f 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.7.1 +version : 4.8 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.7.1 && < 4.8 + , copilot-core >= 4.8 && < 4.9 , language-c99 >= 0.2.0 && < 0.3 , language-c99-simple >= 0.3 && < 0.4 From 2d8b28ad156c1546b39aa8cbef83468ba3c545b4 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 007/118] copilot-prettyprinter: Version bump (4.8). Refs #745. --- 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 c40511c43..393ae9b37 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.7.1 +version: 4.8 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.7.1 && < 4.8 + copilot-core >= 4.8 && < 4.9 exposed-modules: From 792d6d9bff09ecec03538e7d82e72779c7596397 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 008/118] copilot-interpreter: Version bump (4.8). Refs #745. --- 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 0303bf17b..255d0400d 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.7.1 +version: 4.8 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.7.1 && < 4.8 + copilot-core >= 4.8 && < 4.9 exposed-modules: From bce90b0d81f566d61a0b4e136e4f2ee480217823 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 009/118] copilot-theorem: Version bump (4.8). Refs #745. --- 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 1c809e3c9..28127ebd0 100644 --- a/copilot-theorem/copilot-theorem.cabal +++ b/copilot-theorem/copilot-theorem.cabal @@ -14,7 +14,7 @@ description: . -version : 4.7.1 +version : 4.8 license : BSD3 license-file : LICENSE maintainer : Ivan Perez @@ -63,8 +63,8 @@ library , transformers >= 0.5 && < 0.7 , what4 >= 1.3 && < 1.8 - , copilot-core >= 4.7.1 && < 4.8 - , copilot-prettyprinter >= 4.7.1 && < 4.8 + , copilot-core >= 4.8 && < 4.9 + , copilot-prettyprinter >= 4.8 && < 4.9 exposed-modules : Copilot.Theorem , Copilot.Theorem.Prove From 40b284454e23c9c15963eeba2447e9e6f9c0ea55 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 010/118] copilot-language: Version bump (4.8). Refs #745. --- 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 2cfab8eb8..ca5232a8c 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.7.1 +version: 4.8 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.7.1 && < 4.8 - , copilot-interpreter >= 4.7.1 && < 4.8 - , copilot-theorem >= 4.7.1 && < 4.8 + , copilot-core >= 4.8 && < 4.9 + , copilot-interpreter >= 4.8 && < 4.9 + , copilot-theorem >= 4.8 && < 4.9 exposed-modules: Copilot.Language , Copilot.Language.Operators.BitWise From 27e4a4988ae552850ac4c9227a74fc682af14482 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 011/118] copilot-libraries: Version bump (4.8). Refs #745. --- copilot-libraries/copilot-libraries.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-libraries/copilot-libraries.cabal b/copilot-libraries/copilot-libraries.cabal index 85b117f63..dd96c07d4 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.7.1 +version: 4.8 synopsis: Libraries for the Copilot language. description: Libraries for the Copilot language. @@ -41,7 +41,7 @@ library , containers >= 0.4 && < 0.9 , mtl >= 2.0 && < 2.4 , parsec >= 2.0 && < 3.2 - , copilot-language >= 4.7.1 && < 4.8 + , copilot-language >= 4.8 && < 4.9 exposed-modules: Copilot.Library.Analysis From 766bf4f787fde14e88d6cf32e1e28c848b7b93c0 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 012/118] copilot-verifier: Version bump (4.8). Refs #745. --- 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 339892ec9..aed3a0f10 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.7.1 +Version: 4.8 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.7.1 && < 4.8, - copilot-core >= 4.7.1 && < 4.8, - copilot-theorem >= 4.7.1 && < 4.8, + copilot-c99 >= 4.8 && < 4.9, + copilot-core >= 4.8 && < 4.9, + copilot-theorem >= 4.8 && < 4.9, 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.7.1 && < 4.8, - copilot-language >= 4.7.1 && < 4.8, - copilot-libraries >= 4.7.1 && < 4.8, - copilot-prettyprinter >= 4.7.1 && < 4.8, + copilot >= 4.8 && < 4.9, + copilot-language >= 4.8 && < 4.9, + copilot-libraries >= 4.8 && < 4.9, + copilot-prettyprinter >= 4.8 && < 4.9, copilot-verifier exposed-modules: Copilot.Verifier.Examples From cb850da8408028c9628697e87c7c81ef6a385e81 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 013/118] copilot-visualizer: Version bump (4.8). Refs #745. --- copilot-visualizer/copilot-visualizer.cabal | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/copilot-visualizer/copilot-visualizer.cabal b/copilot-visualizer/copilot-visualizer.cabal index 5e8735ea4..1bd88608a 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.7.1 +version: 4.8 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.7.1 && < 4.8, - copilot-core >= 4.7.1 && < 4.8, - copilot-interpreter >= 4.7.1 && < 4.8, - copilot-language >= 4.7.1 && < 4.8 + copilot >= 4.8 && < 4.9, + copilot-core >= 4.8 && < 4.9, + copilot-interpreter >= 4.8 && < 4.9, + copilot-language >= 4.8 && < 4.9 exposed-modules: From 2eabea860dbc45ec2b6f406d6484a15f854e6762 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 014/118] copilot: Version bump (4.8). Refs #745. --- copilot/copilot.cabal | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/copilot/copilot.cabal b/copilot/copilot.cabal index ace61023d..85dd95ab0 100644 --- a/copilot/copilot.cabal +++ b/copilot/copilot.cabal @@ -1,5 +1,5 @@ name: copilot -version: 4.7.1 +version: 4.8 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.7.1 && < 4.8 - , copilot-theorem >= 4.7.1 && < 4.8 - , copilot-language >= 4.7.1 && < 4.8 - , copilot-libraries >= 4.7.1 && < 4.8 - , copilot-c99 >= 4.7.1 && < 4.8 - , copilot-prettyprinter >= 4.7.1 && < 4.8 + , copilot-core >= 4.8 && < 4.9 + , copilot-theorem >= 4.8 && < 4.9 + , copilot-language >= 4.8 && < 4.9 + , copilot-libraries >= 4.8 && < 4.9 + , copilot-c99 >= 4.8 && < 4.9 + , copilot-prettyprinter >= 4.8 && < 4.9 exposed-modules: Language.Copilot, Language.Copilot.Main From 254abaa94f82bc8fd0b7b05d047c197f6c5c55d3 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 015/118] copilot-core: Document changes in CHANGELOG. Refs #745. --- copilot-core/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index 4a019a359..e37d60585 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,3 +1,6 @@ +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) From 88d7cf5abd9b1ff4171ca9635e5549bffddb2749 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 016/118] copilot-bluespec: Document changes in CHANGELOG. Refs #745. --- copilot-bluespec/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG index 63ea6878b..1145b7a83 100644 --- a/copilot-bluespec/CHANGELOG +++ b/copilot-bluespec/CHANGELOG @@ -1,3 +1,6 @@ +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) * Fix translation of special Float values to Bluespec. (#697) From ad9bce157314386f729048cdc9143414f40be55a Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 017/118] copilot-c99: Document changes in CHANGELOG. Refs #745. --- copilot-c99/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-c99/CHANGELOG b/copilot-c99/CHANGELOG index 74c6c1dd4..ba43b631d 100644 --- a/copilot-c99/CHANGELOG +++ b/copilot-c99/CHANGELOG @@ -1,3 +1,6 @@ +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) From 310c80ddf67e8dc10401da6a305189e54ba91575 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 018/118] copilot-prettyprinter: Document changes in CHANGELOG. Refs #745. --- copilot-prettyprinter/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-prettyprinter/CHANGELOG b/copilot-prettyprinter/CHANGELOG index a8e6d3e12..7ffd6c90d 100644 --- a/copilot-prettyprinter/CHANGELOG +++ b/copilot-prettyprinter/CHANGELOG @@ -1,3 +1,6 @@ +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) From e27694855d0c8a8ff6aa6ca1c106615da9266509 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 019/118] copilot-interpreter: Document changes in CHANGELOG. Refs #745. --- copilot-interpreter/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-interpreter/CHANGELOG b/copilot-interpreter/CHANGELOG index 53984488e..d97f4575e 100644 --- a/copilot-interpreter/CHANGELOG +++ b/copilot-interpreter/CHANGELOG @@ -1,3 +1,6 @@ +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) From f45759c245e82df5095071acf926b41bf046f514 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 020/118] copilot-theorem: Document changes in CHANGELOG. Refs #745. --- copilot-theorem/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index fd4dea25b..ec8dafd5a 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,4 +1,5 @@ -2026-06-09 +2026-07-07 + * Version bump (4.8). (#745) * Extend range of versions of Kind2. (#734) 2026-05-07 From d67b8c87f752bc326d270801cad35c3afdde1ac7 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 021/118] copilot-language: Document changes in CHANGELOG. Refs #745. --- copilot-language/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-language/CHANGELOG b/copilot-language/CHANGELOG index 069d20f5d..b162f316a 100644 --- a/copilot-language/CHANGELOG +++ b/copilot-language/CHANGELOG @@ -1,3 +1,6 @@ +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) From 2fddcea36646277ce88ce1f1719144156019b64e Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 022/118] copilot-libraries: Document changes in CHANGELOG. Refs #745. --- copilot-libraries/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG index 19b510a63..b09286048 100644 --- a/copilot-libraries/CHANGELOG +++ b/copilot-libraries/CHANGELOG @@ -1,3 +1,6 @@ +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) * Add stream analysis module. (#726) From d081479e1d86a9fc7479cb233d5c2b84b2c3ff17 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 023/118] copilot-verifier: Document changes in CHANGELOG. Refs #745. --- copilot-verifier/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-verifier/CHANGELOG b/copilot-verifier/CHANGELOG index a2b4dd530..81d2534f7 100644 --- a/copilot-verifier/CHANGELOG +++ b/copilot-verifier/CHANGELOG @@ -1,3 +1,6 @@ +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) From 8d17366634029cb76a13d0a42f0622cf168a9192 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 024/118] copilot-visualizer: Document changes in CHANGELOG. Refs #745. --- copilot-visualizer/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-visualizer/CHANGELOG b/copilot-visualizer/CHANGELOG index 0735d51ab..e4a74c508 100644 --- a/copilot-visualizer/CHANGELOG +++ b/copilot-visualizer/CHANGELOG @@ -1,3 +1,6 @@ +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) From 88a6761537c5d7ae0b0efcd48e6ce59bcae22788 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 025/118] copilot: Document changes in CHANGELOG. Refs #745. --- copilot/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index f58dd30e6..f46d51f91 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,3 +1,6 @@ +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) From ab2f6a50d4e9ef08e0f27d03275cacb329051f8f Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 22:41:08 -0700 Subject: [PATCH 026/118] copilot: Disable secure mode in Cabal in Travis CI. Refs #753. CI is failing during the Haskell setup step with the following error: ``` /root.json does not have enough signatures signed with the appropriate keys ``` It is possible to circumvent this error by configuring Cabal to not operate in secure mode. This commit modifies the Travis CI script to disable secure mode when connecting to Hackage. To be able to modify the settings for that repository, we first have Cabal create a default configuration file. --- .travis.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.travis.yml b/.travis.yml index c7c69118d..f157c7aa8 100644 --- a/.travis.yml +++ b/.travis.yml @@ -26,6 +26,8 @@ before_install: - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH - cabal --version - echo "$(ghc --version) [$(ghc --print-project-git-commit-id 2> /dev/null || echo '?')]" + - cabal user-config init + - sed -i -e "s;-- \(secure.\) True;\1 False;g" ${HOME}/.cabal/config - travis_retry cabal update - git submodule update --remote From 9d6b38cf42822ae0301e193842eb7b6184280d6c Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 8 Sep 2026 06:25:27 +0000 Subject: [PATCH 027/118] copilot: Document changes in CHANGELOG. Refs #753. --- copilot/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index f46d51f91..d497447c5 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,3 +1,6 @@ +2026-09-07 + * Disable secure mode in Cabal in Travis CI. (#753) + 2026-07-07 * Version bump (4.8). (#745) From 68c299123faeb92ece2223b90394da7ab7d03945 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 23 Aug 2026 19:02:15 +0000 Subject: [PATCH 028/118] copilot-visualizer: Fix inconsistent version bounds for `copilot` in Cabal file. Refs #749. The cabal file of `copilot-visualizer` lists inconsistent version bounds for the package `copilot`. Specifically, it depends on `copilot` versions from 4.8 to, but not including, 4.9 for the visualizer library, and from 4.7 up to, but not including, 4.8 for the `gui-example` executable. This prevents the example from being compiled against the same version of the library. This commit fixes the version bounds on `copilot` in the `gui-example` executable so that they match the version bounds applied to the `copilot-visualizer` library. --- 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 1bd88608a..4284c9886 100644 --- a/copilot-visualizer/copilot-visualizer.cabal +++ b/copilot-visualizer/copilot-visualizer.cabal @@ -121,7 +121,7 @@ executable tikz-example build-depends: base >= 4.9 && < 5, - copilot >= 4.7 && < 4.8, + copilot >= 4.8 && < 4.9, copilot-visualizer if flag(examples) From b58fab18c8065aa1311e053809d9f7befe78ab2b Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 23 Aug 2026 19:05:39 +0000 Subject: [PATCH 029/118] copilot-visualizer: Document changes in CHANGELOG. Refs #749. --- copilot-visualizer/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-visualizer/CHANGELOG b/copilot-visualizer/CHANGELOG index e4a74c508..5e16e81f4 100644 --- a/copilot-visualizer/CHANGELOG +++ b/copilot-visualizer/CHANGELOG @@ -1,3 +1,6 @@ +2026-08-23 + * Fix inconsistent version bounds for `copilot` in Cabal file. (#749) + 2026-07-07 * Version bump (4.8). (#745) From c191a7365122492eef4cfbc7ae722d76eea97cc4 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:33 -0700 Subject: [PATCH 030/118] copilot-bluespec: Replace tab in CHANGELOG. Refs #755. The CHANGELOG of the `copilot-bluespec` package contains a tab character. Per our style guide, we should not use tabs anywhere in code, READMEs or CHANGELOGs, unless strictly necessary. This commit replaces a tab in the CHANGELOG of `copilot-bluespec` with spaces. --- copilot-bluespec/CHANGELOG | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG index 1145b7a83..f47fdd362 100644 --- a/copilot-bluespec/CHANGELOG +++ b/copilot-bluespec/CHANGELOG @@ -11,7 +11,7 @@ 2026-01-07 * Version bump (4.6.1). (#705) * Disable test suite via newly added manual cabal flag. (#673) - * Fix translation of constant floating-point values. (#696) + * Fix translation of constant floating-point values. (#696) 2025-11-07 * Version bump (4.6). (#679) From 181d8033634c91cb747ef3b59c57dded2d3fbc04 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:33 -0700 Subject: [PATCH 031/118] copilot-bluespec: Document changes in CHANGELOG. Refs #755. --- copilot-bluespec/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG index f47fdd362..29e143842 100644 --- a/copilot-bluespec/CHANGELOG +++ b/copilot-bluespec/CHANGELOG @@ -1,3 +1,6 @@ +2026-08-22 + * Replace tab in CHANGELOG. (#755) + 2026-07-07 * Version bump (4.8). (#745) From ddeb5985817a0be1a75df8e9c7aa1215e4b19db1 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 30 Jul 2026 23:08:01 -0700 Subject: [PATCH 032/118] copilot-visualizer: Relax version constraints on `ogma-extra`. Refs #757. 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. The package `ogma-extra` has seen release 1.15 and will soon see release 1.16, but `copilot-visualizer` depend on versions prior to 1.13. 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 4284c9886..bb523bfc3 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.13, + ogma-extra >= 1.6.0 && < 1.17, text >= 1.2.3.1 && < 2.2, websockets >= 0.12.7 && < 0.14, From 0743773609d47c3a0070e627239c5596ccd2f2d8 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 30 Jul 2026 23:10:12 -0700 Subject: [PATCH 033/118] copilot-visualizer: Document changes in CHANGELOG. Refs #757. --- copilot-visualizer/CHANGELOG | 1 + 1 file changed, 1 insertion(+) diff --git a/copilot-visualizer/CHANGELOG b/copilot-visualizer/CHANGELOG index 5e16e81f4..5c358e534 100644 --- a/copilot-visualizer/CHANGELOG +++ b/copilot-visualizer/CHANGELOG @@ -1,5 +1,6 @@ 2026-08-23 * Fix inconsistent version bounds for `copilot` in Cabal file. (#749) + * Relax version constraints on `ogma-extra`. (#757) 2026-07-07 * Version bump (4.8). (#745) From 0f1ebfc759daaaf27a01dc3f5b4fc25cda8ddca9 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 21 Aug 2026 19:20:54 -0700 Subject: [PATCH 034/118] copilot-theorem: Remove unnecessary extension. Refs #733. The module `copilot-theorem:Copilot.Theorem.What4.Translate` enables the language extension `PatternSynonyms` unnecessarily. Nothing in the module requires that extension and it should continue to compile without it. Per our style guide to remove unused code and minimize extensions, this extension should be removed from that module. This commit removes the unnecessary extension from the `copilot-theorem:Copilot.Theorem.What4.Translate` module. --- copilot-theorem/src/Copilot/Theorem/What4/Translate.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs index cef4829ee..00edf8744 100644 --- a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs +++ b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs @@ -2,7 +2,6 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} From a26633e64929c8f19d0cb922e9acb39a07460c61 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 21 Aug 2026 20:12:01 -0700 Subject: [PATCH 035/118] copilot-theorem: Document changes in CHANGELOG. Refs #733. --- copilot-theorem/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index ec8dafd5a..140644e06 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,3 +1,6 @@ +2026-08-21 + * Remove unnecessary extension. (#733) + 2026-07-07 * Version bump (4.8). (#745) * Extend range of versions of Kind2. (#734) From 2489e6a227824dadd57bdccd9899600a1a02bf26 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:06:17 -0700 Subject: [PATCH 036/118] copilot-core: Version bump (4.8.1). Refs #760. --- 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 541cad1e3..57f92d703 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.8 +version: 4.8.1 synopsis: An intermediate representation for Copilot. description: Intermediate representation for Copilot. From 1456edb773725a174066f731f86191e672fb4b14 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:06:17 -0700 Subject: [PATCH 037/118] copilot-bluespec: Version bump (4.8.1). Refs #760. --- copilot-bluespec/copilot-bluespec.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-bluespec/copilot-bluespec.cabal b/copilot-bluespec/copilot-bluespec.cabal index 2cff39b37..e8f29e4d7 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.8 +version : 4.8.1 synopsis : A compiler for Copilot targeting FPGAs. description : This package is a back-end from Copilot to FPGAs in Bluespec. @@ -51,7 +51,7 @@ library , ieee754 >= 0.8.0 && < 0.9 , pretty >= 1.1.2 && < 1.2 - , copilot-core >= 4.8 && < 4.9 + , copilot-core >= 4.8.1 && < 4.9 , language-bluespec >= 0.1 && < 0.2 exposed-modules : Copilot.Compile.Bluespec From 2cc9ce1a0750c42e27636f032272231c32b8f99c Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:06:17 -0700 Subject: [PATCH 038/118] copilot-c99: Version bump (4.8.1). Refs #760. --- 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 d3defea3f..ea2e233dc 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.8 +version : 4.8.1 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.8 && < 4.9 + , copilot-core >= 4.8.1 && < 4.9 , language-c99 >= 0.2.0 && < 0.3 , language-c99-simple >= 0.3 && < 0.4 From 80b8ed216fd791cf4c23efd1f14affbdea5b511e Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:06:17 -0700 Subject: [PATCH 039/118] copilot-prettyprinter: Version bump (4.8.1). Refs #760. --- 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 393ae9b37..d6c2bcc11 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.8 +version: 4.8.1 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.8 && < 4.9 + copilot-core >= 4.8.1 && < 4.9 exposed-modules: From 6c233a078660e35ce9d9acc0b485b0f793430d11 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:06:17 -0700 Subject: [PATCH 040/118] copilot-interpreter: Version bump (4.8.1). Refs #760. --- 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 255d0400d..538237a10 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.8 +version: 4.8.1 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.8 && < 4.9 + copilot-core >= 4.8.1 && < 4.9 exposed-modules: From ac3e269d6669d890adf5e9a456c691d7bb3451fd Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:06:17 -0700 Subject: [PATCH 041/118] copilot-theorem: Version bump (4.8.1). Refs #760. --- 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 28127ebd0..cf3e8c44c 100644 --- a/copilot-theorem/copilot-theorem.cabal +++ b/copilot-theorem/copilot-theorem.cabal @@ -14,7 +14,7 @@ description: . -version : 4.8 +version : 4.8.1 license : BSD3 license-file : LICENSE maintainer : Ivan Perez @@ -63,8 +63,8 @@ library , transformers >= 0.5 && < 0.7 , what4 >= 1.3 && < 1.8 - , copilot-core >= 4.8 && < 4.9 - , copilot-prettyprinter >= 4.8 && < 4.9 + , copilot-core >= 4.8.1 && < 4.9 + , copilot-prettyprinter >= 4.8.1 && < 4.9 exposed-modules : Copilot.Theorem , Copilot.Theorem.Prove From 54f48abbf4de3d99c7bf7c761a56294ecde8a6ce Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:06:17 -0700 Subject: [PATCH 042/118] copilot-language: Version bump (4.8.1). Refs #760. --- 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 ca5232a8c..b30c29db6 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.8 +version: 4.8.1 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.8 && < 4.9 - , copilot-interpreter >= 4.8 && < 4.9 - , copilot-theorem >= 4.8 && < 4.9 + , copilot-core >= 4.8.1 && < 4.9 + , copilot-interpreter >= 4.8.1 && < 4.9 + , copilot-theorem >= 4.8.1 && < 4.9 exposed-modules: Copilot.Language , Copilot.Language.Operators.BitWise From 163025363de77403c37c86cbf8663d6bae22766b Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:06:17 -0700 Subject: [PATCH 043/118] copilot-libraries: Version bump (4.8.1). Refs #760. --- copilot-libraries/copilot-libraries.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-libraries/copilot-libraries.cabal b/copilot-libraries/copilot-libraries.cabal index dd96c07d4..aa5c8e61b 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.8 +version: 4.8.1 synopsis: Libraries for the Copilot language. description: Libraries for the Copilot language. @@ -41,7 +41,7 @@ library , containers >= 0.4 && < 0.9 , mtl >= 2.0 && < 2.4 , parsec >= 2.0 && < 3.2 - , copilot-language >= 4.8 && < 4.9 + , copilot-language >= 4.8.1 && < 4.9 exposed-modules: Copilot.Library.Analysis From 512df9749adaefa13cbdf61c0974775458a6d6de Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:06:17 -0700 Subject: [PATCH 044/118] copilot-verifier: Version bump (4.8.1). Refs #760. --- 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 aed3a0f10..4052ee006 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.8 +Version: 4.8.1 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.8 && < 4.9, - copilot-core >= 4.8 && < 4.9, - copilot-theorem >= 4.8 && < 4.9, + copilot-c99 >= 4.8.1 && < 4.9, + copilot-core >= 4.8.1 && < 4.9, + copilot-theorem >= 4.8.1 && < 4.9, 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.8 && < 4.9, - copilot-language >= 4.8 && < 4.9, - copilot-libraries >= 4.8 && < 4.9, - copilot-prettyprinter >= 4.8 && < 4.9, + copilot >= 4.8.1 && < 4.9, + copilot-language >= 4.8.1 && < 4.9, + copilot-libraries >= 4.8.1 && < 4.9, + copilot-prettyprinter >= 4.8.1 && < 4.9, copilot-verifier exposed-modules: Copilot.Verifier.Examples From c9b995ff5de9a0c717ee683a7016d81db47cfe5f Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:06:17 -0700 Subject: [PATCH 045/118] copilot-visualizer: Version bump (4.8.1). Refs #760. --- 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 bb523bfc3..3b1d539eb 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.8 +version: 4.8.1 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.8 && < 4.9, - copilot-core >= 4.8 && < 4.9, - copilot-interpreter >= 4.8 && < 4.9, - copilot-language >= 4.8 && < 4.9 + copilot >= 4.8.1 && < 4.9, + copilot-core >= 4.8.1 && < 4.9, + copilot-interpreter >= 4.8.1 && < 4.9, + copilot-language >= 4.8.1 && < 4.9 exposed-modules: @@ -121,7 +121,7 @@ executable tikz-example build-depends: base >= 4.9 && < 5, - copilot >= 4.8 && < 4.9, + copilot >= 4.8.1 && < 4.9, copilot-visualizer if flag(examples) From 0719333a6df5eb0414876cd9e5eb0671f87f6db9 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:06:17 -0700 Subject: [PATCH 046/118] copilot: Version bump (4.8.1). Refs #760. --- copilot/copilot.cabal | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/copilot/copilot.cabal b/copilot/copilot.cabal index 85dd95ab0..5fa90035e 100644 --- a/copilot/copilot.cabal +++ b/copilot/copilot.cabal @@ -1,5 +1,5 @@ name: copilot -version: 4.8 +version: 4.8.1 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.8 && < 4.9 - , copilot-theorem >= 4.8 && < 4.9 - , copilot-language >= 4.8 && < 4.9 - , copilot-libraries >= 4.8 && < 4.9 - , copilot-c99 >= 4.8 && < 4.9 - , copilot-prettyprinter >= 4.8 && < 4.9 + , copilot-core >= 4.8.1 && < 4.9 + , copilot-theorem >= 4.8.1 && < 4.9 + , copilot-language >= 4.8.1 && < 4.9 + , copilot-libraries >= 4.8.1 && < 4.9 + , copilot-c99 >= 4.8.1 && < 4.9 + , copilot-prettyprinter >= 4.8.1 && < 4.9 exposed-modules: Language.Copilot, Language.Copilot.Main From 69468e7f7b3b05a18faafe8822befa442d92f755 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:09:38 -0700 Subject: [PATCH 047/118] copilot-core: Document changes in CHANGELOG. Refs #760. --- copilot-core/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index e37d60585..1ccbf7db4 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,3 +1,6 @@ +2026-09-07 + * Version bump (4.8.1). (#760) + 2026-07-07 * Version bump (4.8). (#745) From a0c12ad617d16b3f6f532b9785da90ffd6d01134 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:09:38 -0700 Subject: [PATCH 048/118] copilot-bluespec: Document changes in CHANGELOG. Refs #760. --- copilot-bluespec/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG index 29e143842..3b655c5ac 100644 --- a/copilot-bluespec/CHANGELOG +++ b/copilot-bluespec/CHANGELOG @@ -1,4 +1,5 @@ -2026-08-22 +2026-09-07 + * Version bump (4.8.1). (#760) * Replace tab in CHANGELOG. (#755) 2026-07-07 From 1e8c8be5c72c5fd3f69e51a21941309fc0e4f9bd Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:09:38 -0700 Subject: [PATCH 049/118] copilot-c99: Document changes in CHANGELOG. Refs #760. --- copilot-c99/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-c99/CHANGELOG b/copilot-c99/CHANGELOG index ba43b631d..2caf70ef2 100644 --- a/copilot-c99/CHANGELOG +++ b/copilot-c99/CHANGELOG @@ -1,3 +1,6 @@ +2026-09-07 + * Version bump (4.8.1). (#760) + 2026-07-07 * Version bump (4.8). (#745) From 8f84c7646e09f5defee92f52b968db8cfe4c25fc Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:09:38 -0700 Subject: [PATCH 050/118] copilot-prettyprinter: Document changes in CHANGELOG. Refs #760. --- copilot-prettyprinter/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-prettyprinter/CHANGELOG b/copilot-prettyprinter/CHANGELOG index 7ffd6c90d..799783ce8 100644 --- a/copilot-prettyprinter/CHANGELOG +++ b/copilot-prettyprinter/CHANGELOG @@ -1,3 +1,6 @@ +2026-09-07 + * Version bump (4.8.1). (#760) + 2026-07-07 * Version bump (4.8). (#745) From 6ad1e513408324257feb1a2da43e87db074dccaf Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:09:38 -0700 Subject: [PATCH 051/118] copilot-interpreter: Document changes in CHANGELOG. Refs #760. --- copilot-interpreter/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-interpreter/CHANGELOG b/copilot-interpreter/CHANGELOG index d97f4575e..3e396d8d4 100644 --- a/copilot-interpreter/CHANGELOG +++ b/copilot-interpreter/CHANGELOG @@ -1,3 +1,6 @@ +2026-09-07 + * Version bump (4.8.1). (#760) + 2026-07-07 * Version bump (4.8). (#745) From 5659bf71213834c601e771c739164c8b2c90f307 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:09:38 -0700 Subject: [PATCH 052/118] copilot-theorem: Document changes in CHANGELOG. Refs #760. --- copilot-theorem/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index 140644e06..251b49484 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,4 +1,5 @@ -2026-08-21 +2026-09-07 + * Version bump (4.8.1). (#760) * Remove unnecessary extension. (#733) 2026-07-07 From 3f21a9b5ef73203a3f53b7f943e0195f5792dfc8 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:09:38 -0700 Subject: [PATCH 053/118] copilot-language: Document changes in CHANGELOG. Refs #760. --- copilot-language/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-language/CHANGELOG b/copilot-language/CHANGELOG index b162f316a..49162ceb0 100644 --- a/copilot-language/CHANGELOG +++ b/copilot-language/CHANGELOG @@ -1,3 +1,6 @@ +2026-09-07 + * Version bump (4.8.1). (#760) + 2026-07-07 * Version bump (4.8). (#745) From 2dee7e0dd00a063cce8a6338e9f696581131da3e Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:09:38 -0700 Subject: [PATCH 054/118] copilot-libraries: Document changes in CHANGELOG. Refs #760. --- copilot-libraries/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG index b09286048..0e8dcc83f 100644 --- a/copilot-libraries/CHANGELOG +++ b/copilot-libraries/CHANGELOG @@ -1,3 +1,6 @@ +2026-09-07 + * Version bump (4.8.1). (#760) + 2026-07-07 * Version bump (4.8). (#745) From 0206d92bc80463455a973ee57654ecf8dad1d2a0 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:09:38 -0700 Subject: [PATCH 055/118] copilot-verifier: Document changes in CHANGELOG. Refs #760. --- copilot-verifier/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-verifier/CHANGELOG b/copilot-verifier/CHANGELOG index 81d2534f7..1dec1cfd0 100644 --- a/copilot-verifier/CHANGELOG +++ b/copilot-verifier/CHANGELOG @@ -1,3 +1,6 @@ +2026-09-07 + * Version bump (4.8.1). (#760) + 2026-07-07 * Version bump (4.8). (#745) From 5ce32a8d4c0b9a968c284c325e16b30872cc2985 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:09:38 -0700 Subject: [PATCH 056/118] copilot-visualizer: Document changes in CHANGELOG. Refs #760. --- copilot-visualizer/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-visualizer/CHANGELOG b/copilot-visualizer/CHANGELOG index 5c358e534..9d772eca0 100644 --- a/copilot-visualizer/CHANGELOG +++ b/copilot-visualizer/CHANGELOG @@ -1,4 +1,5 @@ -2026-08-23 +2026-09-07 + * Version bump (4.8.1). (#760) * Fix inconsistent version bounds for `copilot` in Cabal file. (#749) * Relax version constraints on `ogma-extra`. (#757) From 1f26417f9a83d12f1d0236ffa4dce5c7907506eb Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 7 Sep 2026 10:09:38 -0700 Subject: [PATCH 057/118] copilot: Document changes in CHANGELOG. Refs #760. --- copilot/CHANGELOG | 1 + 1 file changed, 1 insertion(+) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index d497447c5..a838b070a 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,4 +1,5 @@ 2026-09-07 + * Version bump (4.8.1). (#760) * Disable secure mode in Cabal in Travis CI. (#753) 2026-07-07 From 06c31d052cdbc4be7507b9b041b48ecdbb6354b4 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 11 Oct 2026 08:38:45 -0700 Subject: [PATCH 058/118] copilot-core: Force evaluation of `Proxy` value in `Copilot.Core.Type.Array`. Refs #767. The module `copilot-core:Copilot.Core.Type.Array` achieves less than full coverage in the two of the three main categories used by `hpc`, namely "Top Level Definitions" and "Expressions". For the former, only 4 out of 6 definitions are covered, and for the latter, only 47 out of 48. To make Copilot ready for use in future missions, we want to achieve maximum coverage possible. The lower coverage of "Expressions" is due to a `Proxy` value not being forced in a call to `natVal`, which only needs the type-level information for the `Proxy` being provided. This commit modifies the code of `copilot-core:Copilot.Core.Type.Array` to force the evaluation of a `Proxy` value being passed to `natVal`. Specifically, it uses `($!)`, which achieves the evaluation of the value at the point where it is being used, making `hpc` mark it as evaluated. Other alternatives (e.g., use of `seq`, use of `Proxy#`) either do not achieve the desired effect or require more extensive changes and the use of language extensions. --- copilot-core/src/Copilot/Core/Type/Array.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot-core/src/Copilot/Core/Type/Array.hs b/copilot-core/src/Copilot/Core/Type/Array.hs index b11e8949b..07c10ba31 100644 --- a/copilot-core/src/Copilot/Core/Type/Array.hs +++ b/copilot-core/src/Copilot/Core/Type/Array.hs @@ -37,7 +37,7 @@ array xs | datalen == typelen = Array xs | otherwise = error errmsg where datalen = length xs - typelen = fromIntegral $ natVal (Proxy :: Proxy n) + typelen = fromIntegral $ natVal $! (Proxy :: Proxy n) errmsg = "Length of data (" ++ show datalen ++ ") does not match length of type (" ++ show typelen ++ ")." From fa1d30a20a222d551c37a22be7203f71c2a1263e Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 11 Oct 2026 08:39:08 -0700 Subject: [PATCH 059/118] copilot-core: Test default functions in `Show` instance for `Array`. Refs #767. The module `copilot-core:Copilot.Core.Type.Array` achieves less than full coverage in the two of the three main categories used by `hpc`, namely "Top Level Definitions" and "Expressions". For the former, only 4 out of 6 definitions are covered, and for the latter, only 47 out of 48. To make Copilot ready for use in future missions, we want to achieve maximum coverage possible. The module `copilot-core:Copilot.Core.Type.Array` includes an instance of the class `Show` for the type `Array`. That instance implicitly declares `showList` and `showsPrec`, set to their default values per the class definition. However, there is no guarantee that the definitions are correct for this specific instance, and `hpc` marks them as not covered unless we explicitly test them, affecting the "Top Level Definitions" score for this library. This commit adds two tests for functions that are implicitly set to their default definitions in the `Show` instance for `Array`. --- .../tests/Test/Copilot/Core/Type/Array.hs | 20 +++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/copilot-core/tests/Test/Copilot/Core/Type/Array.hs b/copilot-core/tests/Test/Copilot/Core/Type/Array.hs index e070f138b..0af0ffae9 100644 --- a/copilot-core/tests/Test/Copilot/Core/Type/Array.hs +++ b/copilot-core/tests/Test/Copilot/Core/Type/Array.hs @@ -11,8 +11,9 @@ import Test.Framework (Test, testGroup) import Test.Framework.Providers.QuickCheck2 (testProperty) import Test.QuickCheck (Gen, Property, arbitrary, chooseInt, expectFailure, forAll, - getNegative, getNonNegative, oneof, - property, vector, vectorOf) + getNegative, getNonNegative, + listOf, oneof, property, vector, + vectorOf) -- Internal imports: library modules being tested import Copilot.Core.Type.Array (Array, array, arrayElems, arrayUpdate) @@ -31,6 +32,10 @@ tests = testArrayElemsFail , testProperty "Show for arrays" testShowArray + , testProperty "showsPrec for arrays" + testShowsPrecArray + , testProperty "showList for arrays" + testShowListArray , testProperty "arrayElems (arrayUpdate x i v) !! i == v" (testArrayUpdateElem (Proxy :: Proxy 5)) , testProperty "arrayUpdate x i ((arrayElems x) !! i) == x" @@ -70,6 +75,17 @@ testShowArray :: Property testShowArray = forAll (vector 3) $ \l -> property $ show (array l :: Array 3 Int64) == show (l :: [Int64]) +-- | Test 'Show.showsPrec' for 'Array's. +testShowsPrecArray :: Property +testShowsPrecArray = forAll (getNonNegative <$> arbitrary) $ \prec -> + forAll (vector 3) $ \l -> property $ + showsPrec prec (array l :: Array 3 Int64) "" == show (l :: [Int64]) + +-- | Test 'Show.showList' for 'Array's. +testShowListArray :: Property +testShowListArray = forAll (listOf $ vector 3) $ \l -> property $ + showList (map array l :: [Array 3 Int64]) "" == show (l :: [[Int64]]) + -- | Test that updating an array updates the element appropriately (if we -- project that element we get the value we put in). testArrayUpdateElem :: forall n . KnownNat n => Proxy n -> Property From 34cc90741e8b792d8f55ad7e875a3bdcffe4a122 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 11 Oct 2026 17:16:56 -0700 Subject: [PATCH 060/118] copilot-core: Document changes in CHANGELOG. Refs #767. --- copilot-core/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index 1ccbf7db4..33cf7c007 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,3 +1,6 @@ +2026-10-11 + * Increase test coverage for `Copilot.Core.Type.Array`. (#767) + 2026-09-07 * Version bump (4.8.1). (#760) From ae91b9ad23ddf0f9313ae9f6e3f5d9352969dfb6 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 09:08:19 -0700 Subject: [PATCH 061/118] copilot-core: Fix errors in the documentation of `Copilot.Core.Spec`. Refs #769. The Haddock documentation associated to the type `copilot-core:Copilot.Core.Spec.Stream` contains two grammatical errors. The first is the incorrect use of "in" in the sentence "A stream in an infinite succession of values", which causes the sentence to have no verb, and the second is the use of `Stream` in the second paragraph with no article. To make documentation most useful and in compliance with our style guide, the documentation should have no typos or grammatical errors. This commit fixes both grammatical errors in the documentation of `copilot-core:Copilot.Core.Spec.Stream`, as well as a grammatical error in the top-level documentation of the same module. --- copilot-core/src/Copilot/Core/Spec.hs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/copilot-core/src/Copilot/Core/Spec.hs b/copilot-core/src/Copilot/Core/Spec.hs index 6614d0621..e8972c928 100644 --- a/copilot-core/src/Copilot/Core/Spec.hs +++ b/copilot-core/src/Copilot/Core/Spec.hs @@ -11,9 +11,9 @@ -- and their handling functions, or streams to observe, or a theorem that must -- be proved. -- --- In order to be executed, high-level Copilot Language Spec must be turned --- into Copilot Core's 'Spec'. This module defines the low-level Copilot Core --- representations for Specs and the main types of element in a spec. +-- In order to be executed, a high-level Copilot Language @Spec@ must be +-- turned into a Copilot Core 'Spec'. This module defines the low-level Copilot +-- Core representation for 'Spec' and the main types of element in a spec. module Copilot.Core.Spec ( Stream (..) , Observer (..) @@ -32,9 +32,9 @@ import Data.Typeable (Typeable) import Copilot.Core.Expr (Expr, Id, Name, UExpr) import Copilot.Core.Type (Type, Typed) --- | A stream in an infinite succession of values of the same type. +-- | A stream is an infinite succession of values of the same type. -- --- Stream can carry different types of data. Boolean streams play a special +-- Streams can carry different types of data. Boolean streams play a special -- role: they are used by other parts (e.g., 'Trigger') to detect when the -- properties being monitored are violated. data Stream = forall a . (Typeable a, Typed a) => Stream From ae2dfdb87f54b2288b5e95147830a203bf344382 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 09:09:50 -0700 Subject: [PATCH 062/118] copilot-core: Document changes in CHANGELOG. Refs #769. --- copilot-core/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index 33cf7c007..9e45e6c5b 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,5 +1,6 @@ -2026-10-11 +2026-10-12 * Increase test coverage for `Copilot.Core.Type.Array`. (#767) + * Fix errors in the documentation of `Copilot.Core.Spec`. (#769) 2026-09-07 * Version bump (4.8.1). (#760) From d567a73e4f00f126b9ed49b7b6065240fa120014 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 10:12:14 -0700 Subject: [PATCH 063/118] copilot-core: Replace tab in CHANGELOG. Refs #772. Several files across the codebase contain tabs, including the `DESIGN.md` file in `copilot-bluespec`, the `CHANGELOG` for `copilot-core`, and the `Eval` module in `copilot-interpreter`. Per our style guide, we should not use tabs anywhere in code, READMEs or CHANGELOGs, unless strictly necessary. This commit replaces a tab in the CHANGELOG of `copilot-core` with spaces. --- copilot-core/CHANGELOG | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index 9e45e6c5b..755a52efa 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,5 +1,5 @@ 2026-10-12 - * Increase test coverage for `Copilot.Core.Type.Array`. (#767) + * Increase test coverage for `Copilot.Core.Type.Array`. (#767) * Fix errors in the documentation of `Copilot.Core.Spec`. (#769) 2026-09-07 From 8f59941cd05980f4c9f4cf8ae77e821e5e1cb03e Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 10:13:31 -0700 Subject: [PATCH 064/118] copilot-bluespec: Replace tabs in `DESIGN.md`. Refs #772. Several files across the codebase contain tabs, including the `DESIGN.md` file in `copilot-bluespec`, the `CHANGELOG` for `copilot-core`, and the `Eval` module in `copilot-interpreter`. Per our style guide, we should not use tabs anywhere in code, READMEs or CHANGELOGs, unless strictly necessary. This commit replaces tabs in the `DESIGN.md` document of `copilot-bluespec` with spaces. --- copilot-bluespec/DESIGN.md | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/copilot-bluespec/DESIGN.md b/copilot-bluespec/DESIGN.md index b5a07dd31..6cf5cd610 100644 --- a/copilot-bluespec/DESIGN.md +++ b/copilot-bluespec/DESIGN.md @@ -418,15 +418,15 @@ This generates a Verilog module `mkFibs.v` that looks like the following: ```verilog module mkFibs(CLK, - RST_N, + RST_N, - even_guard, + even_guard, - even_arg0, + even_arg0, - odd_guard, + odd_guard, - odd_arg0); + odd_arg0); input CLK; input RST_N; @@ -815,17 +815,17 @@ that looks like the following: ```verilog module mkFibs(CLK, - RST_N, + RST_N, - even_guard, + even_guard, - even_arg0, + even_arg0, - odd_guard, + odd_guard, - odd_arg0, + odd_arg0, - fibs); + fibs); input CLK; input RST_N; From de586c06d696053c7d7e5fdd70d99a220aac32c8 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 10:12:42 -0700 Subject: [PATCH 065/118] copilot-interpreter: Replace tab in `Copilot.Interpret.Eval`. Refs #772. Several files across the codebase contain tabs, including the `DESIGN.md` file in `copilot-bluespec`, the `CHANGELOG` for `copilot-core`, and the `Eval` module in `copilot-interpreter`. Per our style guide, we should not use tabs anywhere in code, READMEs or CHANGELOGs, unless strictly necessary. This commit replaces a tab in the module `copilot-interpreter:Copilot.Interpret.Eval` with spaces. --- copilot-interpreter/src/Copilot/Interpret/Eval.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot-interpreter/src/Copilot/Interpret/Eval.hs b/copilot-interpreter/src/Copilot/Interpret/Eval.hs index 462b5853e..9543806c9 100644 --- a/copilot-interpreter/src/Copilot/Interpret/Eval.hs +++ b/copilot-interpreter/src/Copilot/Interpret/Eval.hs @@ -19,7 +19,7 @@ module Copilot.Interpret.Eval import Copilot.Core (Expr (..), Field (..), Id, Name, Observer (..), Op1 (..), Op2 (..), Op3 (..), Spec, Stream (..), Trigger (..), Type (..), UExpr (..), Value (..), - arrayElems, arrayUpdate, specObservers, + arrayElems, arrayUpdate, specObservers, specStreams, specTriggers, updateField) import Copilot.Interpret.Error (badUsage) From 9835d834d41bdcea5abc4f83c214af88635c8e0a Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 10:33:19 -0700 Subject: [PATCH 066/118] copilot-core: Document changes in CHANGELOG. Refs #772. --- copilot-core/CHANGELOG | 1 + 1 file changed, 1 insertion(+) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index 755a52efa..8ffeafc40 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,6 +1,7 @@ 2026-10-12 * Increase test coverage for `Copilot.Core.Type.Array`. (#767) * Fix errors in the documentation of `Copilot.Core.Spec`. (#769) + * Replace tab in CHANGELOG. (#772) 2026-09-07 * Version bump (4.8.1). (#760) From 1e34f7b0f1e7aadff87c5f77f8ef5042c3e70930 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 10:33:30 -0700 Subject: [PATCH 067/118] copilot-bluespec: Document changes in CHANGELOG. Refs #772. --- copilot-bluespec/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG index 3b655c5ac..aa122183f 100644 --- a/copilot-bluespec/CHANGELOG +++ b/copilot-bluespec/CHANGELOG @@ -1,3 +1,6 @@ +2026-10-12 + * Replace tabs in `DESIGN.md`. (#772) + 2026-09-07 * Version bump (4.8.1). (#760) * Replace tab in CHANGELOG. (#755) From d00808a471e635c470444edcaaa89478ee9fb0c9 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 10:33:39 -0700 Subject: [PATCH 068/118] copilot-interpreter: Document changes in CHANGELOG. Refs #772. --- copilot-interpreter/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-interpreter/CHANGELOG b/copilot-interpreter/CHANGELOG index 3e396d8d4..1b88d8eb7 100644 --- a/copilot-interpreter/CHANGELOG +++ b/copilot-interpreter/CHANGELOG @@ -1,3 +1,6 @@ +2026-10-12 + * Replace tab in `Copilot.Interpreter.Eval`. (#772) + 2026-09-07 * Version bump (4.8.1). (#760) From cfb8974ddb668f047b026241faa50011ed2c5411 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 10:18:43 -0700 Subject: [PATCH 069/118] copilot: Adjust Travis CI script to flag presence of tabs as an error. Refs #774. The current CI settings do not detect if tabs have been introduced in source code, documentation or CHANGELOGs. That lack of automation makes the accidental introduction of tabs in the code more likely, especially by new users who have not yet configured their editor to replace tabs with spaces. To facilitate keeping Copilot conformant with the style guide, we want to automatically detect when tabs are introduced and warn users accordingly. This commit modifies the Travis CI script to stop with an error if any code, Cabal files, documentation or CHANGELOGs contain any tabs. --- .travis.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.travis.yml b/.travis.yml index f157c7aa8..de3f14bb5 100644 --- a/.travis.yml +++ b/.travis.yml @@ -32,6 +32,9 @@ before_install: - git submodule update --remote script: + # Fail if the code, Cabal files, documentation or CHANGELOGs contain tabs. + - if grep -rP '\t' --include='*.hs' --include='*.cabal' --include='*.md' --include='CHANGELOG' . ; then exit 1; fi + # We explicitly install all libraries so that they are exposed and we can use # them for tests (e.g., with runhaskell). There is no harm in doing this # instead of installing just copilot. From 74a4e39b4e258767a9cea632b0b72e14c44319ee Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 10:34:18 -0700 Subject: [PATCH 070/118] copilot: Document changes in CHANGELOG. Refs #774. --- copilot/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index a838b070a..e7b1e3700 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,3 +1,6 @@ +2026-10-12 + * Adjust Travis CI script to flag presence of tabs as an error. (#774) + 2026-09-07 * Version bump (4.8.1). (#760) * Disable secure mode in Cabal in Travis CI. (#753) From 73c31d9de618cb99dd0dfafb47b9db34fec02fa7 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 13:54:30 -0700 Subject: [PATCH 071/118] copilot-bluespec: Remove trailing spaces. Refs #775. The module `copilot-bluespec:Copilot.Compile.Bluespec.Expr` contains trailing spaces. It's best to remove them, since those are automatically removed by many editors, leading to PRs containing changes unrelated to the main issues being addressed. In compliance with our coding standard, trailing space should be removed. This commit removes all trailing spaces from `copilot-bluespec:Copilot.Compile.Bluespec.Expr`. --- .../src/Copilot/Compile/Bluespec/Expr.hs | 46 +++++++++---------- 1 file changed, 23 insertions(+), 23 deletions(-) diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs index 2b71b3957..84a9ffe7a 100644 --- a/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs +++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs @@ -627,43 +627,43 @@ constInt ty i -- | Translate a Copilot floating-point literal into a Bluespec expression. constFP :: Type ty -> Double -> BS.CExpr constFP ty d - -- Bluespec internally represents all IEEE floating-point values as structs + -- Bluespec internally represents all IEEE floating-point values as structs -- so special symbols have to be called for constructing special values, -- e.g. NaN, inf, and -0.0. See -- https://github.com/B-Lang-org/bsc/blob/main/src/Libraries/Base3-Math/FloatingPoint.bsv#L441 - | isInfinite d = BS.CApply - (BS.CVar $ BS.mkId BS.NoPos "infinity") + | isInfinite d = BS.CApply + (BS.CVar $ BS.mkId BS.NoPos "infinity") [ if d < 0 - then BS.CCon BS.idTrue [] + then BS.CCon BS.idTrue [] else BS.CCon BS.idFalse [] ] - - | isNaN d = let - cexpr = BS.CHasType + + | isNaN d = let + cexpr = BS.CHasType ( BS.CLit $ BS.CLiteral BS.NoPos $ BS.LInt $ BS.IntLit Nothing 10 cval ) - ( BS.CQType [] $ BS.TCon $ - BS.TyCon - (BS.mkId BS.NoPos ctype) - Nothing + ( BS.CQType [] $ BS.TCon $ + BS.TyCon + (BS.mkId BS.NoPos ctype) + Nothing BS.TIabstract ) - cval = case ty of - Float -> fromIntegral $ + cval = case ty of + Float -> fromIntegral $ castFloatToWord32 $ uncastDoubleNaNToFloat d - Double -> fromIntegral $ + Double -> fromIntegral $ castDoubleToWord64 d _ -> impossible "constFP" "copilot-bluespec" - ctype = case ty of + ctype = case ty of Float -> "Bit 32" Double -> "Bit 64" _ -> impossible "constFP" "copilot-bluespec" in BS.CApply (BS.CVar $ BS.mkId BS.NoPos "unpack") [cexpr] - | d == 0 = BS.CApply - (BS.CVar $ BS.mkId BS.NoPos "zero") - [ if isNegativeZero d - then BS.CCon BS.idTrue [] + | d == 0 = BS.CApply + (BS.CVar $ BS.mkId BS.NoPos "zero") + [ if isNegativeZero d + then BS.CCon BS.idTrue [] else BS.CCon BS.idFalse [] ] | d > 0 = withTypeAnnotation ty $ cLit $ BS.LReal d @@ -676,13 +676,13 @@ constFP ty d [cLit $ BS.LReal $ negate d] -- Because NaNs are specially placed as bit-representations by `constfp` and `constfp` requires Doubles as inputs, --- we need to convert NaN doubles safely into NaN floats. GHC Double2Float does not preserve signal nor payload +-- we need to convert NaN doubles safely into NaN floats. GHC Double2Float does not preserve signal nor payload -- internals of NaNs so in this case we need a special conversion. uncastDoubleNaNToFloat :: Double -> Float -uncastDoubleNaNToFloat nan = if (isSignaling nan) - then (setPayloadSignaling payload) +uncastDoubleNaNToFloat nan = if (isSignaling nan) + then (setPayloadSignaling payload) else (setPayload payload) - where + where payload = double2Float $ getPayload nan -- | Create a Bluespec expression consisting of a literal. From 78cdf022d05c422358782bcf19fe210d5d69188b Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 14:04:03 -0700 Subject: [PATCH 072/118] copilot-bluespec: Document changes in CHANGELOG. Refs #775. --- copilot-bluespec/CHANGELOG | 1 + 1 file changed, 1 insertion(+) diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG index aa122183f..b3cc16e04 100644 --- a/copilot-bluespec/CHANGELOG +++ b/copilot-bluespec/CHANGELOG @@ -1,5 +1,6 @@ 2026-10-12 * Replace tabs in `DESIGN.md`. (#772) + * Remove trailing spaces. (#775) 2026-09-07 * Version bump (4.8.1). (#760) From 64912e909a1023d252e2196eba881fd1e66907dc Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 18:29:33 -0700 Subject: [PATCH 073/118] copilot: Adjust Travis CI script to flag trailing space as an error. Refs #777. The current CI settings do not detect if trailing space has been introduced in source code, documentation or CHANGELOGs. That lack of automation makes the accidental introduction of trailing space in the code more likely, especially by new users who have not yet configured their editor to automatically remove trailing spaces. To facilitate keeping Copilot conformant with the style guide, we want to automatically detect when trailing spaces are introduced and warn users accordingly. This commit modifies the Travis CI script to stop with an error if any non-binary files contain any trailing spaces. --- .travis.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.travis.yml b/.travis.yml index de3f14bb5..6cf023165 100644 --- a/.travis.yml +++ b/.travis.yml @@ -32,6 +32,9 @@ before_install: - git submodule update --remote script: + # Fail if the any non-binary files contain trailing spaces. + - if grep -nIHre ' \+$' * ; then exit 1; fi + # Fail if the code, Cabal files, documentation or CHANGELOGs contain tabs. - if grep -rP '\t' --include='*.hs' --include='*.cabal' --include='*.md' --include='CHANGELOG' . ; then exit 1; fi From 177982b2d4cd653774ceb8fae714126f6a4ce3c9 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 18:32:05 -0700 Subject: [PATCH 074/118] copilot: Document changes in CHANGELOG. Refs #777. --- copilot/CHANGELOG | 1 + 1 file changed, 1 insertion(+) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index e7b1e3700..f28d79c55 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,5 +1,6 @@ 2026-10-12 * Adjust Travis CI script to flag presence of tabs as an error. (#774) + * Adjust Travis CI script to flag trailing space as an error. (#777) 2026-09-07 * Version bump (4.8.1). (#760) From 2a04a921cff2f492323512fbd9bf6ade6172a7af Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 15 Oct 2026 22:14:33 -0700 Subject: [PATCH 075/118] copilot: Use "into" instead of "in" when indicating movement in README. Refs #779. The README contains several typos, missing commas, issues with capitalization, and poor wording in some sentences. For example, Copilot is written as `Copilot` in some places, but `copilot` in others, even when referring to the project (as opposed to the library). The sentence "It read temperature as a byte", which accompanies a code example, is grammatically incorrect. To make the README useful and easy to read, we should fix all syntactic and grammatical errors wherever possible. This commit replaces a use of "in" with "into" after a verb that denotes movement or change with direction, which improves the style of the sentence. --- copilot/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot/README.md b/copilot/README.md index 893d6a933..a1f7fd875 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -7,7 +7,7 @@ Copilot is a runtime verification framework for hard real-time systems. Programs can be interpreted for testing, or translated into C99 code to be -incorporated in a project or standalone application. The C99 code generated +incorporated into a project or standalone application. The C99 code generated is constant in memory and time, making it suitable for systems with hard real-time requirements. From e76d6534a876d71075d885678c019bf6d2f7cd93 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 15 Oct 2026 22:13:31 -0700 Subject: [PATCH 076/118] copilot: Add missing article in README. Refs #779. The README contains several typos, missing commas, issues with capitalization, and poor wording in some sentences. For example, Copilot is written as `Copilot` in some places, but `copilot` in others, even when referring to the project (as opposed to the library). The sentence "It read temperature as a byte", which accompanies a code example, is grammatically incorrect. To make the README useful and easy to read, we should fix all syntactic and grammatical errors wherever possible. This commit adds a missing article in a sentence, part of the list of features of Copilot, which is grammatically more correct and reads better. --- copilot/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot/README.md b/copilot/README.md index a1f7fd875..2d8d4ed5a 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -26,7 +26,7 @@ real-time requirements. - Produce hard real-time C99 runtime monitors that run in constant memory and time. -- Catch errors in specifications early using expressive static type system. +- Catch errors in specifications early using an expressive static type system. - Prove properties about specifications using theorem proving extensions. From e351df801b08221074bb0a65d407b279c86b4faf Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 15 Oct 2026 22:14:49 -0700 Subject: [PATCH 077/118] copilot: Add missing comma in README. Refs #779. The README contains several typos, missing commas, issues with capitalization, and poor wording in some sentences. For example, Copilot is written as `Copilot` in some places, but `copilot` in others, even when referring to the project (as opposed to the library). The sentence "It read temperature as a byte", which accompanies a code example, is grammatically incorrect. To make the README useful and easy to read, we should fix all syntactic and grammatical errors wherever possible. This commit adds a comma after the introductory phrase "to use Copilot". --- copilot/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot/README.md b/copilot/README.md index 2d8d4ed5a..49bb8358c 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -98,7 +98,7 @@ ghci> ghci> Leaving GHCi. ### Other Linux distributions On other Linux distributions or older Debian-based distributions, to use -Copilot you must install a Haskell compiler (GHC) and the package manager +Copilot, you must install a Haskell compiler (GHC) and the package manager Cabal. We currently support all versions of GHC from 8.6.5 to modern versions (9.10 as of this writing). You can install the toolchain using [ghcup](https://www.haskell.org/ghcup/) or, if you are on Debian/Ubuntu, From 73a3444671661c9e83410f8c18aab671c55421ed Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 15 Oct 2026 22:14:58 -0700 Subject: [PATCH 078/118] copilot: Add missing comma in README. Refs #779. The README contains several typos, missing commas, issues with capitalization, and poor wording in some sentences. For example, Copilot is written as `Copilot` in some places, but `copilot` in others, even when referring to the project (as opposed to the library). The sentence "It read temperature as a byte", which accompanies a code example, is grammatically incorrect. To make the README useful and easy to read, we should fix all syntactic and grammatical errors wherever possible. This commit adds a comma after the introductory phrase "To use Copilot". --- copilot/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot/README.md b/copilot/README.md index 49bb8358c..0cebe449d 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -129,7 +129,7 @@ ghci> ghci> Leaving GHCi. ## Mac installation [(Back to top)](#table-of-contents) -To use Copilot you must have a Haskell compiler (GHC) and the package manager +To use Copilot, you must have a Haskell compiler (GHC) and the package manager Cabal. We currently support all versions of GHC from 8.6.5 to modern versions (9.6 as of this writing). You can install the toolchain using [ghcup](https://www.haskell.org/ghcup/), as well as with Homebrew: From c05161555f1714d1d913ebabde3e87c1373c75fb Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 14 Oct 2026 20:21:00 -0700 Subject: [PATCH 079/118] copilot: Fix spelling of Travis CI in README. Refs #779. The README contains several typos, missing commas, issues with capitalization, and poor wording in some sentences. For example, Copilot is written as `Copilot` in some places, but `copilot` in others, even when referring to the project (as opposed to the library). The sentence "It read temperature as a byte", which accompanies a code example, is grammatically incorrect. To make the README useful and easy to read, we should fix all syntactic and grammatical errors wherever possible. This commit fixes the spelling of "Travis CI". --- copilot/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot/README.md b/copilot/README.md index 0cebe449d..03ffcf650 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -162,7 +162,7 @@ ghci> ghci> Leaving GHCi. Feel free to open an issue if you are unable to install Copilot following these instructions. -There is a TravisCI file at the root of the repository that may help with +There is a Travis CI file at the root of the repository that may help with troubleshooting the installation. Our issues often include comments with Dockerfiles listing the steps necessary to install Copilot from scratch. From cc42fd662cd6a423f37ffadd892d9c349e5dad5d Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 15 Oct 2026 22:13:37 -0700 Subject: [PATCH 080/118] copilot: Fix discrepancy between pronoun and verb in README. Refs #779. The README contains several typos, missing commas, issues with capitalization, and poor wording in some sentences. For example, Copilot is written as `Copilot` in some places, but `copilot` in others, even when referring to the project (as opposed to the library). The sentence "It read temperature as a byte", which accompanies a code example, is grammatically incorrect. To make the README useful and easy to read, we should fix all syntactic and grammatical errors wherever possible. This commit fixes a discrepancy between the number of the pronoun in a sentence ("It") and the verb ("read"). It also adds an article accmpanying temperature, since there is no marker suggesting it refers specifically to the global C variable by that name. --- copilot/README.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/copilot/README.md b/copilot/README.md index 03ffcf650..ec2c3723b 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -176,8 +176,9 @@ of the main repository. ```haskell -- This example implements a simple home heating system. The system heats --- when the temperature gets too low, and stops when it is high enough. It read --- temperature as a byte (range -50C to 100C) and translates this to Celsius. +-- when the temperature gets too low, and stops when it is high enough. It +-- reads the temperature as a byte (range -50C to 100C) and translates it to +-- Celsius. module Heater where From f32cf04d3e4b9af0ea875c1402b476061143aaa2 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 15 Oct 2026 22:18:34 -0700 Subject: [PATCH 081/118] copilot: Fix capitalization of Copilot in README. Refs #779. The README contains several typos, missing commas, issues with capitalization, and poor wording in some sentences. For example, Copilot is written as `Copilot` in some places, but `copilot` in others, even when referring to the project (as opposed to the library). The sentence "It read temperature as a byte", which accompanies a code example, is grammatically incorrect. To make the README useful and easy to read, we should fix all syntactic and grammatical errors wherever possible. This commit fixes the capitalization of Copilot referring to the project. --- copilot/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot/README.md b/copilot/README.md index ec2c3723b..66060e7ca 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -239,7 +239,7 @@ does not constitute any form of endorsement._ built using NASA's Core Flight System or the Robot Operating System (ROS 2). - [arduino-copilot](https://hackage.haskell.org/package/arduino-copilot) - facilitates building copilot applications that run on Arduino. + facilitates building Copilot applications that run on Arduino. - [sketch-frp-copilot](https://hackage.haskell.org/package/sketch-frp-copilot) extends Copilot with an FRP-like interface. From 5d879d850d14d1e8c263cffa6a2759bdd68f7a35 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 15 Oct 2026 22:18:43 -0700 Subject: [PATCH 082/118] copilot: Fix capitalization of Copilot in README. Refs #779. The README contains several typos, missing commas, issues with capitalization, and poor wording in some sentences. For example, Copilot is written as `Copilot` in some places, but `copilot` in others, even when referring to the project (as opposed to the library). The sentence "It read temperature as a byte", which accompanies a code example, is grammatically incorrect. To make the README useful and easy to read, we should fix all syntactic and grammatical errors wherever possible. This commit fixes the capitalization of Copilot referring to the project. --- copilot/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot/README.md b/copilot/README.md index 66060e7ca..7332fd7da 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -245,7 +245,7 @@ does not constitute any form of endorsement._ extends Copilot with an FRP-like interface. - [zephyr-copilot](https://hackage.haskell.org/package/zephyr-copilot) - facilitates building copilot applications that run on boards supported by the + facilitates building Copilot applications that run on boards supported by the Zephyr project. # Documentation From dc3ac33be460111f241e3bec7d3870c791f5e173 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 14 Oct 2026 20:27:36 -0700 Subject: [PATCH 083/118] copilot: Add missing comma in README. Refs #779. The README contains several typos, missing commas, issues with capitalization, and poor wording in some sentences. For example, Copilot is written as `Copilot` in some places, but `copilot` in others, even when referring to the project (as opposed to the library). The sentence "It read temperature as a byte", which accompanies a code example, is grammatically incorrect. To make the README useful and easy to read, we should fix all syntactic and grammatical errors wherever possible. This commit adds a missing comma after an introductory adverb. --- copilot/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot/README.md b/copilot/README.md index 7332fd7da..536665d87 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -391,5 +391,5 @@ https://github.com/Copilot-Language/copilot/graphs/contributors We are grateful for NASA Contract NNL08AD13T to Galois, Inc. and the National Institute of Aerospace, which partially supported this work. -Additionally NASA Langley contracts 80LARC17C0004 and NNL09AA00A supported +Additionally, NASA Langley contracts 80LARC17C0004 and NNL09AA00A supported further development of Copilot. From 12024c6efe5d80bb09d52eebfb78d23b8536a4ee Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 15 Oct 2026 22:12:30 -0700 Subject: [PATCH 084/118] copilot: Document changes in CHANGELOG. Refs #779. --- copilot/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index f28d79c55..4758ed15b 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,6 +1,7 @@ -2026-10-12 +2026-10-15 * Adjust Travis CI script to flag presence of tabs as an error. (#774) * Adjust Travis CI script to flag trailing space as an error. (#777) + * Update README to correct typos and improve readability. (#779) 2026-09-07 * Version bump (4.8.1). (#760) From 7c2cbbd99c2bf3d476c2b493f0127a61252a4566 Mon Sep 17 00:00:00 2001 From: Kaveh Zare Date: Fri, 16 Oct 2026 13:30:21 -0500 Subject: [PATCH 085/118] copilot-core: Fix comments for two tests in `Test.Copilot.Core.Type`. Refs #781. The Haddock comments that accompany the properties `testUpdateStruct` and `testUpdateStruct`, included in the test module `copilot-core:Test.Copilot.Core.Type` are incorrect. The comments indicate that the properties test showing a struct, when they are related to updates instead. All Haddock comments should correctly document the functionality implemented in Copilot. This commit fixes the Haddock comments for the aforementioned test properties. --- copilot-core/tests/Test/Copilot/Core/Type.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-core/tests/Test/Copilot/Core/Type.hs b/copilot-core/tests/Test/Copilot/Core/Type.hs index 9f9cb6d5e..128cdea67 100644 --- a/copilot-core/tests/Test/Copilot/Core/Type.hs +++ b/copilot-core/tests/Test/Copilot/Core/Type.hs @@ -350,7 +350,7 @@ testShowStruct = forAll arbitrary $ \k1 -> forAll arbitrary $ \k2 -> show (S (Field k1) (Field k2)) == "" --- | Test showing a struct. +-- | Test updating a struct. testUpdateStruct :: Property testUpdateStruct = forAll arbitrary $ \k1 -> @@ -364,7 +364,7 @@ testUpdateStruct = where unField (Field x) = x --- | Test showing a struct. +-- | Test updating a struct (should fail). testUpdateStructFail :: Property testUpdateStructFail = expectFailure $ forAll arbitrary $ \k1 -> From 54f18ef8b755704082929a374ab8700c61eaeb9c Mon Sep 17 00:00:00 2001 From: Kaveh Zare Date: Fri, 16 Oct 2026 13:35:12 -0500 Subject: [PATCH 086/118] copilot-core: Document changes in CHANGELOG. Refs #781. --- copilot-core/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index 8ffeafc40..ad519557c 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,7 +1,8 @@ -2026-10-12 +2026-10-16 * Increase test coverage for `Copilot.Core.Type.Array`. (#767) * Fix errors in the documentation of `Copilot.Core.Spec`. (#769) * Replace tab in CHANGELOG. (#772) + * Fix comments for two tests in `Test.Copilot.Core.Type`. (#781) 2026-09-07 * Version bump (4.8.1). (#760) From 570cda7fa751149911d0e69f6ab1d9a57b48ccb2 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 17 Oct 2026 08:20:18 -0700 Subject: [PATCH 087/118] copilot-core: Fix typo in Haddock comment of test property. Refs #783. The Haddock comment for the property `copilot-core:Test.Copilot.Core.Type.testTypeLength2` states that it tests "that the length of an multi-dimensional array is as expected", which is grammatically incorrect. To make documentation most useful and in compliance with our style guide, the documentation should have no typos or grammatical errors. This commit fixes the aforementioned typo. --- copilot-core/tests/Test/Copilot/Core/Type.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot-core/tests/Test/Copilot/Core/Type.hs b/copilot-core/tests/Test/Copilot/Core/Type.hs index 128cdea67..979f87d88 100644 --- a/copilot-core/tests/Test/Copilot/Core/Type.hs +++ b/copilot-core/tests/Test/Copilot/Core/Type.hs @@ -165,7 +165,7 @@ testTypeLength1 = property $ typeLength a == 3 a :: Type (Array 3 Int8) a = Array Int8 --- | Test that the length of an multi-dimensional array is as expected. +-- | Test that the length of a multi-dimensional array is as expected. testTypeLength2 :: Property testTypeLength2 = property $ typeLength a == 3 where From 7c9c43fe28bd2cf4d311547fcadf372c646f134e Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 18 Oct 2026 09:28:29 -0700 Subject: [PATCH 088/118] copilot-core: Document changes in CHANGELOG. Refs #783. --- copilot-core/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index ad519557c..b2d405f95 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,8 +1,9 @@ -2026-10-16 +2026-10-17 * Increase test coverage for `Copilot.Core.Type.Array`. (#767) * Fix errors in the documentation of `Copilot.Core.Spec`. (#769) * Replace tab in CHANGELOG. (#772) * Fix comments for two tests in `Test.Copilot.Core.Type`. (#781) + * Fix typo in Haddock comment of test property. (#783) 2026-09-07 * Version bump (4.8.1). (#760) From 6046703392ad20ea306b16ab03a7d604a68c0af6 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 17 Oct 2026 08:30:23 -0700 Subject: [PATCH 089/118] copilot-core: Fix test to use `typeSize` instead of `typeLength`. Refs #784. The test property `copilot-core:Test.Copilot.Core.Type.testTypeSize1` claims, in its name, in the Haddock comment that accompanies it, and in the property description as part of the property group, that it tests `typeSize`. However, its implementation tests `typeLength`. The property should test the function it is expected to be testing. This commit modifies `copilot-core:Test.Copilot.Core.Type.testTypeSize1` to use `typeSize` instead of `typeLength`. --- copilot-core/tests/Test/Copilot/Core/Type.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot-core/tests/Test/Copilot/Core/Type.hs b/copilot-core/tests/Test/Copilot/Core/Type.hs index 979f87d88..47d8c5940 100644 --- a/copilot-core/tests/Test/Copilot/Core/Type.hs +++ b/copilot-core/tests/Test/Copilot/Core/Type.hs @@ -174,7 +174,7 @@ testTypeLength2 = property $ typeLength a == 3 -- | Test that the size of an array is as expected. testTypeSize1 :: Property -testTypeSize1 = property $ typeLength a == 3 +testTypeSize1 = property $ typeSize a == 3 where a :: Type (Array 3 Int8) a = Array Int8 From 1aac617ad5ac27e167ff755e5905c1b0e1c507e6 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 18 Oct 2026 11:43:35 -0700 Subject: [PATCH 090/118] copilot-core: Document changes in CHANGELOG. Refs #784. --- copilot-core/CHANGELOG | 1 + 1 file changed, 1 insertion(+) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index b2d405f95..c8a3f790d 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -4,6 +4,7 @@ * Replace tab in CHANGELOG. (#772) * Fix comments for two tests in `Test.Copilot.Core.Type`. (#781) * Fix typo in Haddock comment of test property. (#783) + * Fix test to use `typeSize` instead of `typeLength` (#784). 2026-09-07 * Version bump (4.8.1). (#760) From 5c32631cb72d51ce8b91802f58b840e2f482d05f Mon Sep 17 00:00:00 2001 From: James Todd Gloyd Date: Fri, 23 Oct 2026 20:54:08 +0000 Subject: [PATCH 091/118] copilot-libraries: Add random stream generation module. Refs #766. Copilot does not currently contain any capability to produce a random stream of values. Randomization is useful for a lot of applications, from testing to fault injection. To make Copilot more versatile and useful for the use cases we want to support, we want to add a module to `copilot-libraries` with randomization primitives. This commit adds a new module that provides functions to produce random streams of different types and with different properties. --- copilot-libraries/copilot-libraries.cabal | 1 + .../src/Copilot/Library/Random.hs | 145 ++++++++++++++++++ 2 files changed, 146 insertions(+) create mode 100644 copilot-libraries/src/Copilot/Library/Random.hs diff --git a/copilot-libraries/copilot-libraries.cabal b/copilot-libraries/copilot-libraries.cabal index aa5c8e61b..b34020a57 100644 --- a/copilot-libraries/copilot-libraries.cabal +++ b/copilot-libraries/copilot-libraries.cabal @@ -51,6 +51,7 @@ library , Copilot.Library.PTLTL , Copilot.Library.StateMachines , Copilot.Library.Statistics + , Copilot.Library.Random , Copilot.Library.RegExp , Copilot.Library.Utils , Copilot.Library.Voting diff --git a/copilot-libraries/src/Copilot/Library/Random.hs b/copilot-libraries/src/Copilot/Library/Random.hs new file mode 100644 index 000000000..d4828e12b --- /dev/null +++ b/copilot-libraries/src/Copilot/Library/Random.hs @@ -0,0 +1,145 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +-- | +-- Basic pseudo-random number generation. +-- +-- Information on performance of a selection of pseudo-random number generation +-- algorithms, including those implemented below, can be found at: +-- https://prng.di.unimi.it/ +-- +-- Important: these pseudo-random number generators are NOT cryptographically +-- secure generators. +module Copilot.Library.Random + ( randomW32 + , randomW64 + , boundedRandomIntegral + , proportionalRandomBool + , weightedRandomSelection + ) + where + +-- External imports +import Copilot.Language (Array, Stream, Typed, Word32, Word64, arrayElems, + constant, mod, mux, (!), (++), (.<<.), (.>>.), (.^.), + (<), (<=)) +import GHC.TypeLits (KnownNat, type (<=)) +import Prelude hiding (mod, (++), (<), (<=)) + +-- | Given two Word32 seeds, produce a pseudo-random stream of Word32 numbers, +-- which has a period of 2^32 - 1. Neither of the seeds should be zero, since +-- the underlying randomization algorithm maps zero to itself. +-- +-- This function uses an Xorshift+ algorithm. +randomW32 :: Word32 -> Word32 -> Stream Word32 +randomW32 0 _ = error "randomW32: seed cannot be zero." +randomW32 _ 0 = error "randomW32: seed cannot be zero." +randomW32 seed1 seed2 = s1 + s2 + + where + + s1 :: Stream Word32 + s1 = [seed1] ++ (xorshift32 s1) + + s2 :: Stream Word32 + s2 = [seed2] ++ (xorshift32 s2) + + -- This is a simple implementation of an Xorshift algorithm + xorshift32 :: Stream Word32 -> Stream Word32 + xorshift32 x1 = x4 -- Note: 0 maps to itself with this + where + x4 = x3 .^. (x3 .<<. (5 :: Stream Word32)) + x3 = x2 .^. (x2 .>>. (17 :: Stream Word32)) + x2 = x1 .^. (x1 .<<. (13 :: Stream Word32)) + +-- | Given two Word64 seeds, produce a pseudo-random stream of Word64 numbers, +-- which has a period of 2^128 - 1. Neither of the seeds should be zero, as +-- doing so will negatively impact the quality of the randomness. +-- +-- This function uses an Xorshiftrplus algorithm. +randomW64 :: Word64 -> Word64 -> Stream Word64 +randomW64 0 _ = error "randomW64: seed cannot be zero." +randomW64 _ 0 = error "randomW64: seed cannot be zero." +randomW64 seed1 seed2 = x + + where + + s0 :: Stream Word64 + s0 = [seed1] ++ s1 + + s1 :: Stream Word64 + s1 = [seed2] ++ (x + s1) + + x :: Stream Word64 + x = xorshiftr128plus s0 s1 + + xorshiftr128plus :: Stream Word64 -> Stream Word64 -> Stream Word64 + xorshiftr128plus x1 y = x4 + where + x4 = x3 .^. y + x3 = x2 .^. (x2 .>>. (17 :: Stream Word64)) + x2 = x1 .^. (x1 .<<. (23 :: Stream Word64)) + +-- | Given a stream of random integral numbers, a minimum value, and a maximum +-- value, produce a stream of random values greater than or equal to the +-- minimum and less than the maximum value, i.e., [@mN@, @mX@). +boundedRandomIntegral :: (Typed a, Integral a) + => Stream a -> a -> a -> Stream a +boundedRandomIntegral gen mN mX = (gen `mod` constant (mX - mN)) + constant mN + +-- | Given a stream of random integral numbers and two integers defining the +-- numerator and denominator of a rational probability, produce a boolean +-- stream that is randomly @True@ with the given probability. That is to say, +-- given a numerator @n@ and denominator @d@, then, over a sufficiently large +-- sample size, the resulting stream @s@ is @True@ @n@ out of @d@ times. +proportionalRandomBool :: (Typed a, Integral a) + => Stream a -> a -> a -> Stream Bool +proportionalRandomBool gen n d = (gen `mod` constant d) < constant n + +-- | Given a stream of random integral numbers, an array of values, and an +-- equal length array of weights, produce a stream of random values from the +-- given array with probabilities proportional to the given weights. +weightedRandomSelection :: forall a b s + . (KnownNat s, s <= MaxWord32, Typed a, Typed b, + Integral a, Bounded a) + => Stream a -> Array s b -> Array s a -> Stream b +weightedRandomSelection gen values weights + | overflow + = error "weightedRandomSelection: sum of weights overflows type" + + | signedType + = error "weightedRandomSelection: type of weights array must be unsigned" + + | otherwise + = constant values ! idx + + where + + -- Check if cumulativeSum decreases at any point. For unsigned integral + -- types, a decreasing element in this cumulative sequence corresponds to + -- an overflow. + overflow = or (zipWith (>) cumulativeSum (drop 1 cumulativeSum)) + + signedType = 0 > (minBound :: a) + + idx :: Stream Word32 + idx = countLeq cumulativeSum (gen `mod` constant totalSum) + + countLeq :: [a] -> Stream a -> Stream Word32 + countLeq xs v = sum [ mux (constant x <= v) 1 0 | x <- xs ] + -- ^ get number of elements in @xs@ less than or equal to @v@. + -- For non-decreasing @xs@, this is equal to the index of the first + -- element greater than @v@. + + cumulativeSum :: [a] + cumulativeSum = scanl1 (+) (arrayElems weights) + + totalSum :: a + totalSum = last cumulativeSum + +-- | Type-level representation of the upper bound on an unsigned 32-bit +-- integer. +type MaxWord32 = 4294967295 -- 2^32 - 1 From 39548759d483719d4554bf8cd2e21adf5a8b21aa Mon Sep 17 00:00:00 2001 From: James Todd Gloyd Date: Fri, 23 Oct 2026 21:04:47 +0000 Subject: [PATCH 092/118] copilot-libraries: Document changes in CHANGELOG. Refs #766. --- copilot-libraries/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG index 0e8dcc83f..b95a2cd3f 100644 --- a/copilot-libraries/CHANGELOG +++ b/copilot-libraries/CHANGELOG @@ -1,3 +1,6 @@ +2026-10-23 + * Add random stream generation module. (#766) + 2026-09-07 * Version bump (4.8.1). (#760) From e6d4b6450f8c90247d7d9f5b105d1cbb9217901d Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 8 May 2026 14:56:02 +0000 Subject: [PATCH 093/118] copilot: Add Github Actions workflow file. Refs #790. CI jobs are being automatically cancelled by Travis CI mid-build. Travis CI is reporting the plan as being out of credits, when the organization have plenty of credits to run jobs to completion. This commit adds a Github Actions workflow file that replicates the steps executed by Travis CI. --- .github/workflows/build.yml | 66 +++++++++++++++++++++++++++++++++++++ 1 file changed, 66 insertions(+) create mode 100644 .github/workflows/build.yml diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml new file mode 100644 index 000000000..21e929e6c --- /dev/null +++ b/.github/workflows/build.yml @@ -0,0 +1,66 @@ +name: build + +# Trigger the workflow on push or pull request +on: + - pull_request + - push + +jobs: + cabal: + name: ${{ matrix.os }} / ghc ${{ matrix.ghc }} / cabal ${{ matrix.cabal }} + runs-on: ${{ matrix.os }} + strategy: + matrix: + os: [ubuntu-26.04] + cabal: ["2.4", "3.2", "3.4"] + ghc: + - "8.6.5" + - "8.8.4" + - "8.10.4" + - "9.0.1" + + steps: + + - uses: haskell-actions/setup@main + id: setup-haskell-cabal + name: Setup Haskell + continue-on-error: true + with: + ghc-version: ${{ matrix.ghc }} + cabal-version: ${{ matrix.cabal }} + + - name: Prepare environment + run: | + echo "$HOME/.ghcup/bin" >> $GITHUB_PATH + echo "$HOME/.cabal/bin" >> $GITHUB_PATH + sed -i -e "s;-- \(secure.\) True;\1 False;g" $HOME/.cabal/config + cabal update + + - uses: actions/checkout@v7 + + - name: Install dependencies + run: | + sudo apt-get install -y cppcheck z3 + + - name: Format check + run: | + # Fail if the any non-binary files contain trailing spaces. + if grep -nIHre ' \+$' * ; then exit 1; fi + + # Fail if the code, Cabal files, documentation or CHANGELOGs contain tabs. + if grep -rP '\t' --include='*.hs' --include='*.cabal' --include='*.md' --include='CHANGELOG' . ; then exit 1; fi + + - name: Install copilot + run: | + cabal v2-install --lib copilot/ copilot-core/ copilot-c99/ copilot-language/ copilot-libraries/ copilot-theorem/ copilot-interpreter/ copilot-prettyprinter/ + + - name: Test packages + if: matrix.ghc == '8.10.4' + run: | + cabal v2-test -j1 copilot-core/ copilot-language/ copilot-interpreter/ copilot-c99/ copilot-theorem/ copilot-libraries/ + + - name: Check cpp + if: matrix.ghc == '8.10.4' + run: | + export GHC_ENVIRONMENT=~/.ghc/x86_64-linux-8.10.4/environments/default + runhaskell copilot/examples/Heater.hs; cppcheck --force --addon=misra.py --suppress=misra-c2012-14.4 --error-exitcode=2 heater.c From a39952269a8545c7e71002b53f632336794c4be3 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 8 May 2026 14:56:13 +0000 Subject: [PATCH 094/118] copilot: Remove Travis CI file. Refs #790. CI jobs are being automatically cancelled by Travis CI mid-build. Travis CI is reporting the plan as being out of credits, when the organization have plenty of credits to run jobs to completion. A prior commit added a Github Actions workflow file that replicates the steps executed by Travis CI, thus making the Travis CI setup redundant. This commit removes the Travis CI script from the repository. --- .travis.yml | 58 ----------------------------------------------------- 1 file changed, 58 deletions(-) delete mode 100644 .travis.yml diff --git a/.travis.yml b/.travis.yml deleted file mode 100644 index 6cf023165..000000000 --- a/.travis.yml +++ /dev/null @@ -1,58 +0,0 @@ -# dist should be at least focal because we need cppcheck >= 1.88. -dist: focal - -# NB: don't set `language: haskell` here - -# The following enables several GHC versions to be tested; often it's enough to -# test only against the last release in a major GHC version. Feel free to omit -# lines listings versions you don't need/want testing for. -env: - - CABALVER=2.4 GHCVER=8.6.5 - - CABALVER=3.2 GHCVER=8.8.4 - - CABALVER=3.2 GHCVER=8.10.4 - - CABALVER=3.4 GHCVER=9.0.1 -# - CABALVER=head GHCVER=head # see section about GHC HEAD snapshots - -# Note: the distinction between `before_install` and `install` is not important. -before_install: - - travis_retry sudo add-apt-repository -y ppa:hvr/ghc - - travis_retry sudo apt-get update - - travis_retry sudo apt-get install cabal-install-$CABALVER ghc-$GHCVER # see note about happy/alex - - # We install z3 and cppcheck only for the tests, since they are not needed - # for normal compilation. - - if [ "${GHCVER}" == "8.10.4" ]; then travis_retry sudo apt-get install --yes z3 cppcheck; fi - - - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH - - cabal --version - - echo "$(ghc --version) [$(ghc --print-project-git-commit-id 2> /dev/null || echo '?')]" - - cabal user-config init - - sed -i -e "s;-- \(secure.\) True;\1 False;g" ${HOME}/.cabal/config - - travis_retry cabal update - - git submodule update --remote - -script: - # Fail if the any non-binary files contain trailing spaces. - - if grep -nIHre ' \+$' * ; then exit 1; fi - - # Fail if the code, Cabal files, documentation or CHANGELOGs contain tabs. - - if grep -rP '\t' --include='*.hs' --include='*.cabal' --include='*.md' --include='CHANGELOG' . ; then exit 1; fi - - # We explicitly install all libraries so that they are exposed and we can use - # them for tests (e.g., with runhaskell). There is no harm in doing this - # instead of installing just copilot. - - travis_wait 30 cabal v2-install --lib copilot copilot-core copilot-c99 copilot-language copilot-libraries copilot-theorem copilot-interpreter copilot-prettyprinter - - # Run tests only on GHC 8.10.4 - # - # Only libraries with tests are listed below or the v2-test command fails. - # - # Testing copilot-theorem and copilot-libraries requires z3. See above - # conditional installation, and keep GHC version numbers in both places in - # sync. - - if [ "${GHCVER}" == "8.10.4" ]; then cabal v2-test -j1 copilot-core copilot-language copilot-interpreter copilot-c99 copilot-theorem copilot-libraries; fi - - # Check that the code produced by Copilot complies with MISRA C 2012. We - # explicitly make cppcheck produce a non-zero exit code on non-compliance - # with the standard to make the CI build fail. - - if [ "${GHCVER}" == "8.10.4" ]; then runhaskell copilot/examples/Heater.hs; cppcheck --force --addon=misra.py --suppress=misra-c2012-14.4 --error-exitcode=2 heater.c; fi From b0e6e698ded581bdb49c7d7e0ac6196e39cab2b8 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 21:01:56 +0000 Subject: [PATCH 095/118] copilot: Replace Travis CI badge with Github Actions badge in README. Refs #790. CI jobs are being automatically cancelled by Travis CI mid-build. Travis CI is reporting the plan as being out of credits, when the organization have plenty of credits to run jobs to completion. Prior commits replaced the Travis CI-based setup with one based on Github Actions. This commit updates the Travis CI build status badge in the `README.md` to reflect the build status of the `master` branch on Github Actions, and to point to the corresponding workflow file. --- copilot/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot/README.md b/copilot/README.md index 536665d87..63a2459ef 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -2,7 +2,7 @@ # Copilot -[![Build Status](https://api.travis-ci.com/Copilot-Language/copilot.svg?branch=master)](https://app.travis-ci.com/github/Copilot-Language/copilot) +[![Build Status](https://github.com/Copilot-Language/copilot/actions/workflows/build.yml/badge.svg?branch=master)](https://github.com/Copilot-Language/copilot/actions/workflows/build.yml) [![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 701880b127fadd9d94f9f8c73ec44ba791d42775 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 21:27:02 +0000 Subject: [PATCH 096/118] copilot: Document changes in CHANGELOG. Refs #790. --- copilot/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index 4758ed15b..c350ec33a 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,7 +1,8 @@ -2026-10-15 +2026-11-07 * Adjust Travis CI script to flag presence of tabs as an error. (#774) * Adjust Travis CI script to flag trailing space as an error. (#777) * Update README to correct typos and improve readability. (#779) + * Replace Travis CI with Github Actions. (#790) 2026-09-07 * Version bump (4.8.1). (#760) From 1a137a86d5a8459750d3092e28679cb326e868d2 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 097/118] copilot-core: Version bump (4.8.2). Refs #792. --- 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 57f92d703..288399a9c 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.8.1 +version: 4.8.2 synopsis: An intermediate representation for Copilot. description: Intermediate representation for Copilot. From c666b71483eaf5889f53fa82d588d991bc123e35 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 098/118] copilot-bluespec: Version bump (4.8.2). Refs #792. --- copilot-bluespec/copilot-bluespec.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-bluespec/copilot-bluespec.cabal b/copilot-bluespec/copilot-bluespec.cabal index e8f29e4d7..1d8f7b3af 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.8.1 +version : 4.8.2 synopsis : A compiler for Copilot targeting FPGAs. description : This package is a back-end from Copilot to FPGAs in Bluespec. @@ -51,7 +51,7 @@ library , ieee754 >= 0.8.0 && < 0.9 , pretty >= 1.1.2 && < 1.2 - , copilot-core >= 4.8.1 && < 4.9 + , copilot-core >= 4.8.2 && < 4.9 , language-bluespec >= 0.1 && < 0.2 exposed-modules : Copilot.Compile.Bluespec From fd210f80474c58044014aaa8bf5014aeffa1ef16 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 099/118] copilot-c99: Version bump (4.8.2). Refs #792. --- 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 ea2e233dc..7e1e3d17a 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.8.1 +version : 4.8.2 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.8.1 && < 4.9 + , copilot-core >= 4.8.2 && < 4.9 , language-c99 >= 0.2.0 && < 0.3 , language-c99-simple >= 0.3 && < 0.4 From c2b0269f9838f21e08e040e4bcb39635fd683eb0 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 100/118] copilot-prettyprinter: Version bump (4.8.2). Refs #792. --- 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 d6c2bcc11..35c5c7d7c 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.8.1 +version: 4.8.2 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.8.1 && < 4.9 + copilot-core >= 4.8.2 && < 4.9 exposed-modules: From d17de87e12bc1a7ba2f4bf4e26ec83e03d768c81 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 101/118] copilot-interpreter: Version bump (4.8.2). Refs #792. --- 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 538237a10..60152a66a 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.8.1 +version: 4.8.2 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.8.1 && < 4.9 + copilot-core >= 4.8.2 && < 4.9 exposed-modules: From 8e714c714950405f568b5e2ebb2f1a3e15ebc04e Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 102/118] copilot-theorem: Version bump (4.8.2). Refs #792. --- 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 cf3e8c44c..da29f566a 100644 --- a/copilot-theorem/copilot-theorem.cabal +++ b/copilot-theorem/copilot-theorem.cabal @@ -14,7 +14,7 @@ description: . -version : 4.8.1 +version : 4.8.2 license : BSD3 license-file : LICENSE maintainer : Ivan Perez @@ -63,8 +63,8 @@ library , transformers >= 0.5 && < 0.7 , what4 >= 1.3 && < 1.8 - , copilot-core >= 4.8.1 && < 4.9 - , copilot-prettyprinter >= 4.8.1 && < 4.9 + , copilot-core >= 4.8.2 && < 4.9 + , copilot-prettyprinter >= 4.8.2 && < 4.9 exposed-modules : Copilot.Theorem , Copilot.Theorem.Prove From 1f67ea0f33b69c775f25dd21d48c540d95e0ac45 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 103/118] copilot-language: Version bump (4.8.2). Refs #792. --- 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 b30c29db6..40ba65f2c 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.8.1 +version: 4.8.2 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.8.1 && < 4.9 - , copilot-interpreter >= 4.8.1 && < 4.9 - , copilot-theorem >= 4.8.1 && < 4.9 + , copilot-core >= 4.8.2 && < 4.9 + , copilot-interpreter >= 4.8.2 && < 4.9 + , copilot-theorem >= 4.8.2 && < 4.9 exposed-modules: Copilot.Language , Copilot.Language.Operators.BitWise From c97769b18999b8be9b673726817123466bf1c4e9 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 104/118] copilot-libraries: Version bump (4.8.2). Refs #792. --- copilot-libraries/copilot-libraries.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-libraries/copilot-libraries.cabal b/copilot-libraries/copilot-libraries.cabal index b34020a57..6e18aba84 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.8.1 +version: 4.8.2 synopsis: Libraries for the Copilot language. description: Libraries for the Copilot language. @@ -41,7 +41,7 @@ library , containers >= 0.4 && < 0.9 , mtl >= 2.0 && < 2.4 , parsec >= 2.0 && < 3.2 - , copilot-language >= 4.8.1 && < 4.9 + , copilot-language >= 4.8.2 && < 4.9 exposed-modules: Copilot.Library.Analysis From dabb5562b912ae11074e2db5a3610c5a9c296bb6 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 105/118] copilot-verifier: Version bump (4.8.2). Refs #792. --- 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 4052ee006..bcf1061bf 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.8.1 +Version: 4.8.2 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.8.1 && < 4.9, - copilot-core >= 4.8.1 && < 4.9, - copilot-theorem >= 4.8.1 && < 4.9, + copilot-c99 >= 4.8.2 && < 4.9, + copilot-core >= 4.8.2 && < 4.9, + copilot-theorem >= 4.8.2 && < 4.9, 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.8.1 && < 4.9, - copilot-language >= 4.8.1 && < 4.9, - copilot-libraries >= 4.8.1 && < 4.9, - copilot-prettyprinter >= 4.8.1 && < 4.9, + copilot >= 4.8.2 && < 4.9, + copilot-language >= 4.8.2 && < 4.9, + copilot-libraries >= 4.8.2 && < 4.9, + copilot-prettyprinter >= 4.8.2 && < 4.9, copilot-verifier exposed-modules: Copilot.Verifier.Examples From a9847388d62d2b725acf1c521ce5b31efc9af989 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 106/118] copilot-visualizer: Version bump (4.8.2). Refs #792. --- 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 3b1d539eb..34d2289bd 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.8.1 +version: 4.8.2 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.8.1 && < 4.9, - copilot-core >= 4.8.1 && < 4.9, - copilot-interpreter >= 4.8.1 && < 4.9, - copilot-language >= 4.8.1 && < 4.9 + copilot >= 4.8.2 && < 4.9, + copilot-core >= 4.8.2 && < 4.9, + copilot-interpreter >= 4.8.2 && < 4.9, + copilot-language >= 4.8.2 && < 4.9 exposed-modules: @@ -121,7 +121,7 @@ executable tikz-example build-depends: base >= 4.9 && < 5, - copilot >= 4.8.1 && < 4.9, + copilot >= 4.8.2 && < 4.9, copilot-visualizer if flag(examples) From 82d2e07f507e688a8ab5415a9b469787f84fa904 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 107/118] copilot: Version bump (4.8.2). Refs #792. --- copilot/copilot.cabal | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/copilot/copilot.cabal b/copilot/copilot.cabal index 5fa90035e..00a495e3f 100644 --- a/copilot/copilot.cabal +++ b/copilot/copilot.cabal @@ -1,5 +1,5 @@ name: copilot -version: 4.8.1 +version: 4.8.2 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.8.1 && < 4.9 - , copilot-theorem >= 4.8.1 && < 4.9 - , copilot-language >= 4.8.1 && < 4.9 - , copilot-libraries >= 4.8.1 && < 4.9 - , copilot-c99 >= 4.8.1 && < 4.9 - , copilot-prettyprinter >= 4.8.1 && < 4.9 + , copilot-core >= 4.8.2 && < 4.9 + , copilot-theorem >= 4.8.2 && < 4.9 + , copilot-language >= 4.8.2 && < 4.9 + , copilot-libraries >= 4.8.2 && < 4.9 + , copilot-c99 >= 4.8.2 && < 4.9 + , copilot-prettyprinter >= 4.8.2 && < 4.9 exposed-modules: Language.Copilot, Language.Copilot.Main From 9a6a2d4ebc52fa54fb7f090624c44b7ca6c8797e Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 108/118] copilot-core: Document changes in CHANGELOG. Refs #792. --- copilot-core/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index c8a3f790d..033129dbc 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,4 +1,5 @@ -2026-10-17 +2026-11-07 + * Version bump (4.8.2). (#792) * Increase test coverage for `Copilot.Core.Type.Array`. (#767) * Fix errors in the documentation of `Copilot.Core.Spec`. (#769) * Replace tab in CHANGELOG. (#772) From 8511f4801141ff2773a1787cb9d51e97e6523b33 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 109/118] copilot-bluespec: Document changes in CHANGELOG. Refs #792. --- copilot-bluespec/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG index b3cc16e04..b5130fa0b 100644 --- a/copilot-bluespec/CHANGELOG +++ b/copilot-bluespec/CHANGELOG @@ -1,4 +1,5 @@ -2026-10-12 +2026-11-07 + * Version bump (4.8.2). (#792) * Replace tabs in `DESIGN.md`. (#772) * Remove trailing spaces. (#775) From 3096f9356cc298409b2c2beb909f5cbdff38458b Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 110/118] copilot-c99: Document changes in CHANGELOG. Refs #792. --- copilot-c99/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-c99/CHANGELOG b/copilot-c99/CHANGELOG index 2caf70ef2..b53dcc838 100644 --- a/copilot-c99/CHANGELOG +++ b/copilot-c99/CHANGELOG @@ -1,3 +1,6 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + 2026-09-07 * Version bump (4.8.1). (#760) From c8e5d846f393ff4c60c079c510a6e4ca3cbb7ec3 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 111/118] copilot-prettyprinter: Document changes in CHANGELOG. Refs #792. --- copilot-prettyprinter/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-prettyprinter/CHANGELOG b/copilot-prettyprinter/CHANGELOG index 799783ce8..bbe715c47 100644 --- a/copilot-prettyprinter/CHANGELOG +++ b/copilot-prettyprinter/CHANGELOG @@ -1,3 +1,6 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + 2026-09-07 * Version bump (4.8.1). (#760) From 3b79a5b0213f85ca0dd3a904afa474a00f9562d3 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 112/118] copilot-interpreter: Document changes in CHANGELOG. Refs #792. --- copilot-interpreter/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-interpreter/CHANGELOG b/copilot-interpreter/CHANGELOG index 1b88d8eb7..55cdec51c 100644 --- a/copilot-interpreter/CHANGELOG +++ b/copilot-interpreter/CHANGELOG @@ -1,4 +1,5 @@ -2026-10-12 +2026-11-07 + * Version bump (4.8.2). (#792) * Replace tab in `Copilot.Interpreter.Eval`. (#772) 2026-09-07 From c6dcc87d50db4d3d33ecc7755d4fc4476413401c Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 113/118] copilot-theorem: Document changes in CHANGELOG. Refs #792. --- copilot-theorem/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index 251b49484..0207c5446 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,3 +1,6 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + 2026-09-07 * Version bump (4.8.1). (#760) * Remove unnecessary extension. (#733) From 184eaeaa68300f3a303cb92d678ead8ae89acc2b Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 114/118] copilot-language: Document changes in CHANGELOG. Refs #792. --- copilot-language/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-language/CHANGELOG b/copilot-language/CHANGELOG index 49162ceb0..4aacc9e2e 100644 --- a/copilot-language/CHANGELOG +++ b/copilot-language/CHANGELOG @@ -1,3 +1,6 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + 2026-09-07 * Version bump (4.8.1). (#760) From 1efa2d78fd4f4d40cadd36e0721b9020806cc202 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 115/118] copilot-libraries: Document changes in CHANGELOG. Refs #792. --- copilot-libraries/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG index b95a2cd3f..f84c75a48 100644 --- a/copilot-libraries/CHANGELOG +++ b/copilot-libraries/CHANGELOG @@ -1,4 +1,5 @@ -2026-10-23 +2026-11-07 + * Version bump (4.8.2). (#792) * Add random stream generation module. (#766) 2026-09-07 From 090ff4e6dd4914cd10497452de6970d23f84c5b5 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 116/118] copilot-verifier: Document changes in CHANGELOG. Refs #792. --- copilot-verifier/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-verifier/CHANGELOG b/copilot-verifier/CHANGELOG index 1dec1cfd0..c69ccd708 100644 --- a/copilot-verifier/CHANGELOG +++ b/copilot-verifier/CHANGELOG @@ -1,3 +1,6 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + 2026-09-07 * Version bump (4.8.1). (#760) From 11c0601e795f40db74538cc0d52c41f2810ebdf3 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 117/118] copilot-visualizer: Document changes in CHANGELOG. Refs #792. --- copilot-visualizer/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-visualizer/CHANGELOG b/copilot-visualizer/CHANGELOG index 9d772eca0..b578bedb9 100644 --- a/copilot-visualizer/CHANGELOG +++ b/copilot-visualizer/CHANGELOG @@ -1,3 +1,6 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + 2026-09-07 * Version bump (4.8.1). (#760) * Fix inconsistent version bounds for `copilot` in Cabal file. (#749) From 8049dbb1e8aea3b123ca54be5a285bd1950ea2c6 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 118/118] copilot: Document changes in CHANGELOG. Refs #792. --- copilot/CHANGELOG | 1 + 1 file changed, 1 insertion(+) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index c350ec33a..8b691705e 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,4 +1,5 @@ 2026-11-07 + * Version bump (4.8.2). (#792) * Adjust Travis CI script to flag presence of tabs as an error. (#774) * Adjust Travis CI script to flag trailing space as an error. (#777) * Update README to correct typos and improve readability. (#779)