[Haskell-cafe] [ANN] Copilot 4.2

[Ivan Perez]

Hi everyone!!

We are really excited to announce Copilot 4.2 [1,2]. Copilot is a
stream-based EDSL in Haskell 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), clocks and voting algorithms. Compilation to Bluespec, to
target FPGAs, is also supported.

Copilot is NASA Class D open-source software, and is being used at NASA
in drone test flights. Through the NASA tool Ogma [3] (also written in
Haskell), Copilot also serves as a runtime monitoring backend for
NASA's Core Flight System, Robot Operating System (ROS2), FPrime (the
software framework used in the Mars Helicopter).

This release introduces several big 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.

- 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.

- We have increased test coverage in `copilot-core`, reaching full
  coverage of all elements of the public interface that are not
  automatically generated by GHC.

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.

The new implementation is compatible with versions of GHC from 8.6 to
9.10, as well as Stackage Nightly.

This release has been made possible thanks to key submissions from
Frank Dedden, Ryan Scott, and Kyle Beech, 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.

For details on this release, see [1].
https://github.com/Copilot-Language/copilot/releases/tag/v4.2.

As always, we're releasing exactly 2 months since the last release. Our
next release is scheduled for Mar 7th, 2025.

We want to remind the community that Copilot is now accepting code
contributions from external participants again. Please see the
discussions and the issues in our github repo [4] to learn how to
participate.

Current emphasis is on improving the codebase in terms of performance,
stability and test coverage, removing unnecessary dependencies, hiding
internal definitions, formatting the code to meet our new coding
standards, and simplifying the Copilot interface. Users are encouraged
to participate by opening issues, asking questions, extending the
implementation, and sending bug fixes.

Happy Haskelling!

Ivan

--

[1] https://github.com/Copilot-Language/copilot/releases/tag/v4.2

[2] https://hackage.haskell.org/package/copilot

[3] https://github.com/nasa/ogma

[4] https://github.com/Copilot-Language/copilot
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20250107/09cdb74b/attachment.html>