Merge branch 'release-4.3'. Close #604.

ivanperez-keera · ivanperez-keera · commit e04293366896 · 2025-03-07T18:22:58.000-08:00
**Description** Version 4.3 of Copilot is ready and should be closed and published on Hackage. **Type** - Management: release and publication. **Additional context** None. **Requester** - Ivan Perez. **Method to check presence of bug** Not applicable (not a bug). **Expected result** - Cabal files indicate new version number, constraints are adjusted as needed, commit is tagged with version number, and packages are published on Hackage. - The following docker image installs copilot enforcing the new version via compiler constraints. It prints the message "Success" at the end if all completes correctly, and shows an error message otherwise. ```Dockerfile FROM ubuntu:focal ENV DEBIAN_FRONTEND=noninteractive RUN apt-get update RUN apt-get install --yes \ libz-dev \ git \ curl \ gcc \ g++ \ make \ libgmp3-dev \ pkg-config RUN mkdir -p $HOME/.ghcup/bin RUN curl https://downloads.haskell.org/~ghcup/0.1.40.0/x86_64-linux-ghcup-0.1.40.0 -o $HOME/.ghcup/bin/ghcup RUN chmod a+x $HOME/.ghcup/bin/ghcup ENV PATH=$PATH:/root/.ghcup/bin/ ENV PATH=$PATH:/root/.cabal/bin/ SHELL ["/bin/bash", "-c"] RUN ghcup install ghc 9.10.1 RUN ghcup install cabal 3.14 RUN ghcup set ghc 9.10.1 RUN cabal update SHELL ["/bin/bash", "-c"] CMD git clone $REPO \ && cd $NAME \ && git checkout $COMMIT \ && cabal install \ --package-env . \ --lib \ --constraint="copilot==4.3" \ --constraint="copilot-c99==4.3" \ --constraint="copilot-core==4.3" \ --constraint="copilot-prettyprinter==4.3" \ --constraint="copilot-interpreter==4.3" \ --constraint="copilot-language==4.3" \ --constraint="copilot-libraries==4.3" \ --constraint="copilot-theorem==4.3" \ copilot**/ \ && echo Success ``` Command (substitute variables based on new path after merge): ``` $ docker run -e "REPO=https://github.com/Copilot-Language/copilot" -e "NAME=copilot" -e "COMMIT=<HASH>" -it copilot-verify-604 ``` **Solution implemented** - Cabal files indicate new version number, constraints are adjusted as needed, commit is tagged with version number, and packages are published on Hackage. **Further notes** None.
diff --git a/copilot-c99/CHANGELOG b/copilot-c99/CHANGELOG
@@ -1,3 +1,6 @@
+2025-03-07
+        * Version bump (4.3). (#604)
+
 2025-01-07
         * Version bump (4.2). (#577)
         * Remove uses of Copilot.Core.Expr.UExpr.uExprType. (#565)
diff --git 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.2
+version                   : 4.3
 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.2   && < 4.3
+                          , copilot-core        >= 4.3   && < 4.4
                           , language-c99        >= 0.2.0 && < 0.3
                           , language-c99-simple >= 0.3   && < 0.4
 
diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG
@@ -1,4 +1,5 @@
-2025-02-28
+2025-03-07
+        * Version bump (4.3). (#604)
         * Fix typo in documentation. (#587)
         * Add a Show instance for Type. (#589)
         * Add a Prop type to capture how a property is quantified. (#254)
diff --git 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.2
+version:             4.3
 synopsis:            An intermediate representation for Copilot.
 description:
   Intermediate representation for Copilot.
diff --git a/copilot-interpreter/CHANGELOG b/copilot-interpreter/CHANGELOG
@@ -1,3 +1,6 @@
+2025-03-07
+        * Version bump (4.3). (#604)
+
 2025-01-07
         * Version bump (4.2). (#577)
 
diff --git 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.2
+version:             4.3
 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.2 && < 4.3
+    copilot-core >= 4.3 && < 4.4
 
   exposed-modules:
 
diff --git a/copilot-language/CHANGELOG b/copilot-language/CHANGELOG
@@ -1,4 +1,5 @@
 2025-03-07
+        * Version bump (4.3). (#604)
         * Fix typo in documentation. (#587)
         * Record how a Property's underlying proposition is quantified. (#254)
         * Remove deprecated function Copilot.Language.Operators.Array.(.!!).
diff --git 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.2
+version:             4.3
 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.2 && < 4.3
-               , copilot-interpreter   >= 4.2 && < 4.3
-               , copilot-theorem       >= 4.2 && < 4.3
+               , copilot-core          >= 4.3 && < 4.4
+               , copilot-interpreter   >= 4.3 && < 4.4
+               , copilot-theorem       >= 4.3 && < 4.4
 
   exposed-modules: Copilot.Language
                  , Copilot.Language.Operators.BitWise
diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG
@@ -1,4 +1,5 @@
 2025-03-07
+        * Version bump (4.3). (#604)
         * Remove deprecated function Copilot.Library.Utils.(!!). (#599)
 
 2025-01-07
diff --git 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.2
+version:             4.3
 synopsis:            Libraries for the Copilot language.
 description:
   Libraries for the Copilot language.
@@ -41,7 +41,7 @@ library
                , containers       >= 0.4 && < 0.8
                , mtl              >= 2.0 && < 2.4
                , parsec           >= 2.0 && < 3.2
-               , copilot-language >= 4.2 && < 4.3
+               , copilot-language >= 4.3 && < 4.4
 
   exposed-modules:
       Copilot.Library.Libraries
diff --git a/copilot-prettyprinter/CHANGELOG b/copilot-prettyprinter/CHANGELOG
@@ -1,4 +1,5 @@
-2025-02-28
+2025-03-07
+        * Version bump (4.3). (#604)
         * Update pretty-printing to handle Props. (#254)
 
 2025-01-07
diff --git 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.2
+version:             4.3
 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.2 && < 4.3
+    copilot-core >= 4.3 && < 4.4
 
   exposed-modules:
 
diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG
@@ -1,4 +1,5 @@
-2025-02-28
+2025-03-07
+        * Version bump (4.3). (#604)
         * Fix multiple typos in README. (#560)
         * Fix typo in documentation. (#587)
         * Add function to produce counterexamples for invalid properties. (#589)
diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal
@@ -14,7 +14,7 @@ description:
   <https://copilot-language.github.io>.
 
 
-version                   : 4.2
+version                   : 4.3
 license                   : BSD3
 license-file              : LICENSE
 maintainer                : Ivan Perez <ivan.perezdominguez@nasa.gov>
@@ -63,8 +63,8 @@ library
                           , xml                   >= 1.3 && < 1.4
                           , what4                 >= 1.3 && < 1.7
 
-                          , copilot-core          >= 4.2 && < 4.3
-                          , copilot-prettyprinter >= 4.2 && < 4.3
+                          , copilot-core          >= 4.3 && < 4.4
+                          , copilot-prettyprinter >= 4.3 && < 4.4
 
   exposed-modules         : Copilot.Theorem
                           , Copilot.Theorem.Prove
diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG
@@ -1,4 +1,5 @@
-2025-03-05
+2025-03-07
+        * Version bump (4.3). (#604)
         * Include missing dependencies in installation instructions. (#591)
         * Update version of GHC in README. (#590)
         * Add example of how to use proveWithCounterExample. (#589)
diff --git a/copilot/copilot.cabal b/copilot/copilot.cabal
@@ -1,5 +1,5 @@
 name:                copilot
-version:             4.2
+version:             4.3
 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.2 && < 4.3
-                     , copilot-theorem       >= 4.2 && < 4.3
-                     , copilot-language      >= 4.2 && < 4.3
-                     , copilot-libraries     >= 4.2 && < 4.3
-                     , copilot-c99           >= 4.2 && < 4.3
-                     , copilot-prettyprinter >= 4.2 && < 4.3
+                     , copilot-core          >= 4.3 && < 4.4
+                     , copilot-theorem       >= 4.3 && < 4.4
+                     , copilot-language      >= 4.3 && < 4.4
+                     , copilot-libraries     >= 4.3 && < 4.4
+                     , copilot-c99           >= 4.3 && < 4.4
+                     , copilot-prettyprinter >= 4.3 && < 4.4
 
 
     exposed-modules: Language.Copilot, Language.Copilot.Main

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,5 @@`
`1`	`1`	`2025-03-07`
	`2`	`+ * Version bump (4.3). (#604)`
`2`	`3`	`* Fix typo in documentation. (#587)`
`3`	`4`	`* Record how a Property's underlying proposition is quantified. (#254)`
`4`	`5`	`* Remove deprecated function Copilot.Language.Operators.Array.(.!!).`