From 4aae5528134e1a3f474c5efb4a7dc98d5dd49a76 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 28 May 2026 06:36:03 +0000 Subject: [PATCH 1/3] Update news for Copilot 4.7.1. Refs #62. --- home.md | 46 ++++++++++++++++++---------------------------- 1 file changed, 18 insertions(+), 28 deletions(-) diff --git a/home.md b/home.md index 964020f..b929cab 100644 --- a/home.md +++ b/home.md @@ -1,7 +1,7 @@ ## News -**Release 4.2 -- 2025-01-07** +**Release 4.7.1 -- 2026-05-07** -We are pleased to announce the release of Copilot 4.2, a stream-based DSL for +We are pleased to announce the release of Copilot 4.7.1, a stream-based DSL for writing and monitoring embedded C programs, with an emphasis on correctness and hard realtime requirements. Copilot is typically used as a high-level runtime verification framework, and supports temporal logic (LTL, PTLTL and MTL), @@ -10,45 +10,35 @@ clocks and voting algorithms. Among others, Copilot is being used at the Safety Critical Avionics Systems Branch of NASA Langley Research Center for monitoring test flights of drones. -This release introduces several big improvements to Copilot: +This release introduces several improvements to Copilot: -- Specifications can now use the same handler for multiple monitors, provided - that the arguments to those handlers always have consistent types and arity. -This simplifies the code that uses Copilot, since it's no longer necessary to -create multiple boilerplate wrappers around the same handling routines. +- Fix corner cases in the treatment of special floating point numbers in the + Bluespec backend and `copilot-theorem`. -- The use of structs has been vastly simplified. Before, it was necessary to - define class instances for structs, whose implementations were, although -repetitive, not intuitive especially for users unfamiliar with Haskell. In -Copilot 4.2, it is now possible to define those methods automatically by -relying on default method implementations that work well for most cases, -although users retain the ability to customize those methods if desired. +- Fix errors in examples in `copilot-theorem` that use Z3. -- We have increased test coverage in `copilot-core`, reaching full coverage of - the public interface. +- Add to `copilot-libraries` a module to perform sanity checks of Copilot + specifications. -The interface of `copilot-core` has also been simplified, deprecating record -fields of an existential type UExpr, which were largely unused outside of -Copilot's internals. +- Add to `copilot-libraries` a module to facilitate implementing state + machines. + +We expect those new modules to grow in the future. The new implementation is compatible with versions of GHC from 8.6 to 9.10, as well as with Stackage Nightly. -This release has been made possible thanks to key submissions from Frank Dedden -(@fdedden), Ryan Scott (@RyanGlScott), and Kyle Beechly (@kaBeech), the last of -which is also a first-time contributor to the project. We are grateful to them -for their timely contributions, especially during the holidays, and for making -Copilot better every day. We also want to thank the attendees of Zurihac 2024 -for technical discussions that helped find the right solutions to some of the -problems addressed by this release. +This release has been made possible thanks to key submissions from Ryan Scott +(Galois), and Chris Hathhorn (Galois). We are grateful to them for their timely +contributions, and for making Copilot better every day. Details are available -[here](https://github.com/Copilot-Language/copilot/milestone/30?closed=1), +[here](https://github.com/Copilot-Language/copilot/milestone/38?closed=1), and -[here](https://github.com/Copilot-Language/copilot/releases/tag/v4.2). +[here](https://github.com/Copilot-Language/copilot/releases/tag/v4.7.1). As always, we're releasing exactly 2 months since the last release. Our next -release is scheduled for Mar 7th, 2025. +release is scheduled for Jul 7th, 2026. We want to remind the community that Copilot is now accepting code contributions from external participants again. Please see the discussions and From 8a8cc8e3c0100bf499759d87f2aea8477c2175fd Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 28 May 2026 06:54:40 +0000 Subject: [PATCH 2/3] Bump version of `upload-pages-artifact`. Refs #63. --- .github/workflows/publish.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/publish.yml b/.github/workflows/publish.yml index 52cd929..f78a38f 100644 --- a/.github/workflows/publish.yml +++ b/.github/workflows/publish.yml @@ -22,7 +22,7 @@ jobs: make - name: Upload artifact - uses: actions/upload-pages-artifact@v2 + uses: actions/upload-pages-artifact@v5 deploy: permissions: From 8f1350812e0ebc41edd3c1ae027825ae627ac49e Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 28 May 2026 07:00:07 +0000 Subject: [PATCH 3/3] Bump version of `deploy-pages`. Refs #64. --- .github/workflows/publish.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/publish.yml b/.github/workflows/publish.yml index f78a38f..1615927 100644 --- a/.github/workflows/publish.yml +++ b/.github/workflows/publish.yml @@ -40,4 +40,4 @@ jobs: steps: - name: Deploy artifact id: deployment - uses: actions/deploy-pages@v1 + uses: actions/deploy-pages@v5