From ebe9582fe1f6a549542f08b88e7b27d5a7920136 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 9 Nov 2021 09:26:23 -0500 Subject: [PATCH 01/31] Update POC on website. Refs #36. Update POC from Frank to Ivan. --- contact.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/contact.md b/contact.md index 82b25e9..952f576 100644 --- a/contact.md +++ b/contact.md @@ -9,8 +9,8 @@ and discuss the issue. ## General Questions For general questions about Copilot, questions that are unsuited to be posted publicly or if you are not in the possession of a GitHub account, please send -your questions to the maintainer, Frank Dedden -[dev@dedden.net](mailto://dev@dedden.net). +your questions to the maintainer, Ivan Perez +[ivan.perezdominguez@nasa.gov](mailto://ivan.perezdominguez@nasa.gov). ## Previous developers From b3752e56ee6df5a3d41ee6092577c617b125263a Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 9 Nov 2021 09:31:33 -0500 Subject: [PATCH 02/31] Updated the news for Copilot 3.6. Refs #35. --- home.md | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/home.md b/home.md index a684674..cc2739e 100644 --- a/home.md +++ b/home.md @@ -1,7 +1,7 @@ ## News -**Release 3.5 -- 2021-09-07** +**Release 3.6 -- 2021-11-07** -We are pleased to announce the release of Copilot 3.5, a stream-based DSL for +We are pleased to announce the release of Copilot 3.6, 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,21 +10,18 @@ clocks and voting algorithms. Among others, Copilot has been used at the Safety Critical Avionics Systems Branch of NASA Langley Research Center for monitoring test flights of drones. -This new release introduces a simple but important feature to make Copilot code -more modular: the name of Copilot's main entry point in the generated C code, -known as the step function, can now be customized. This will allow -specifications to be defined in different modules, compiled separately, and -linked as part of the same C executable. It will also facilitate interoperation -with other systems that consider 'step' a reserved a global name. -Additionally, this release introduces other fixes in the code and in the -documentation, and deprecates definitions that have been superseded. +This new release supports three new operators: atan2, floor, and ceiling. +Additionally, the target directory of the code generated by Copilot can now be +customized. Release 3.6 also includes a battery of unit tests for the library +copilot-core. This release introduces other fixes in the code and in the +documentation, and deprecates definitions that have been superseded or that +were largely unused. Current emphasis is on facilitating the use with other systems, and improving the codebase in terms of stability and test coverage. Users are encouraged to participate by opening issues and asking questions via our [github repo](https://github.com/copilot-language/copilot). - ## Licence Copilot is distributed under the BSD-3-Clause licence, which can be found [here](https://raw.githubusercontent.com/Copilot-Language/Copilot/master/LICENSE). From c6c5f1d01ffd6c0d7e2291183c2ef042f72f8bd9 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 8 Jan 2022 01:42:43 +0100 Subject: [PATCH 03/31] Updated the news for Copilot 3.7. Refs #37. --- home.md | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/home.md b/home.md index cc2739e..8385144 100644 --- a/home.md +++ b/home.md @@ -1,7 +1,7 @@ ## News -**Release 3.6 -- 2021-11-07** +**Release 3.7 -- 2022-01-07** -We are pleased to announce the release of Copilot 3.6, a stream-based DSL for +We are pleased to announce the release of Copilot 3.7, 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,12 +10,8 @@ clocks and voting algorithms. Among others, Copilot has been used at the Safety Critical Avionics Systems Branch of NASA Langley Research Center for monitoring test flights of drones. -This new release supports three new operators: atan2, floor, and ceiling. -Additionally, the target directory of the code generated by Copilot can now be -customized. Release 3.6 also includes a battery of unit tests for the library -copilot-core. This release introduces other fixes in the code and in the -documentation, and deprecates definitions that have been superseded or that -were largely unused. +This new release fixes 5 bugs, and removes deprecated definitions, and +deprecates internal types. Current emphasis is on facilitating the use with other systems, and improving the codebase in terms of stability and test coverage. Users are encouraged to From dc0fbd1a5cdaddf94ed7de06607221b2f1bdc91f Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 24 Mar 2022 10:50:01 -0400 Subject: [PATCH 04/31] Updated the news for Copilot 3.8. Refs #38. --- home.md | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/home.md b/home.md index 8385144..9160092 100644 --- a/home.md +++ b/home.md @@ -1,7 +1,7 @@ ## News -**Release 3.7 -- 2022-01-07** +**Release 3.8 -- 2022-01-08** -We are pleased to announce the release of Copilot 3.7, a stream-based DSL for +We are pleased to announce the release of Copilot 3.8, 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,8 +10,9 @@ clocks and voting algorithms. Among others, Copilot has been used at the Safety Critical Avionics Systems Branch of NASA Langley Research Center for monitoring test flights of drones. -This new release fixes 5 bugs, and removes deprecated definitions, and -deprecates internal types. +This new release introduces further unit tests, removes deprecated definitions +and modules. It also marks packages as uncurated to prevent modifications on +the part of the Hackage maintainers. Current emphasis is on facilitating the use with other systems, and improving the codebase in terms of stability and test coverage. Users are encouraged to From 7e3ef219d36560cce8436b4e23f33150c3cc74bd Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 16 May 2022 09:27:16 -0400 Subject: [PATCH 05/31] Update news for Copilot 3.9. Refs #39. --- home.md | 24 +++++++++++++++--------- 1 file changed, 15 insertions(+), 9 deletions(-) diff --git a/home.md b/home.md index 9160092..34e50df 100644 --- a/home.md +++ b/home.md @@ -1,7 +1,7 @@ ## News -**Release 3.8 -- 2022-01-08** +**Release 3.9 -- 2022-01-08** -We are pleased to announce the release of Copilot 3.8, a stream-based DSL for +We are pleased to announce the release of Copilot 3.9, 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,13 +10,19 @@ clocks and voting algorithms. Among others, Copilot has been used at the Safety Critical Avionics Systems Branch of NASA Langley Research Center for monitoring test flights of drones. -This new release introduces further unit tests, removes deprecated definitions -and modules. It also marks packages as uncurated to prevent modifications on -the part of the Hackage maintainers. - -Current emphasis is on facilitating the use with other systems, and improving -the codebase in terms of stability and test coverage. Users are encouraged to -participate by opening issues and asking questions via our [github +This new release fixes multiple bugs, removes deprecated elements, hides +internal parts of the implementation from the public API, implements part of +our new coding standard, and adds support for GHC 9. As part of this new +release, we have also put in place a new software engineering process designed +to meet the requirements to obtain NASA's Class D software classification. +Details are available +[here](https://github.com/Copilot-Language/copilot/milestone/13?closed=1). + +Current emphasis is on facilitating the use with other systems, improving the +codebase in terms of stability and test coverage, removing unnecessary +dependencies, hiding internal definitions, and formatting the code to meet our +new coding standards. Users are encouraged to participate by opening issues and +asking questions via our [github repo](https://github.com/copilot-language/copilot). ## Licence From fed5678805871dbc26466e98e2523e2845ff3e9a Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 7 Sep 2022 23:03:54 +0000 Subject: [PATCH 06/31] Update news for Copilot 3.10. Refs #40. --- home.md | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/home.md b/home.md index 34e50df..05a602c 100644 --- a/home.md +++ b/home.md @@ -1,7 +1,7 @@ ## News -**Release 3.9 -- 2022-01-08** +**Release 3.10 -- 2022-07-07** -We are pleased to announce the release of Copilot 3.9, a stream-based DSL for +We are pleased to announce the release of Copilot 3.10, 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,12 +10,12 @@ clocks and voting algorithms. Among others, Copilot has been used at the Safety Critical Avionics Systems Branch of NASA Langley Research Center for monitoring test flights of drones. -This new release fixes multiple bugs, removes deprecated elements, hides -internal parts of the implementation from the public API, implements part of -our new coding standard, and adds support for GHC 9. As part of this new -release, we have also put in place a new software engineering process designed -to meet the requirements to obtain NASA's Class D software classification. -Details are available +This new release alters how structs are passed as arguments to handler +functions. It also fixes multiple bugs, removes deprecated elements, hides +internal parts of the implementation from the public API, and removes +unnecessary dependencies. This release also continues to use our new software +engineering process designed to meet the requirements to obtain NASA's Class D +software classification. Details are available [here](https://github.com/Copilot-Language/copilot/milestone/13?closed=1). Current emphasis is on facilitating the use with other systems, improving the From 73f286a60f9bd4a56eaf317a4adc026b4e0252dd Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 7 Sep 2022 23:09:42 +0000 Subject: [PATCH 07/31] Fix broken link to examples. Refs #41. --- documentation.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/documentation.md b/documentation.md index 3c6089e..b8acead 100644 --- a/documentation.md +++ b/documentation.md @@ -3,7 +3,7 @@ A manual to Copilot can be downloaded [here](downloads/copilot_tutorial.pdf). Copilot comes with a set of examples as part of its distribution, available in the [Examples -directory](https://github.com/Copilot-Language/Copilot/tree/master/Examples) of +directory](https://github.com/Copilot-Language/Copilot/tree/master/copilot/examples) of the repository. From 759c84ac647c6c64f3bc66ac7ba2e7c47142e935 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 7 Sep 2022 23:14:55 +0000 Subject: [PATCH 08/31] Update news for Copilot 3.11. Refs #42. --- home.md | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/home.md b/home.md index 05a602c..80d62db 100644 --- a/home.md +++ b/home.md @@ -1,7 +1,7 @@ ## News -**Release 3.10 -- 2022-07-07** +**Release 3.11 -- 2022-09-07** -We are pleased to announce the release of Copilot 3.10, a stream-based DSL for +We are pleased to announce the release of Copilot 3.11, 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,13 +10,15 @@ clocks and voting algorithms. Among others, Copilot has been used at the Safety Critical Avionics Systems Branch of NASA Langley Research Center for monitoring test flights of drones. -This new release alters how structs are passed as arguments to handler -functions. It also fixes multiple bugs, removes deprecated elements, hides -internal parts of the implementation from the public API, and removes -unnecessary dependencies. This release also continues to use our new software +This new release introduces a new library copilot-interpreter that exposes the +functions related to the interpreter backend, pre-existing functions included +as part of copilot-core are now deprecated. It also fixes multiple bugs, +removes deprecated elements, hides internal parts of the implementation from +the public API, and improves the codebase by re-implementing a function without +the use of unsafeCoerce. This release also continues to use our new software engineering process designed to meet the requirements to obtain NASA's Class D software classification. Details are available -[here](https://github.com/Copilot-Language/copilot/milestone/13?closed=1). +[here](https://github.com/Copilot-Language/copilot/milestone/15?closed=1). Current emphasis is on facilitating the use with other systems, improving the codebase in terms of stability and test coverage, removing unnecessary From 5c4a428dabcaac8604ac2f818801848419075a04 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 7 Sep 2022 23:16:32 +0000 Subject: [PATCH 09/31] Document existence of copilot-interpreter as part of Copilot 3.11. Refs #42. --- documentation.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/documentation.md b/documentation.md index b8acead..5610fd6 100644 --- a/documentation.md +++ b/documentation.md @@ -22,6 +22,9 @@ that make up Copilot, that all share a single repository: new back-end to Copilot. ([Hackage](https://hackage.haskell.org/package/copilot-core)) +- `copilot-interpreter`: A backend for simulating Copilot specifications. + ([Hackage](https://hackage.haskell.org/package/copilot-interpreter)) + - `copilot-language`: The front-end of Copilot defining the user language. A user of Copilot typically interacts with this library. ([Hackage](https://hackage.haskell.org/package/copilot-language)) From 72b00dadd96170c7908bb8faf68a5b9812582bf4 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 9 Nov 2022 18:37:10 +0000 Subject: [PATCH 10/31] Update news for Copilot 3.12. Refs #44. --- home.md | 49 ++++++++++++++++++++++++++++++++----------------- 1 file changed, 32 insertions(+), 17 deletions(-) diff --git a/home.md b/home.md index 80d62db..d35d97c 100644 --- a/home.md +++ b/home.md @@ -1,7 +1,7 @@ ## News -**Release 3.11 -- 2022-09-07** +**Release 3.12 -- 2022-11-07** -We are pleased to announce the release of Copilot 3.11, a stream-based DSL for +We are pleased to announce the release of Copilot 3.12, 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,21 +10,36 @@ clocks and voting algorithms. Among others, Copilot has been used at the Safety Critical Avionics Systems Branch of NASA Langley Research Center for monitoring test flights of drones. -This new release introduces a new library copilot-interpreter that exposes the -functions related to the interpreter backend, pre-existing functions included -as part of copilot-core are now deprecated. It also fixes multiple bugs, -removes deprecated elements, hides internal parts of the implementation from -the public API, and improves the codebase by re-implementing a function without -the use of unsafeCoerce. This release also continues to use our new software -engineering process designed to meet the requirements to obtain NASA's Class D -software classification. Details are available -[here](https://github.com/Copilot-Language/copilot/milestone/15?closed=1). - -Current emphasis is on facilitating the use with other systems, improving the -codebase in terms of stability and test coverage, removing unnecessary -dependencies, hiding internal definitions, and formatting the code to meet our -new coding standards. Users are encouraged to participate by opening issues and -asking questions via our [github +The main changes in this release are as follows: + +- A new library `copilot-prettyprinter` exposes functions related to the + Copilot Core pretty-printing backend. Pre-existing functions included as + part of `copilot-core` are now deprecated. +- The C99 backend now produces an additional header file with struct + declarations. This file is used by the C implementation file generated by + Copilot to define structs before the declarations of the handlers, avoiding + potential forward declarations that the C compiler cannot resolve. Users of + Copilot can choose to import the same new type declaration header file before + the standard Copilot header file in their hand-written code, or use external + definitions that declare compatible structs. Note that, in the former case, + the header file that declares the structs must be included *before* the + header file that declares the externs, handlers and step function. +- The custom type equality module in `copilot-core` is now deprecated in favor + of the definition of type equality in `base`. +- `copilot-theorem` now includes support for proofs by bisimulation necessary + for future extensions to Copilot. +- `copilot-core` now complies with the coding rules established as part of the + process of compliance with NASA's Class D requirements (NPR 7150.2). + +This release also continues to use our new software engineering process +designed to meet the requirements to obtain NASA's Class D software +classification. Details are available +[here](https://github.com/Copilot-Language/copilot/milestone/16?closed=1). + +Current emphasis is on improving the codebase in terms of stability and test +coverage, removing unnecessary dependencies, hiding internal definitions, and +formatting the code to meet our new coding standards. Users are encouraged to +participate by opening issues and asking questions via our [github repo](https://github.com/copilot-language/copilot). ## Licence From 2dba464b91212fa9ab7f0efc75e588cafce4af2b Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 10 Jan 2023 08:21:49 +0000 Subject: [PATCH 11/31] Update news for Copilot 3.13. Refs #45. --- home.md | 25 ++++--------------------- 1 file changed, 4 insertions(+), 21 deletions(-) diff --git a/home.md b/home.md index d35d97c..577e987 100644 --- a/home.md +++ b/home.md @@ -1,5 +1,5 @@ ## News -**Release 3.12 -- 2022-11-07** +**Release 3.13 -- 2023-01-07** We are pleased to announce the release of Copilot 3.12, a stream-based DSL for writing and monitoring embedded C programs, with an emphasis on correctness and @@ -10,26 +10,9 @@ clocks and voting algorithms. Among others, Copilot has been used at the Safety Critical Avionics Systems Branch of NASA Langley Research Center for monitoring test flights of drones. -The main changes in this release are as follows: - -- A new library `copilot-prettyprinter` exposes functions related to the - Copilot Core pretty-printing backend. Pre-existing functions included as - part of `copilot-core` are now deprecated. -- The C99 backend now produces an additional header file with struct - declarations. This file is used by the C implementation file generated by - Copilot to define structs before the declarations of the handlers, avoiding - potential forward declarations that the C compiler cannot resolve. Users of - Copilot can choose to import the same new type declaration header file before - the standard Copilot header file in their hand-written code, or use external - definitions that declare compatible structs. Note that, in the former case, - the header file that declares the structs must be included *before* the - header file that declares the externs, handlers and step function. -- The custom type equality module in `copilot-core` is now deprecated in favor - of the definition of type equality in `base`. -- `copilot-theorem` now includes support for proofs by bisimulation necessary - for future extensions to Copilot. -- `copilot-core` now complies with the coding rules established as part of the - process of compliance with NASA's Class D requirements (NPR 7150.2). +This release fixes 4 bugs in `copilot-core` and `copilot-c99`. We have also +removed 2 deprecated modules and one dependency. The new release has been +published on hackage, as well as github. This release also continues to use our new software engineering process designed to meet the requirements to obtain NASA's Class D software From c39a80b59cc4e5e51ae203b1d1b2c882e7a08716 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 10 Jan 2023 08:26:23 +0000 Subject: [PATCH 12/31] Fix link to Copilot 3.13 milestone. Refs #46. --- home.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/home.md b/home.md index 577e987..ab4f942 100644 --- a/home.md +++ b/home.md @@ -17,7 +17,7 @@ published on hackage, as well as github. This release also continues to use our new software engineering process designed to meet the requirements to obtain NASA's Class D software classification. Details are available -[here](https://github.com/Copilot-Language/copilot/milestone/16?closed=1). +[here](https://github.com/Copilot-Language/copilot/milestone/17?closed=1). Current emphasis is on improving the codebase in terms of stability and test coverage, removing unnecessary dependencies, hiding internal definitions, and From 64f8b158c9371350cd9a1ef1056519b9815e59c1 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 8 Mar 2023 17:54:44 +0000 Subject: [PATCH 13/31] Update version of Copilot available, and GHC needed. Refs #43. --- download.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/download.md b/download.md index f0d845c..4620e7b 100644 --- a/download.md +++ b/download.md @@ -1,7 +1,7 @@ # Download & Installing Copilot is implemented as a Embedded Domain Specific Language in Haskell. -Currently Copilot 3.1 requires a version of the Glasgow Haskell Compiler (GHC) -of at least 8.0 to be installed. The recommended way to do this is by +Currently Copilot 3.14 requires a version of the Glasgow Haskell Compiler (GHC) +of at least 8.6 to be installed. The recommended way to do this is by installing the [Haskell Platform](https://www.haskell.org/platform/). The Haskell platform comes with the compiler and basic tools necessary to install Copilot. From 243fce0b4a88382bd74045e6b9d04925856920a2 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 8 Mar 2023 18:00:23 +0000 Subject: [PATCH 14/31] Update news for Copilot 3.14. Refs #47. --- home.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/home.md b/home.md index ab4f942..e5e88d8 100644 --- a/home.md +++ b/home.md @@ -10,8 +10,8 @@ clocks and voting algorithms. Among others, Copilot has been used at the Safety Critical Avionics Systems Branch of NASA Langley Research Center for monitoring test flights of drones. -This release fixes 4 bugs in `copilot-core` and `copilot-c99`. We have also -removed 2 deprecated modules and one dependency. The new release has been +This release removes deprecated definitions, provides support for GHC 9.4 and +What4 1.4, and includes a much improved README. The new release has been published on hackage, as well as github. This release also continues to use our new software engineering process From 128bf59f3e3af3b67815083bb420dea090c0b9a8 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 22 May 2023 01:46:37 +0000 Subject: [PATCH 15/31] Update news for Copilot 3.15. Refs #49. --- home.md | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/home.md b/home.md index e5e88d8..a8ca0b7 100644 --- a/home.md +++ b/home.md @@ -1,7 +1,7 @@ ## News -**Release 3.13 -- 2023-01-07** +**Release 3.15 -- 2023-05-07** -We are pleased to announce the release of Copilot 3.12, a stream-based DSL for +We are pleased to announce the release of Copilot 3.15, 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,9 +10,8 @@ clocks and voting algorithms. Among others, Copilot has been used at the Safety Critical Avionics Systems Branch of NASA Langley Research Center for monitoring test flights of drones. -This release removes deprecated definitions, provides support for GHC 9.4 and -What4 1.4, and includes a much improved README. The new release has been -published on hackage, as well as github. +This is a maintenance release that removes deprecated definitions. The new +release has been published on hackage, as well as github. This release also continues to use our new software engineering process designed to meet the requirements to obtain NASA's Class D software From 51b0bb5846664b1b40a5f99b4b813efcd9f54c24 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 8 Jul 2023 19:45:22 +0000 Subject: [PATCH 16/31] Remove tabs. Refs #51. --- tpl/default | 34 +++++++++++------------ tpl/home | 78 ++++++++++++++++++++++++++--------------------------- 2 files changed, 56 insertions(+), 56 deletions(-) diff --git a/tpl/default b/tpl/default index e9cad31..f68b53c 100755 --- a/tpl/default +++ b/tpl/default @@ -3,22 +3,22 @@ cat < - - Copilot: $TITLE - - - - -
- - -
- $CONTENT -
-
- + + Copilot: $TITLE + + + + +
+ + +
+ $CONTENT +
+
+ ! diff --git a/tpl/home b/tpl/home index fadb881..8269f14 100644 --- a/tpl/home +++ b/tpl/home @@ -3,38 +3,38 @@ cat < - - Copilot: $TITLE - - - - - -
- - -
-
-

- Copilot is a realtime programming language and Runtime Verification - framework. It allows users to write concise programs in a simple - but powerful way using a stream-based approach. -

-

- Programs can be interpreted for testing, or translated C99 code to be - incorporated in a project, or as a standalone application. The C99 - backend ensures us that the output is constant in memory and time, - making it suitable for systems with hard realtime requirements. -

-

- Learn more about the project... -

-
-
- 
-- Raw temperature from sensor, range -50.0C to 100.0C.
+    
+        Copilot: $TITLE
+        
+        
+        
+        
+    
+        

+            
+            
+            

+                

+                    

+                        Copilot is a realtime programming language and Runtime Verification
+                        framework.  It allows users to write concise programs in a simple
+                        but powerful way using a stream-based approach.
+                    

+                    

+                        Programs can be interpreted for testing, or translated C99 code to be
+                        incorporated in a project, or as a standalone application. The C99
+                        backend ensures us that the output is constant in memory and time,
+                        making it suitable for systems with hard realtime requirements.
+                    

+                    

+                        Learn more about the project...
+                    

+                

+                

+                    
-- Raw temperature from sensor, range -50.0C to 100.0C.
 temp :: Stream Word8
 temp = extern "temperature" Nothing
 
@@ -46,12 +46,12 @@ ctemp = (unsafeCast temp) * (150.0 / "heaton"  (ctemp < 18.0) [arg ctemp]
   trigger "heatoff" (ctemp > 21.0) [arg ctemp]

-				

-			

-			

-				$CONTENT
-			

-		

-	
+
+
+
+ $CONTENT +
+
+ ! From 2dabefa74478bba4275b30cf876d3ac7c605c4a4 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 8 Jul 2023 19:47:01 +0000 Subject: [PATCH 17/31] Update news for Copilot 3.16. Refs #50. --- home.md | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/home.md b/home.md index a8ca0b7..8a03c4a 100644 --- a/home.md +++ b/home.md @@ -1,7 +1,7 @@ ## News -**Release 3.15 -- 2023-05-07** +**Release 3.16 -- 2023-07-07** -We are pleased to announce the release of Copilot 3.15, a stream-based DSL for +We are pleased to announce the release of Copilot 3.16, 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,13 +10,16 @@ clocks and voting algorithms. Among others, Copilot has been used at the Safety Critical Avionics Systems Branch of NASA Langley Research Center for monitoring test flights of drones. -This is a maintenance release that removes deprecated definitions. The new -release has been published on hackage, as well as github. +This release introduces two important changes. The first is a battery of tests +for the C99 backend. This contribution is a key component towards meeting the +requirements of NASA's Procedural Requirements for Research and Technology +Software. The second is a breaking change in copilot-language: a type has moved +modules. -This release also continues to use our new software engineering process -designed to meet the requirements to obtain NASA's Class D software -classification. Details are available -[here](https://github.com/Copilot-Language/copilot/milestone/17?closed=1). +Details are available +[here](https://github.com/Copilot-Language/copilot/milestone/20?closed=1) +and +[here](https://github.com/Copilot-Language/copilot/releases/tag/v3.16). Current emphasis is on improving the codebase in terms of stability and test coverage, removing unnecessary dependencies, hiding internal definitions, and From 9adccb220006acaab9f70c8fc8f72d524b992cd5 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 9 Nov 2023 07:58:18 +0000 Subject: [PATCH 18/31] Americanize the spelling of license. Refs #53. This commit replaces all occurrences of the word licence (British spelling) with license (American spelling). --- home.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/home.md b/home.md index 8a03c4a..b16221a 100644 --- a/home.md +++ b/home.md @@ -27,8 +27,8 @@ formatting the code to meet our new coding standards. Users are encouraged to participate by opening issues and asking questions via our [github repo](https://github.com/copilot-language/copilot). -## Licence -Copilot is distributed under the BSD-3-Clause licence, which can be found +## License +Copilot is distributed under the BSD-3-Clause license, which can be found [here](https://raw.githubusercontent.com/Copilot-Language/Copilot/master/LICENSE). ## Acknowledgements From 79836f72886be300551a7a3b6b5f7d9b091f9660 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 9 Nov 2023 07:58:32 +0000 Subject: [PATCH 19/31] Update news for Copilot 3.17. Refs #52. --- home.md | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/home.md b/home.md index b16221a..6cba1a9 100644 --- a/home.md +++ b/home.md @@ -1,7 +1,7 @@ ## News -**Release 3.16 -- 2023-07-07** +**Release 3.17 -- 2023-11-07** -We are pleased to announce the release of Copilot 3.16, a stream-based DSL for +We are pleased to announce the release of Copilot 3.17, 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,22 +10,22 @@ clocks and voting algorithms. Among others, Copilot has been used at the Safety Critical Avionics Systems Branch of NASA Langley Research Center for monitoring test flights of drones. -This release introduces two important changes. The first is a battery of tests -for the C99 backend. This contribution is a key component towards meeting the -requirements of NASA's Procedural Requirements for Research and Technology -Software. The second is a breaking change in copilot-language: a type has moved -modules. +This release introduces compatibility with what4 versions up to 1.5.1, and +replaces several functions in `copilot-core`. The second change is a breaking +change: the functions replaced have been deprecated and new alternatives +introduced instead. Details are available -[here](https://github.com/Copilot-Language/copilot/milestone/20?closed=1) +[here](https://github.com/Copilot-Language/copilot/milestone/22?closed=1) and -[here](https://github.com/Copilot-Language/copilot/releases/tag/v3.16). +[here](https://github.com/Copilot-Language/copilot/releases/tag/v3.17). Current emphasis is on improving the codebase in terms of stability and test coverage, removing unnecessary dependencies, hiding internal definitions, and -formatting the code to meet our new coding standards. Users are encouraged to -participate by opening issues and asking questions via our [github -repo](https://github.com/copilot-language/copilot). +formatting the code to meet our new coding standards. Upcoming releases will +focus on introducing tests for `copilot-theorem` and `copilot-libraries`. Users +are encouraged to participate by opening issues and asking questions via our +[github repo](https://github.com/copilot-language/copilot). ## License Copilot is distributed under the BSD-3-Clause license, which can be found From b53e8a33d7f7e9fae50790339998b5e53f78a3f1 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 10 Dec 2023 13:56:46 +0000 Subject: [PATCH 20/31] Automate page generation process. Refs #54. This commit automates the page generation process by: - Introducing a script that will generate the html pages under _site/ from the markdown files. - Adjusting the Makefile to make use of such script. - Moving all static files into _site/ - Adjusting the templates to be plain files, as opposed to scripts. - Adjusting the permissions of the templates to disable the executable bit. --- Makefile | 39 ++++++++++-------- .../downloads}/copilot_tutorial.pdf | Bin haskell.css => _site/haskell.css | 0 home.css => _site/home.css | 0 style.css => _site/style.css | 0 compile.sh | 9 ++++ nav | 8 ++++ tpl/default | 4 -- tpl/home | 20 ++++----- 9 files changed, 48 insertions(+), 32 deletions(-) rename {downloads => _site/downloads}/copilot_tutorial.pdf (100%) rename haskell.css => _site/haskell.css (100%) rename home.css => _site/home.css (100%) rename style.css => _site/style.css (100%) create mode 100755 compile.sh create mode 100644 nav mode change 100755 => 100644 tpl/default diff --git a/Makefile b/Makefile index d19756f..b41abbd 100644 --- a/Makefile +++ b/Makefile @@ -1,21 +1,26 @@ -MAP=map -OUT=html -TEMPLATE=tpl/default +.PHONY: all -include Makefile.base +all: _site/about.html \ + _site/contact.html \ + _site/documentation.html \ + _site/download.html \ + _site/home.html \ + _site/index.html -publish: all - git add . - git stash - git checkout master - git checkout --theirs stash -- . - git stash drop - git reset . - git clean -df - git clean -df +_site/about.html: about.md + ./compile.sh About $< default -home.html: home.nav home.content tpl/home - web-render tpl/home home home.nav home.content > $@ +_site/contact.html: contact.md + ./compile.sh Contact $< default -index.html: home.html - ln -s $< $@ +_site/documentation.html: documentation.md + ./compile.sh Documentation $< default + +_site/download.html: download.md + ./compile.sh Download $< default + +_site/home.html: home.md + ./compile.sh Home $< home + +_site/index.html: _site/home.html + cp $< $@ diff --git a/downloads/copilot_tutorial.pdf b/_site/downloads/copilot_tutorial.pdf similarity index 100% rename from downloads/copilot_tutorial.pdf rename to _site/downloads/copilot_tutorial.pdf diff --git a/haskell.css b/_site/haskell.css similarity index 100% rename from haskell.css rename to _site/haskell.css diff --git a/home.css b/_site/home.css similarity index 100% rename from home.css rename to _site/home.css diff --git a/style.css b/_site/style.css similarity index 100% rename from style.css rename to _site/style.css diff --git a/compile.sh b/compile.sh new file mode 100755 index 0000000..26eee40 --- /dev/null +++ b/compile.sh @@ -0,0 +1,9 @@ +#!/bin/bash + +TITLE="$1" +NAV="$(cat nav)" +CONTENT="$(pandoc $2 -t html)" +TARGET="_site/$(basename $2 .md).html" +TEMPLATE="$3" +mkdir -p _site/ +env TITLE="$TITLE" NAV="$NAV" CONTENT="$CONTENT" envsubst '${TITLE}':'${NAV}':'${CONTENT}' < tpl/$TEMPLATE > $TARGET diff --git a/nav b/nav new file mode 100644 index 0000000..e12e9b5 --- /dev/null +++ b/nav @@ -0,0 +1,8 @@ +

+Home +About +Download +Documentation +Contact +Source Code +

diff --git a/tpl/default b/tpl/default old mode 100755 new mode 100644 index f68b53c..e82b92c --- a/tpl/default +++ b/tpl/default @@ -1,6 +1,3 @@ -#!/bin/sh - -cat < @@ -21,4 +18,3 @@ cat < -! diff --git a/tpl/home b/tpl/home index 8269f14..c50ead7 100644 --- a/tpl/home +++ b/tpl/home @@ -1,6 +1,3 @@ -#!/bin/sh - -cat < @@ -15,7 +12,9 @@ cat <Copilot Realtime Programming Language and Runtime Verification Framework - +

@@ -46,12 +45,11 @@ ctemp = (unsafeCast temp) * (150.0 / "heaton" (ctemp < 18.0) [arg ctemp] trigger "heatoff" (ctemp > 21.0) [arg ctemp] -

-
-
- $CONTENT -
- + +
+ $CONTENT +
+ + -! From a53a04d1fce396dcc40e1a7146cc7fc0b7ba443e Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 10 Dec 2023 13:59:13 +0000 Subject: [PATCH 21/31] Remove files no longer needed by page generation script. Refs #54. This commit removes older files that were not being used and will no longer be used to generate the website. --- Makefile.base | 19 ------------------- map | 6 ------ 2 files changed, 25 deletions(-) delete mode 100644 Makefile.base delete mode 100644 map diff --git a/Makefile.base b/Makefile.base deleted file mode 100644 index 34572e4..0000000 --- a/Makefile.base +++ /dev/null @@ -1,19 +0,0 @@ -HTML=$(shell awk '$$1 == "T" {print $$2}' $(MAP)) - -all: $(HTML) - -%.nav: $(MAP) - web-nav $^ | markdown > $@ - -%.content: %.md - markdown $^ > $@ - -%.html: %.nav %.content $(TEMPLATE) - web-render $(TEMPLATE) $* $*.nav $*.content > $@ - -clean: - rm -f $(HTML) - rm -f $(HTML:.html=.nav) - rm -f $(HTML:.html=.content) - -.PHONY: clean diff --git a/map b/map deleted file mode 100644 index 98546b5..0000000 --- a/map +++ /dev/null @@ -1,6 +0,0 @@ -T home.html Home -T about.html About -T download.html Download -T documentation.html Documentation -T contact.html Contact -L https://github.com/copilot-language/copilot Source Code From 466a3085155b1ca0e82148e7fdac11f0bb1824da Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 10 Dec 2023 13:59:52 +0000 Subject: [PATCH 22/31] Add page build and publication action. Refs #54. Add a github actions job that will compile and generate the page directly from the markdown source. --- .github/workflows/publish.yml | 43 +++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) create mode 100644 .github/workflows/publish.yml diff --git a/.github/workflows/publish.yml b/.github/workflows/publish.yml new file mode 100644 index 0000000..52cd929 --- /dev/null +++ b/.github/workflows/publish.yml @@ -0,0 +1,43 @@ +name: Publish web +on: + push: + +jobs: + build: + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@v4 + + - name: Setup Pages + id: pages + uses: actions/configure-pages@v3 + + - name: Install pandoc + run: | + sudo apt-get install --yes pandoc + + - name: Build with Pandoc + run: | + make + + - name: Upload artifact + uses: actions/upload-pages-artifact@v2 + + deploy: + permissions: + contents: read + pages: write + id-token: write + + runs-on: ubuntu-latest + + needs: build + + environment: + name: github-pages + url: ${{steps.deployment.outputs.page_url}} + steps: + - name: Deploy artifact + id: deployment + uses: actions/deploy-pages@v1 From 227e095e855f024d1f36c3825b8581eac63394b3 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 8 Mar 2024 14:17:03 +0000 Subject: [PATCH 23/31] Update news for Copilot 3.18.1. Refs #55. --- home.md | 34 +++++++++++++++++++--------------- 1 file changed, 19 insertions(+), 15 deletions(-) diff --git a/home.md b/home.md index 6cba1a9..5cf95e1 100644 --- a/home.md +++ b/home.md @@ -1,30 +1,34 @@ ## News -**Release 3.17 -- 2023-11-07** +**Release 3.18.1 -- 2024-01-07** -We are pleased to announce the release of Copilot 3.17, 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), -clocks and voting algorithms. +We are pleased to announce the release of Copilot 3.18.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), clocks and voting algorithms. Among others, Copilot has been used at the Safety Critical Avionics Systems Branch of NASA Langley Research Center for monitoring test flights of drones. -This release introduces compatibility with what4 versions up to 1.5.1, and -replaces several functions in `copilot-core`. The second change is a breaking -change: the functions replaced have been deprecated and new alternatives -introduced instead. +This release updates the C backend so that the code produced complies with +MISRA C, and introduces testing infrastructure for `copilot-libraries` and +`copilot-theorem`. We also , fix an issue with how arrays are generated +internally when used as arguments to triggers, introduce compatibility with GHC +9.6, and introduce a new function `forAll` to void clashes with the language +keyword `forall`, which will be needed to be compatible with GHC >= 9.8 in +future versions. Details are available -[here](https://github.com/Copilot-Language/copilot/milestone/22?closed=1) +[here](https://github.com/Copilot-Language/copilot/milestone/24?closed=1), +[here](https://github.com/Copilot-Language/copilot/milestone/23?closed=1) and -[here](https://github.com/Copilot-Language/copilot/releases/tag/v3.17). +[here](https://github.com/Copilot-Language/copilot/releases/tag/v3.18.1). Current emphasis is on improving the codebase in terms of stability and test coverage, removing unnecessary dependencies, hiding internal definitions, and -formatting the code to meet our new coding standards. Upcoming releases will -focus on introducing tests for `copilot-theorem` and `copilot-libraries`. Users -are encouraged to participate by opening issues and asking questions via our +formatting the code to meet our new coding standards. We also plan to add +extensions to the language to be able to updates arrays and structs. Users are +encouraged to participate by opening issues and asking questions via our [github repo](https://github.com/copilot-language/copilot). ## License From 4db79176cedccb47fcdb63f0624287d1a0fe64be Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 8 Mar 2024 14:23:35 +0000 Subject: [PATCH 24/31] Update news for Copilot 3.19. Refs #56. --- home.md | 21 ++++++++------------- 1 file changed, 8 insertions(+), 13 deletions(-) diff --git a/home.md b/home.md index 5cf95e1..2e422e2 100644 --- a/home.md +++ b/home.md @@ -1,28 +1,23 @@ ## News -**Release 3.18.1 -- 2024-01-07** +**Release 3.19 -- 2024-03-07** -We are pleased to announce the release of Copilot 3.18.1, a stream-based DSL +We are pleased to announce the release of Copilot 3.19, 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), clocks and voting algorithms. -Among others, Copilot has been used at the Safety Critical Avionics Systems +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 updates the C backend so that the code produced complies with -MISRA C, and introduces testing infrastructure for `copilot-libraries` and -`copilot-theorem`. We also , fix an issue with how arrays are generated -internally when used as arguments to triggers, introduce compatibility with GHC -9.6, and introduce a new function `forAll` to void clashes with the language -keyword `forall`, which will be needed to be compatible with GHC >= 9.8 in -future versions. +This release drastically increases the test coverage of `copilot-core`. We also +remove deprecated functions from `copilot-core` that had been renamed in prior +versions to comply with our style guide. Details are available -[here](https://github.com/Copilot-Language/copilot/milestone/24?closed=1), -[here](https://github.com/Copilot-Language/copilot/milestone/23?closed=1) +[here](https://github.com/Copilot-Language/copilot/milestone/25?closed=1), and -[here](https://github.com/Copilot-Language/copilot/releases/tag/v3.18.1). +[here](https://github.com/Copilot-Language/copilot/releases/tag/v3.19). Current emphasis is on improving the codebase in terms of stability and test coverage, removing unnecessary dependencies, hiding internal definitions, and From 5bf6844189a6c56a33aaeaf9cf5ee2d6b7c0046b Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 8 Jul 2024 03:56:24 +0000 Subject: [PATCH 25/31] Update news for Copilot 3.20. Refs #57. --- home.md | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/home.md b/home.md index 2e422e2..d1b4c01 100644 --- a/home.md +++ b/home.md @@ -1,7 +1,7 @@ ## News -**Release 3.19 -- 2024-03-07** +**Release 3.20 -- 2024-07-07** -We are pleased to announce the release of Copilot 3.19, a stream-based DSL +We are pleased to announce the release of Copilot 3.20, 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 @@ -10,21 +10,22 @@ MTL), 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 drastically increases the test coverage of `copilot-core`. We also -remove deprecated functions from `copilot-core` that had been renamed in prior -versions to comply with our style guide. +This release introduces support to upload the values of fields in structs, and +add support for GHC 9.8. We also remove deprecated functions from +`copilot-language` that had been renamed in prior versions for compatibility +with newer versions of GHC. Details are available -[here](https://github.com/Copilot-Language/copilot/milestone/25?closed=1), +[here](https://github.com/Copilot-Language/copilot/milestone/27?closed=1), and -[here](https://github.com/Copilot-Language/copilot/releases/tag/v3.19). - -Current emphasis is on improving the codebase in terms of stability and test -coverage, removing unnecessary dependencies, hiding internal definitions, and -formatting the code to meet our new coding standards. We also plan to add -extensions to the language to be able to updates arrays and structs. Users are -encouraged to participate by opening issues and asking questions via our -[github repo](https://github.com/copilot-language/copilot). +[here](https://github.com/Copilot-Language/copilot/releases/tag/v3.20). + +Current emphasis is on introducing support to update the values of elements in +arrays, improving the codebase in test coverage, removing unnecessary +dependencies, hiding internal definitions, and formatting the code to meet our +new coding standards. We also plan to add extensions to be able to visualize +streams. Users are encouraged to participate by opening issues and asking +questions via our [github repo](https://github.com/copilot-language/copilot). ## License Copilot is distributed under the BSD-3-Clause license, which can be found From 5a8e110c53947d06cb54a090303cc5c613273356 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 8 Jan 2025 03:22:02 +0000 Subject: [PATCH 26/31] Update news for Copilot 4.2. Refs #58. --- home.md | 71 ++++++++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 53 insertions(+), 18 deletions(-) diff --git a/home.md b/home.md index d1b4c01..f70d794 100644 --- a/home.md +++ b/home.md @@ -1,33 +1,68 @@ ## News -**Release 3.20 -- 2024-07-07** +**Release 4.2 -- 2025-01-07** -We are pleased to announce the release of Copilot 3.20, 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), clocks and voting algorithms. +We are pleased to announce the release of Copilot 4.2, 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), +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 support to upload the values of fields in structs, and -add support for GHC 9.8. We also remove deprecated functions from -`copilot-language` that had been renamed in prior versions for compatibility -with newer versions of GHC. +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 + the public interface. + +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 with the Stackage Nightly. + +This release has been made possible thanks to key submissions from Frank Dedden +(@fdedden), Ryan Scott (@RyanGlScott), and Kyle Beech (@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. Details are available -[here](https://github.com/Copilot-Language/copilot/milestone/27?closed=1), +[here](https://github.com/Copilot-Language/copilot/milestone/30?closed=1), and -[here](https://github.com/Copilot-Language/copilot/releases/tag/v3.20). +[here](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. -Current emphasis is on introducing support to update the values of elements in -arrays, improving the codebase in test coverage, removing unnecessary -dependencies, hiding internal definitions, and formatting the code to meet our -new coding standards. We also plan to add extensions to be able to visualize -streams. Users are encouraged to participate by opening issues and asking -questions via our [github repo](https://github.com/copilot-language/copilot). +We want to remind the community that Copilot is now accepting code +contributions from external participants again. Please see the discussions and +the issues 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 via our [github repo](https://github.com/copilot-language/copilot). ## License + Copilot is distributed under the BSD-3-Clause license, which can be found [here](https://raw.githubusercontent.com/Copilot-Language/Copilot/master/LICENSE). From 8775a49534095ad54c824c6220df5679086d1658 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 8 Jan 2025 03:53:44 +0000 Subject: [PATCH 27/31] Fix typo. Refs #59. --- home.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/home.md b/home.md index f70d794..ba91418 100644 --- a/home.md +++ b/home.md @@ -32,7 +32,7 @@ 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 with the Stackage Nightly. +well as with Stackage Nightly. This release has been made possible thanks to key submissions from Frank Dedden (@fdedden), Ryan Scott (@RyanGlScott), and Kyle Beech (@kaBeech), the last of From 0ee76164a54ba1f288f0146fb4ec939ea1ef24e8 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 8 Jan 2025 18:51:38 +0000 Subject: [PATCH 28/31] Fix typo. Refs #60. --- home.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/home.md b/home.md index ba91418..964020f 100644 --- a/home.md +++ b/home.md @@ -35,7 +35,7 @@ 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 Beech (@kaBeech), the last of +(@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 From 4aae5528134e1a3f474c5efb4a7dc98d5dd49a76 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 28 May 2026 06:36:03 +0000 Subject: [PATCH 29/31] 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 30/31] 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 31/31] 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