[ANN] Copilot 4.7.1

--===============1899493347068097938==
Content-Type: multipart/alternative; boundary="000000000000f3fcc50652db6175"

--000000000000f3fcc50652db6175
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

Hi caf=C3=A9!

We are really excited to announce Copilot 4.7.1 [1]. Copilot is a
stream-based EDSL in Haskell for writing and monitoring embedded
systems, 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 and with rovers. Through the NASA tool Ogma [2]
(also written in Haskell), Copilot also serves as a programming
language and runtime framework for NASA's Core Flight System, Robot
Operating System (ROS 2) and FPrime (the software framework used in the
Mars Helicopter). Ogma now supports producing flight and robotics
applications directly in Copilot, not just for monitoring, but for
implementing the logic of the applications themselves.

This release introduces several improvements to Copilot:

- Fix corner cases in the treatment of special floating point numbers
in the Bluespec backend and `copilot-theorem`.

- Fix errors in examples in `copilot-theorem` that use Z3.

- Add to `copilot-libraries` a module to perform sanity checks of
Copilot specifications.

- Add to `copilot-libraries` a module to facilitate implementing state
machines.

Copilot is compatible with versions of GHC from 8.6 to 9.10. Packages
are published on Hackage [3], as well as several Linux distributions
(e.g., Debian, Fedora).

This release has been possible thanks to submissions from Ryan Scott
(Galois) and Chris Hathhorn (Galois). We are grateful to them for their
contributions, and for making Copilot better every day.

For details on this release, see:
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 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 the issues in our Github repo [4] to learn how to
participate.

Current emphasis is on using Copilot for full data processing
applications (e.g, system control, arduinos, rovers, drones), improving
usability, performance, and stability, increasing test coverage,
removing unnecessary dependencies, hiding internal definitions, and
formatting the code to meet our coding standards. 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.7.1

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

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

[4] https://github.com/Copilot-Language/copilot

--000000000000f3fcc50652db6175
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr">Hi caf=C3=A9!<br><br>We are really excited to announce Cop=
ilot 4.7.1 [1]. Copilot is a<br>stream-based EDSL in Haskell for writing an=
d monitoring embedded<br>systems, with an emphasis on correctness and hard =
realtime<br>requirements. Copilot is typically used as a high-level runtime=
<br>verification framework, and supports temporal logic (LTL, PTLTL and<br>=
MTL), clocks and voting algorithms. Compilation to Bluespec, to target<br>F=
PGAs, is also supported.<br><br>Copilot is NASA Class D open-source softwar=
e, and is being used at NASA<br>in drone test flights and with rovers. Thro=
ugh the NASA tool Ogma [2]<br>(also written in Haskell), Copilot also serve=
s as a programming<br>language and runtime framework for NASA&#39;s Core Fl=
ight System, Robot<br>Operating System (ROS 2) and FPrime (the software fra=
mework used in the<br>Mars Helicopter). Ogma now supports producing flight =
and robotics<br>applications directly in Copilot, not just for monitoring, =
but for<br>implementing the logic of the applications themselves.<br><br>Th=
is release introduces several improvements to Copilot:<br><br>- Fix corner =
cases in the treatment of special floating point numbers<br>in the Bluespec=
 backend and `copilot-theorem`.<br><br>- Fix errors in examples in `copilot=
-theorem` that use Z3.<br><br>- Add to `copilot-libraries` a module to perf=
orm sanity checks of<br>Copilot specifications.<br><br>- Add to `copilot-li=
braries` a module to facilitate implementing state<br>machines.<br><br>Copi=
lot is compatible with versions of GHC from 8.6 to 9.10. Packages<br>are pu=
blished on Hackage [3], as well as several Linux distributions<br>(e.g., De=
bian, Fedora).<br><br>This release has been possible thanks to submissions =
from Ryan Scott<br>(Galois) and Chris Hathhorn (Galois). We are grateful to=
 them for their<br>contributions, and for making Copilot better every day.<=
br><br>For details on this release, see:<br><a href=3D"https://github.com/C=
opilot-Language/copilot/releases/tag/v4.7.1">https://github.com/Copilot-Lan=
guage/copilot/releases/tag/v4.7.1</a>.<br><br>As always, we&#39;re releasin=
g exactly 2 months since the last release. Our<br>next release is scheduled=
 for Jul 7th, 2026.<br><br>We want to remind the community that Copilot is =
now accepting code<br>contributions from external participants again. Pleas=
e see the<br>discussions and the issues in our Github repo [4] to learn how=
 to<br>participate.<br><br>Current emphasis is on using Copilot for full da=
ta processing<br>applications (e.g, system control, arduinos, rovers, drone=
s), improving<br>usability, performance, and stability, increasing test cov=
erage,<br>removing unnecessary dependencies, hiding internal definitions, a=
nd<br>formatting the code to meet our coding standards. Users are encourage=
d<br>to participate by opening issues, asking questions, extending the<br>i=
mplementation, and sending bug fixes.<br><br>Happy Haskelling!<br><br>Ivan<=
br><br>--<br><br>[1] <a href=3D"https://github.com/Copilot-Language/copilot=
/releases/tag/v4.7.1">https://github.com/Copilot-Language/copilot/releases/=
tag/v4.7.1</a><br><br>[2] <a href=3D"https://github.com/nasa/ogma">https://=
github.com/nasa/ogma</a><br><br>[3] <a href=3D"https://hackage.haskell.org/=
package/copilot">https://hackage.haskell.org/package/copilot</a><br><br>[4]=
 <a href=3D"https://github.com/Copilot-Language/copilot">https://github.com=
/Copilot-Language/copilot</a></div>

--000000000000f3fcc50652db6175--

--===============1899493347068097938==
Content-Type: text/plain; charset="us-ascii"
MIME-Version: 1.0
Content-Transfer-Encoding: 7bit
Content-Disposition: inline

_______________________________________________
Haskell-Cafe mailing list -- [email protected]
To (un)subscribe, modify options or view archives go to:
Only members subscribed via the mailman list are allowed to post.
--===============1899493347068097938==--