From 88c2be9d982a2c6a00add5236e28f3fb55a4871e Mon Sep 17 00:00:00 2001 From: Frank Dedden Date: Tue, 5 May 2020 23:03:48 +0200 Subject: [PATCH 01/30] Replaced old site with new one. Refs #22. All old files were (re)moved, except for the license. --- _config.yml | 4 - about.html | 73 +++++++ contact.html | 83 ++++++++ documentation.html | 70 +++++++ download.html | 51 +++++ .../copilot_tutorial.pdf | Bin haskell.css | 15 ++ home.css | 27 +++ home.html | 73 +++++++ index.md | 179 ------------------ style.css | 156 +++++++++++++++ 11 files changed, 548 insertions(+), 183 deletions(-) delete mode 100644 _config.yml create mode 100644 about.html create mode 100644 contact.html create mode 100644 documentation.html create mode 100644 download.html rename copilot_tutorial.pdf => downloads/copilot_tutorial.pdf (100%) create mode 100644 haskell.css create mode 100644 home.css create mode 100644 home.html delete mode 100644 index.md create mode 100644 style.css diff --git a/_config.yml b/_config.yml deleted file mode 100644 index 9544d23..0000000 --- a/_config.yml +++ /dev/null @@ -1,4 +0,0 @@ -theme: jekyll-theme-minimal - -title: Copilot -description: A stream DSL for writing embedded C programs diff --git a/about.html b/about.html new file mode 100644 index 0000000..94e124d --- /dev/null +++ b/about.html @@ -0,0 +1,73 @@ + + + + Copilot: about + + + + +
+ + +
+

About

+ +

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. Copilot provides a strong type +system that helps keeping programmers from making common mistakes, aiding in +the quality of the code.

+ +

Copilot provides a library providing higher-level constructs, for example for +defining clocks, a Boyer-Moore majority voting implementation and various +temporal logics, including Linear Temporal logic (LTL) and Past Time LTL.

+ +

Code example

+ +

This is a simple example showing basic usage. It implements a home heating +system: It heats when temp gets too low, and stops when it is high enough. It +reads temperature as a byte (range -50C to 100C) and translates this to +Celsius.

+ +
{-# LANGUAGE RebindableSyntax #-}
+
+module Main where
+
+import Language.Copilot
+import Copilot.Compile.C99
+
+-- External temperature as a byte, range of -50C to 100C.
+temp :: Stream Word8
+temp = extern "temperature" Nothing
+
+-- Calculate temperature in Celsius.
+-- We need to cast the Word8 to a Float. Note that it is an unsafeCast, as there
+-- is no direct relation between Word8 and Float.
+ctemp :: Stream Float
+ctemp = (unsafeCast temp) * (150.0 / 255.0) - 50.0
+
+spec = do
+  -- Triggers that fire when the ctemp is too low or too high,
+  -- pass the current ctemp as an argument.
+  trigger "heaton"  (ctemp < 18.0) [arg ctemp]
+  trigger "heatoff" (ctemp > 21.0) [arg ctemp]
+
+-- Compile the spec
+main = reify spec >>= compile "heater"
+
+
+ + diff --git a/contact.html b/contact.html new file mode 100644 index 0000000..354ca4b --- /dev/null +++ b/contact.html @@ -0,0 +1,83 @@ + + + + Copilot: contact + + + + +
+ + +
+

Contact & Help

+ +

Having trouble using Copilot, or encountered a possible bug? Asking questions +or reporting bugs can both be done through the issue tracker at GitHub. This +helps us keep track of open bugs and problems, and allows us to easily comment +and discuss the issue.

+ +

As Copilot consists of several packages, each of them comes with its own issue +tracker. If you have a question about a specific package or encountered a +problem specific to a package, please report the problem at that package, if +possible. In all other cases, please refer to the issue tracker of the general +Copilot package:

+ + + + +

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 Frank Dedden dev@dedden.net.

+ +

Copilot developers

+ +

Copilot is currently developed and maintained by Frank Dedden. Alwyn Goodloe +and Ivan Perez provide helpful feedback on the usage of Copilot at NASA +Langley Research Center.

+ +

Previous developers

+ +

The development of Copilot spans across several years. During these years +the following people have helped develop Copilot (in no particular order):

+ +
    +
  • Lee Pike
    • +
  • Alwyn Goodloe
    • +
  • Robin Morisset
    • +
  • Sebastian Niller
    • +
  • Nis Wegmann
    • +
  • Chris Hathhorn
    • +
  • Eli Mendelson
    • +
  • Jonathan Laurent
    • +
  • Laura Titolo
    • +
  • Georges-Axel Jolayan
    • +
  • Macallan Cruff
    • +
  • Ryan Spring
    • +
  • Lauren Pick
    • +
  • Frank Dedden
    • +
  • Ivan Perez
    • +
+
+
+ + diff --git a/documentation.html b/documentation.html new file mode 100644 index 0000000..4f37666 --- /dev/null +++ b/documentation.html @@ -0,0 +1,70 @@ + + + + Copilot: documentation + + + + +
+ + +
+

Documentation

+ +

A manual to Copilot can be downloaded here.

+ +

Copilot comes with a set of examples as part of its distribution, available in +the Examples +directory of +the main repository.

+ +

Structure and Sources

+ +

Apart from the Copilot Github project +page, there are a number of sub-projects +that make up Copilot:

+ +
    +

  • Copilot: The main Copilot package, to which all others are a dependency. +One should install this one to install Copilot. +(Sources) +(Hackage)

    • +

  • copilot-core: The core language, which efficiently represents Copilot +expressions. The core is only of interest to implementers wishing to add a +new back-end to Copilot. +(Sources) +(Hackage)

    • +

  • copilot-language: The front-end of Copilot defining the user language. A +user of Copilot typically interacts with this library. +(Sources) +(Hackage)

    • +

  • copilot-libraries: User-supplied libraries for Copilot, including +linear-temporal logic, fault-tolerant voting, regular expressions, etc. +(Sources) +(Hackage)

    • +

  • copilot-c99: A backend writing hard realtime C99 code. It writes +readable output and ensures the output code is constant in memory and time. +(Sources) +(Hackage)

    • +

  • copilot-theorem: Some tools to prove properties on Copilot. +(Sources) +(Hackage)

    • +
+ + +

Additionally there is a specific repository that lists most of the papers and +articles written on Copilot: +copilot-discussion.

+
+
+ + diff --git a/download.html b/download.html new file mode 100644 index 0000000..0dc3b87 --- /dev/null +++ b/download.html @@ -0,0 +1,51 @@ + + + + Copilot: download + + + + +
+ + +
+

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 +installing the Haskell Platform. The +Haskell platform comes with the compiler and basic tools necessary to install +Copilot.

+ +

With a newly installed Haskell environment, we can easily install the latest +version of Copilot. As a regular user, just execute the following two commands +from the command line:

+ +
cabal update
+cabal install copilot
+
+ +

These commands first update the list of known packages, and secondly install +the latest available version of Copilot and all of its dependencies.

+ +

After these commands successfully finish, Copilot is installed and ready to +use.

+ +

Sources

+ +

The source code to Copilot can be found at our GitHub +project page.

+
+
+ + diff --git a/copilot_tutorial.pdf b/downloads/copilot_tutorial.pdf similarity index 100% rename from copilot_tutorial.pdf rename to downloads/copilot_tutorial.pdf diff --git a/haskell.css b/haskell.css new file mode 100644 index 0000000..2115ca4 --- /dev/null +++ b/haskell.css @@ -0,0 +1,15 @@ +.language-haskell mark.comment { + color: grey; +} + +.language-haskell mark.string { + color: orangered; +} + +.language-haskell mark.literal { + color: darkgreen; +} + +.language-haskell mark.keyword { + color: blue; +} diff --git a/home.css b/home.css new file mode 100644 index 0000000..11188ea --- /dev/null +++ b/home.css @@ -0,0 +1,27 @@ +#panel { + background: #764B8E; + padding: 2em; + + display: grid; + grid-template-columns: 1fr 1fr; + grid-gap: 2em; +} + +#panel p { + color: white; + text-shadow: 1px 1px black; +} + +#panel a { + color: inherit; +} + +#panel pre { + background: #222; + color: white; + padding: .5em; +} + +#panel .language-haskell mark.literal { + color: greenyellow; +} diff --git a/home.html b/home.html new file mode 100644 index 0000000..171c84c --- /dev/null +++ b/home.html @@ -0,0 +1,73 @@ + + + + Copilot: home + + + + + +
+ + +
+
+

+ 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.0 to 150.0.
+temp :: Stream Word8
+temp = extern "temperature" Nothing
+
+-- Transform the temperature to Celsius.
+ctemp :: Stream Float
+ctemp = (unsafeCast temp) * (150.0 / 255.0) - 50.0
+
+-- Bind two triggers with a 3.0C hysteresis.
+spec = do
+  trigger "heaton"  (ctemp < 18.0) [arg ctemp]
+  trigger "heatoff" (ctemp > 21.0) [arg ctemp]
+
+
+
+

Licence

+ +

Copilot is distributed under the BSD-3-Clause licence, which can be found +here.

+ +

Acknowledgements

+ +

We are grateful for NASA Contract NNL08AD13T to Galois, Inc. and the National +Institute of Aerospace, which partially supported this work.

+ +

Additionally NASA Langley contracts 80LARC17C0004 and NNL09AA00A supported +further development of Copilot.

+ +

We would like to thank Kaveh Darafsheh (NASA Langley Research Center) for his +help with testing Copilot. In addition numerous people have helped with smaller +things, reporting bugs etc. Thanks to all of them!

+
+
+ + diff --git a/index.md b/index.md deleted file mode 100644 index 0ea0f7c..0000000 --- a/index.md +++ /dev/null @@ -1,179 +0,0 @@ -## Introduction -Copilot is a runtime verification framework written in Haskell. It allows the -user to write 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. - - -## Installation - -Currently the Copilot 3.0 release requires GHC 8.0 or higher. - -Copilot is available from -[Hackage](https://hackage.haskell.org/package/copilot), and the latest version -can be installed easily: - - cabal install copilot - -Alternatively one can download and install it from the repositories as well: - - git clone https://github.com/Copilot-Language/copilot.git - cd copilot - git submodule update --init --remote - - Compiling can either be done in a Nix-style build, or a traditional one: - - _Nix-Style build (Cabal >= 2.x)_ - - cabal build # For Cabal 3.x - cabal v2-build # For Cabal 2.x - - _Traditional build (Cabal 1.x)_ - - cabal install --dependencies-only - cabal build - -Typically one would only go this route to develop Copilot. For regular users -the cabal method is highly recommended. - - -## Example -Here follows a simple example of a heating system. Other examples can be found -in the [Examples -directory](https://github.com/Copilot-Language/Copilot/tree/master/Examples) -of the main repository. - - -- This is a simple example with basic usage. It implements a simple home - -- heating system: It heats when temp gets too low, and stops when it is high - -- enough. It read temperature as a byte (range -50C to 100C) and translates - -- this to Celcius. - - module Heater where - - import Language.Copilot - import Copilot.Compile.C99 - - import Prelude hiding ((>), (<), div) - - -- External temperature as a byte, range of -50C to 100C - temp :: Stream Word8 - temp = extern "temperature" Nothing - - -- Calculate temperature in Celcius. - -- We need to cast the Word8 to a Float. Note that it is an unsafeCast, as there - -- is no direct relation between Word8 and Float. - ctemp :: Stream Float - ctemp = (unsafeCast temp) * (150.0 / 255.0) - 50.0 - - spec = do - -- Triggers that fire when the ctemp is too low or too high, - -- pass the current ctemp as an argument. - trigger "heaton" (ctemp < 18.0) [arg ctemp] - trigger "heatoff" (ctemp > 21.0) [arg ctemp] - - -- Compile the spec - main = reify spec >>= compile "heater" - - -## Documentation -A manual to Copilot can be downloaded [here](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 -the main repository. - - -## Structure and Sources -Apart from the Copilot [Github project -page](https://github.com/Copilot-Language), there are a number of sub-projects -that make up Copilot: - -- `Copilot`: The main Copilot package, to which all others are a dependency. - One should install this one to install Copilot. - ([Sources](https://github.com/Copilot-Language/Copilot)) - ([Hackage](https://hackage.haskell.org/package/copilot)) - -- `copilot-core`: The core language, which efficiently represents Copilot - expressions. The core is only of interest to implementers wishing to add a - new back-end to Copilot. - ([Sources](https://github.com/Copilot-Language/copilot-core)) - ([Hackage](https://hackage.haskell.org/package/copilot-core)) - -- `copilot-language`: The front-end of Copilot defining the user language. A - user of Copilot typically interacts with this library. - ([Sources](https://github.com/Copilot-Language/copilot-language)) - ([Hackage](https://hackage.haskell.org/package/copilot-language)) - -- `copilot-libraries`: User-supplied libraries for Copilot, including - linear-temporal logic, fault-tolerant voting, regular expressions, etc. - ([Sources](https://github.com/Copilot-Language/copilot-libraries)) - ([Hackage](https://hackage.haskell.org/package/copilot-libraries)) - -- `copilot-c99`: A backend writing hard realtime C99 code. It writes - readable output and ensures the output code is constant in memory and time. - ([Sources](https://github.com/Copilot-Language/copilot-c99)) - ([Hackage](https://hackage.haskell.org/package/copilot-c99)) - -- `copilot-theorem`: Some tools to prove properties on Copilot. - ([Sources](https://github.com/Copilot-Language/copilot-theorem)) - ([Hackage](https://hackage.haskell.org/package/copilot-theorem)) - -Additionally there is a specific repository that lists most of the papers and -articles written on Copilot: -[copilot-discussion](https://github.com/Copilot-Language/copilot-discussion). - - -## Acknowledgements -We are grateful for NASA Contract NNL08AD13T to Galois, Inc. and the National -Institute of Aerospace, which partially supported this work. - -Additionally NASA Langley contracts 80LARC17C0004 and NNL09AA00A supported -further development of Copilot. - -We would like to thank Kaveh Darafsheh (NASA Langley Research Center) for his -help with testing Copilot. - -In addition numerous people have helped with smaller things, reporting bugs -etc. Thanks to all of them! - - -## License -Copilot is distributed under the BSD-3-Clause license, which can be found -[here](https://raw.githubusercontent.com/Copilot-Language/Copilot/master/LICENSE) - - -## Issues / Bugs -If you happen to find any issues or bugs, please add an issue to the -corresponding repository on our Github pages. - - -## Contact -The project is currently maintained by Frank Dedden and Alwyn Goodloe (NASA -Langley Research Center). For any questions, remarks, ideas etc. please send an -email to [dev@dedden.net](mailto:dev@dedden.net). - - -## The Copilot Team -The development of Copilot spans across several years. During these years -the following people have helped develop Copilot (in no particular order): - -* Lee Pike -* Alwyn Goodloe -* Robin Morisset -* Sebastian Niller -* Nis Wegmann -* Chris Hathhorn -* Eli Mendelson -* Jonathan Laurent -* Laura Titolo -* Georges-Axel Jolayan -* Macallan Cruff -* Ryan Spring -* Lauren Pick -* Frank Dedden -* Ivan Perez diff --git a/style.css b/style.css new file mode 100644 index 0000000..e0894ed --- /dev/null +++ b/style.css @@ -0,0 +1,156 @@ +/* Layout and spacing */ +* { + margin: 0; + padding: 0; +} + +#page { + max-width: 60em; + margin: 0 auto; +} + +#header { + line-height: 6em; + padding: 0 1.5em; +} + +#menu { + padding: 0 1em; +} + +#content { + padding: 3em 5em; +} + +p { + padding: .3em 0; + line-height: 1.7em; +} + +h1, h2, h3, h4, h5, h6 { + margin: 1em 0 0 0; +} + +ul { + margin: 0 0 0 3em; +} + +li { + padding: .2em 0; +} + +#menu p { + margin: 0; + padding: 0; +} + + +/* The palette used for the website: +Purple + shade 0 = #582A72 + shade 1 = #9775AA + shade 2 = #764B8E + shade 3 = #3D1255 + shade 4 = #260339 + +Blue + shade 0 = #29506D + shade 1 = #718EA4 + shade 2 = #496D89 + shade 3 = #123652 + shade 4 = #042037 +*/ +/* Theme */ +* { + font-family: sans-serif; +} + +p { + font-size: 93%; + text-align: justify; +} + +h1, h2, h3, h4, h5, h6 { + font-weight: 100; +} + +h1 { + border: 0; + border-style: solid; + border-width: 0 0 2px 0; + border-color: #3D1255; + font-size: 150%; + font-variant: small-caps; +} + +h2 { + font-size: 110%; +} + +code { + font-family: monospace; +} + +pre { + border: 0; + border-style: solid; + border-width: 0 0 0 5px; + border-color: #9775AA; + padding: .5em; +} + +#page { + background: white; + box-shadow: 0 0 .5em lightgrey; +} + +body { + background: #eee; +} + +#header a { + color: #3D1255; + font-variant: small-caps; + font-weight: 100; + font-size: 250%; + text-decoration: none; +} + +#header span { + color: grey; + font-style: italic; + margin: 0 0 0 1.5em; +} + +#menu { + background: #3D1255; +} + +#menu a { + color: white; + display: inline-block; + padding: .2em 1em; + text-decoration: none; + text-shadow: 1px 1px black; +} + +#menu a:hover { + background: #764B8E; +} + +#content a { + color: #29526D; +} + +#content a:hover { + color: #718EA4; +} + +mark { + background: transparent; + font-family: inherit; +} + +li { + font-size: 93%; +} From 2f3d84e975d0b8a88fd1b97f63dbf416b0984795 Mon Sep 17 00:00:00 2001 From: Frank Dedden Date: Tue, 5 May 2020 23:12:09 +0200 Subject: [PATCH 02/30] Added index.html symlink. Refs #23. --- index.html | 1 + 1 file changed, 1 insertion(+) create mode 120000 index.html diff --git a/index.html b/index.html new file mode 120000 index 0000000..1194c96 --- /dev/null +++ b/index.html @@ -0,0 +1 @@ +home.html \ No newline at end of file From 9a5abe4068dc5c364d173f609759eea46b24c148 Mon Sep 17 00:00:00 2001 From: Frank Dedden Date: Tue, 5 May 2020 23:21:03 +0200 Subject: [PATCH 03/30] Removed maintainers from contact page. --- contact.html | 6 ------ 1 file changed, 6 deletions(-) diff --git a/contact.html b/contact.html index 354ca4b..6ce1193 100644 --- a/contact.html +++ b/contact.html @@ -49,12 +49,6 @@

General Questions

publicly or if you are not in the possession of a GitHub account, please send your questions to Frank Dedden dev@dedden.net.

-

Copilot developers

- -

Copilot is currently developed and maintained by Frank Dedden. Alwyn Goodloe -and Ivan Perez provide helpful feedback on the usage of Copilot at NASA -Langley Research Center.

-

Previous developers

The development of Copilot spans across several years. During these years From f9443f118107bbba79a7decc1b50e8e7e6c9f149 Mon Sep 17 00:00:00 2001 From: Frank Dedden Date: Wed, 6 May 2020 19:47:21 +0200 Subject: [PATCH 04/30] Published fixes in example on homepage. Refs #24. --- home.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/home.html b/home.html index 171c84c..d378d9e 100644 --- a/home.html +++ b/home.html @@ -36,7 +36,7 @@

- 
-- Raw temperature from sensor, range -50.0 to 150.0.
+					
-- Raw temperature from sensor, range -50.0C to 100.0C.
 temp :: Stream Word8
 temp = extern "temperature" Nothing
 

From 401b3970c978fbd3dd4b58a0619cfffad1e2300b Mon Sep 17 00:00:00 2001
From: Frank Dedden 
Date: Tue, 30 Jun 2020 15:11:24 +0200
Subject: [PATCH 05/30] Updated maintainers in contact page. Refs #19.

---
 contact.html | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/contact.html b/contact.html
index 6ce1193..d1992a6 100644
--- a/contact.html
+++ b/contact.html
@@ -47,7 +47,8 @@ 
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 Frank Dedden dev@dedden.net.

+your questions to the maintainer, Frank Dedden
+dev@dedden.net.

 
 
Previous developers

 
@@ -68,7 +69,6 @@ 
Previous developers

 
  • Macallan Cruff
    • 
 
  • Ryan Spring
    • 
 
  • Lauren Pick
    • 
-
  • Frank Dedden
    • 
 
  • Ivan Perez
    •
    From f62d2ea6ba53169cf99c39ea98f2ed6a5dc8ab7b Mon Sep 17 00:00:00 2001 From: Frank Dedden Date: Wed, 24 Mar 2021 20:46:43 +0100 Subject: [PATCH 06/30] Added news item for release 3.2.1. Closes #27. --- home.html | 27 ++++++++++++++++++++++++++- 1 file changed, 26 insertions(+), 1 deletion(-) diff --git a/home.html b/home.html index d378d9e..5fc2dbe 100644 --- a/home.html +++ b/home.html @@ -51,7 +51,32 @@
    -

    Licence

    +

    News

    + +

    Release 3.2.1 – 2021-03-08

    + +

    We are very pleased to announce the release of Copilot 3.2.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.

    + +

    In collaboration with the development team at Galois, Inc., the new release +introduces a backend to their What4 +solver frontend. With this addition, it is now possible to prove properties of +Copilot specifications using. We thank Galois for their help and their +contribution.

    + +

    The second big focus of this release was the documentation: the public API +documentation has been improved and completed.

    + +

    Additionally, several small improvements and fixes are made in the C99 code +generator.

    + +

    Licence

    Copilot is distributed under the BSD-3-Clause licence, which can be found here.

    From 167be6c115b35a6229813dff413c22d9992c6e51 Mon Sep 17 00:00:00 2001 From: Frank Dedden Date: Wed, 30 Jun 2021 22:27:24 +0200 Subject: [PATCH 07/30] Changes after #28 and #29. --- contact.html | 21 ++------------------- documentation.html | 13 ++++--------- home.html | 30 ++++++++++++++---------------- 3 files changed, 20 insertions(+), 44 deletions(-) diff --git a/contact.html b/contact.html index d1992a6..7f18db6 100644 --- a/contact.html +++ b/contact.html @@ -21,28 +21,11 @@

    Contact & Help

    Having trouble using Copilot, or encountered a possible bug? Asking questions -or reporting bugs can both be done through the issue tracker at GitHub. This +or reporting bugs can both be done through the issue +tracker at GitHub. This helps us keep track of open bugs and problems, and allows us to easily comment and discuss the issue.

    -

    As Copilot consists of several packages, each of them comes with its own issue -tracker. If you have a question about a specific package or encountered a -problem specific to a package, please report the problem at that package, if -possible. In all other cases, please refer to the issue tracker of the general -Copilot package:

    - - - -

    General Questions

    For general questions about Copilot, questions that are unsuited to be posted diff --git a/documentation.html b/documentation.html index 4f37666..8e345c6 100644 --- a/documentation.html +++ b/documentation.html @@ -25,38 +25,33 @@

    Documentation

    Copilot comes with a set of examples as part of its distribution, available in the Examples directory of -the main repository.

    +the repository.

    Structure and Sources

    Apart from the Copilot Github project page, there are a number of sub-projects -that make up Copilot:

    +that make up Copilot, that all share a single repository:

      -

    • Copilot: The main Copilot package, to which all others are a dependency. +

    • copilot: The main Copilot package, to which all others are a dependency. One should install this one to install Copilot. -(Sources) +(Sources) (Hackage)

    • copilot-core: The core language, which efficiently represents Copilot expressions. The core is only of interest to implementers wishing to add a new back-end to Copilot. -(Sources) (Hackage)

    • copilot-language: The front-end of Copilot defining the user language. A user of Copilot typically interacts with this library. -(Sources) (Hackage)

    • copilot-libraries: User-supplied libraries for Copilot, including linear-temporal logic, fault-tolerant voting, regular expressions, etc. -(Sources) (Hackage)

    • copilot-c99: A backend writing hard realtime C99 code. It writes readable output and ensures the output code is constant in memory and time. -(Sources) (Hackage)

    • copilot-theorem: Some tools to prove properties on Copilot. -(Sources) (Hackage)

    diff --git a/home.html b/home.html index 5fc2dbe..7dd0d7d 100644 --- a/home.html +++ b/home.html @@ -53,28 +53,26 @@

    News

    -

    Release 3.2.1 – 2021-03-08

    +

    Release 3.3 – 2021-05-14

    -

    We are very pleased to announce the release of Copilot 3.2.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.

    +

    We are pleased to announce the release of Copilot 3.3, 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.

    -

    In collaboration with the development team at Galois, Inc., the new release -introduces a backend to their What4 -solver frontend. With this addition, it is now possible to prove properties of -Copilot specifications using. We thank Galois for their help and their -contribution.

    +

    This new release introduces a number of bug fixes and deprecates functions that +have been superseded. Additionally, our main Copilot repository will now +include also all the libraries that accompany the Copilot framework, and all +development will take place under that same repository.

    -

    The second big focus of this release was the documentation: the public API -documentation has been improved and completed.

    - -

    Additionally, several small improvements and fixes are made in the C99 code -generator.

    +

    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.

    Licence

    From 0a2d6a269516ecf0e8b47a16094624c5ea56191e Mon Sep 17 00:00:00 2001 From: Frank Dedden Date: Thu, 8 Jul 2021 19:07:16 +0200 Subject: [PATCH 08/30] Updated news for release of Copilot 3.4. Refs #30. --- home.html | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/home.html b/home.html index 7dd0d7d..f314d83 100644 --- a/home.html +++ b/home.html @@ -53,9 +53,9 @@

    News

    -

    Release 3.3 – 2021-05-14

    +

    Release 3.4 – 2021-07-07

    -

    We are pleased to announce the release of Copilot 3.3, a stream-based DSL for +

    We are pleased to announce the release of Copilot 3.4, 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), @@ -65,9 +65,7 @@

    News

    Branch of NASA Langley Research Center for monitoring test flights of drones.

    This new release introduces a number of bug fixes and deprecates functions that -have been superseded. Additionally, our main Copilot repository will now -include also all the libraries that accompany the Copilot framework, and all -development will take place under that same repository.

    +have been superseded.

    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 e961e9570f16f67a58712b1333bd97e7f8347737 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 19 Aug 2021 10:36:36 -0400 Subject: [PATCH 09/30] Updated news for release of Copilot 3.5. Refs #33. --- home.html | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/home.html b/home.html index f314d83..e3fea5e 100644 --- a/home.html +++ b/home.html @@ -53,9 +53,9 @@

    News

    -

    Release 3.4 – 2021-07-07

    +

    Release 3.5 – 2021-09-07

    -

    We are pleased to announce the release of Copilot 3.4, a stream-based DSL for +

    We are pleased to announce the release of Copilot 3.5, 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), @@ -64,8 +64,14 @@

    News

    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 number of bug fixes and deprecates functions that -have been superseded.

    +

    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.

    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 2a83ab091a56ba5503da5c56401d78b418ca67ac Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 9 Nov 2021 09:24:50 -0500 Subject: [PATCH 10/30] Update POC on website. Refs #36. Update POC from Frank to Ivan. --- contact.html | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/contact.html b/contact.html index 7f18db6..0af8d8d 100644 --- a/contact.html +++ b/contact.html @@ -30,8 +30,8 @@

    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.

    +your questions to the maintainer, Ivan Perez +ivan.perezdominguez@nasa.gov.

    Previous developers

    From 62409f547cdaa93e486f884a30bf8d2f60772fb4 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 9 Nov 2021 09:34:23 -0500 Subject: [PATCH 11/30] Updated news for release of Copilot 3.6. Refs #35. --- home.html | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/home.html b/home.html index e3fea5e..63d4b60 100644 --- a/home.html +++ b/home.html @@ -53,9 +53,9 @@

    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), @@ -64,14 +64,12 @@

    News

    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 From 45209b7ac8d8e751f63916711b64d2388a40a8b1 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 8 Jan 2022 01:41:24 +0100 Subject: [PATCH 12/30] Updated news for release of Copilot 3.7. Refs #37. --- home.html | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/home.html b/home.html index 63d4b60..028cee6 100644 --- a/home.html +++ b/home.html @@ -53,9 +53,9 @@

    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), @@ -64,12 +64,8 @@

    News

    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 4ba99b8e5a9b0f84e7e946519c48c1076a3de560 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 24 Mar 2022 10:52:36 -0400 Subject: [PATCH 13/30] Updated the news for Copilot 3.8. Refs #38. --- home.html | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/home.html b/home.html index 028cee6..ee1cf92 100644 --- a/home.html +++ b/home.html @@ -53,9 +53,9 @@

    News

    -

    Release 3.7 – 2022-01-07

    +

    Release 3.8 – 2022-03-07

    -

    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), @@ -64,8 +64,9 @@

    News

    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 a1b23ad74cd2a91c52b541c922278edf1f591432 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 16 May 2022 09:24:15 -0400 Subject: [PATCH 14/30] Update news for Copilot 3.9. Refs #39. --- home.html | 25 ++++++++++++++++--------- 1 file changed, 16 insertions(+), 9 deletions(-) diff --git a/home.html b/home.html index ee1cf92..dbbabba 100644 --- a/home.html +++ b/home.html @@ -53,9 +53,9 @@

    News

    -

    Release 3.8 – 2022-03-07

    +

    Release 3.9 – 2022-05-07

    -

    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), @@ -64,14 +64,21 @@

    News

    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.

    +

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

    -

    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.

    +

    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.

    Licence

    From dfb944a03c271fefd1680f7fb09d1e20923ab7b9 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 7 Sep 2022 23:00:36 +0000 Subject: [PATCH 15/30] Update news for Copilot 3.10. Refs #40. --- home.html | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/home.html b/home.html index dbbabba..dde18ff 100644 --- a/home.html +++ b/home.html @@ -53,24 +53,25 @@

    News

    -

    Release 3.9 – 2022-05-07

    +

    Release 3.10 – 2022-07-07

    -

    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), -clocks and voting algorithms.

    +

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

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

    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.

    Current emphasis is on facilitating the use with other systems, improving From f06d7f972a516434ce4d40f8ce276a33401c8a71 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 7 Sep 2022 23:10:35 +0000 Subject: [PATCH 16/30] Fix broken link to examples. Refs #41. --- documentation.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/documentation.html b/documentation.html index 8e345c6..c5d3bd7 100644 --- a/documentation.html +++ b/documentation.html @@ -23,7 +23,7 @@

    Documentation

    A manual to Copilot can be downloaded here.

    Copilot comes with a set of examples as part of its distribution, available in -the Examples +the Examples directory of the repository.

    From a85b4ba14140885c84422ab70b02b82431d28131 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 7 Sep 2022 23:18:32 +0000 Subject: [PATCH 17/30] Update news for Copilot 3.11. Refs #42. --- home.html | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/home.html b/home.html index dde18ff..6df2c7d 100644 --- a/home.html +++ b/home.html @@ -53,9 +53,9 @@

    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 +

    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 @@ -65,13 +65,15 @@

    News

    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 -engineering process designed to meet the requirements to obtain NASA's Class D -software classification. Details are available here. +

    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.

    Current emphasis is on facilitating the use with other systems, improving From 01fe77e06c00df304f46fe34cf8062014ea9b836 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 7 Sep 2022 23:19:26 +0000 Subject: [PATCH 18/30] Document existence of copilot-interpreter as part of Copilot 3.11. Refs #42. --- documentation.html | 2 ++ 1 file changed, 2 insertions(+) diff --git a/documentation.html b/documentation.html index c5d3bd7..7a9e8e8 100644 --- a/documentation.html +++ b/documentation.html @@ -42,6 +42,8 @@

    Structure and Sources

    expressions. The core is only of interest to implementers wishing to add a new back-end to Copilot. (Hackage)

    +

  • copilot-interpreter: A backend for simulating Copilot specifications. +(Hackage)

  • copilot-language: The front-end of Copilot defining the user language. A user of Copilot typically interacts with this library. (Hackage)

    • From 16e599f5fd6b15bb51d6e83301368af1ba707b99 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 9 Nov 2022 18:47:16 +0000 Subject: [PATCH 19/30] Update news for Copilot 3.12. Refs #44. --- home.html | 60 ++++++++++++++++++++++++++++++++++++++----------------- 1 file changed, 42 insertions(+), 18 deletions(-) diff --git a/home.html b/home.html index 6df2c7d..1b1a14c 100644 --- a/home.html +++ b/home.html @@ -53,9 +53,9 @@

    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 +

    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 @@ -65,22 +65,46 @@

    News

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

    - -

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

    + +

    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.

    Licence

    From 534bf0b6a4e826c959519654237cb7ce9cd13e8a Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 10 Jan 2023 08:20:15 +0000 Subject: [PATCH 20/30] Update news for Copilot 3.13. Refs #45. --- home.html | 38 ++++++-------------------------------- 1 file changed, 6 insertions(+), 32 deletions(-) diff --git a/home.html b/home.html index 1b1a14c..313d177 100644 --- a/home.html +++ b/home.html @@ -53,9 +53,9 @@

    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 +

    We are pleased to announce the release of Copilot 3.13, 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 @@ -65,36 +65,10 @@

    News

    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.The main changes in this release are as follows:

    This release also continues to use our new software engineering process designed to meet the requirements to obtain NASA’s Class D software From 18f779a9ef05e5cef7146fd2f07d89f47869cf65 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 10 Jan 2023 08:25:43 +0000 Subject: [PATCH 21/30] Fix link to Copilot 3.13 milestone. Refs #46. --- home.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/home.html b/home.html index 313d177..0e8e908 100644 --- a/home.html +++ b/home.html @@ -73,7 +73,7 @@

    News

    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.

    +href="https://github.com/Copilot-Language/copilot/milestone/17?closed=1">here.

    Current emphasis is on improving the codebase in terms of stability and test coverage, removing unnecessary dependencies, hiding internal definitions, and From b0c66d88745298304e6572b5a8d14f3eb77621e6 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 8 Mar 2023 17:55:56 +0000 Subject: [PATCH 22/30] Update version of Copilot available, and GHC needed. Refs #43. --- download.html | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/download.html b/download.html index 0dc3b87..af42ec8 100644 --- a/download.html +++ b/download.html @@ -21,8 +21,8 @@

    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. The Haskell platform comes with the compiler and basic tools necessary to install Copilot.

    From c2006413222565ca3e06de742199fe7760d6a78f Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 8 Mar 2023 17:59:23 +0000 Subject: [PATCH 23/30] Update news for Copilot 3.14. Refs #47. --- home.html | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/home.html b/home.html index 0e8e908..979204a 100644 --- a/home.html +++ b/home.html @@ -53,9 +53,9 @@

    News

    -

    Release 3.13 – 2023-01-07

    +

    Release 3.14 – 2023-03-07

    -

    We are pleased to announce the release of Copilot 3.13, a stream-based DSL +

    We are pleased to announce the release of Copilot 3.14, 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 @@ -65,10 +65,9 @@

    News

    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 published on hackage, as well as -github.The main changes in this release are as follows:

    +

    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 designed to meet the requirements to obtain NASA’s Class D software From d9f178321c28fb6b06b24d5dced0adf79d6bff90 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 8 Mar 2023 18:07:55 +0000 Subject: [PATCH 24/30] Deference symlink. Refs #48. --- index.html | 103 ++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 102 insertions(+), 1 deletion(-) mode change 120000 => 100644 index.html diff --git a/index.html b/index.html deleted file mode 120000 index 1194c96..0000000 --- a/index.html +++ /dev/null @@ -1 +0,0 @@ -home.html \ No newline at end of file diff --git a/index.html b/index.html new file mode 100644 index 0000000..979204a --- /dev/null +++ b/index.html @@ -0,0 +1,102 @@ + + + + Copilot: home + + + + + +

    + + +
    +
    +

    + 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
+
+-- Transform the temperature to Celsius.
+ctemp :: Stream Float
+ctemp = (unsafeCast temp) * (150.0 / 255.0) - 50.0
+
+-- Bind two triggers with a 3.0C hysteresis.
+spec = do
+  trigger "heaton"  (ctemp < 18.0) [arg ctemp]
+  trigger "heatoff" (ctemp > 21.0) [arg ctemp]
    +
    +
    +
    +

    News

    + +

    Release 3.14 – 2023-03-07

    + +

    We are pleased to announce the release of Copilot 3.14, 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 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 +designed to meet the requirements to obtain NASA’s Class D software +classification. Details are available here.

    + +

    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.

    + +

    Licence

    + +

    Copilot is distributed under the BSD-3-Clause licence, which can be found +here.

    + +

    Acknowledgements

    + +

    We are grateful for NASA Contract NNL08AD13T to Galois, Inc. and the National +Institute of Aerospace, which partially supported this work.

    + +

    Additionally NASA Langley contracts 80LARC17C0004 and NNL09AA00A supported +further development of Copilot.

    + +

    We would like to thank Kaveh Darafsheh (NASA Langley Research Center) for his +help with testing Copilot. In addition numerous people have helped with smaller +things, reporting bugs etc. Thanks to all of them!

    +
    +
    + + From 73caecd2af61da0aa2f270171d32e3aa911d3a3c Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 22 May 2023 01:44:57 +0000 Subject: [PATCH 25/30] Update news for Copilot 3.15. Refs #49. --- home.html | 9 ++++----- index.html | 9 ++++----- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/home.html b/home.html index 979204a..a849025 100644 --- a/home.html +++ b/home.html @@ -53,9 +53,9 @@

    News

    -

    Release 3.14 – 2023-03-07

    +

    Release 3.15 – 2023-05-07

    -

    We are pleased to announce the release of Copilot 3.14, a stream-based DSL +

    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 @@ -65,9 +65,8 @@

    News

    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 diff --git a/index.html b/index.html index 979204a..a849025 100644 --- a/index.html +++ b/index.html @@ -53,9 +53,9 @@

    News

    -

    Release 3.14 – 2023-03-07

    +

    Release 3.15 – 2023-05-07

    -

    We are pleased to announce the release of Copilot 3.14, a stream-based DSL +

    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 @@ -65,9 +65,8 @@

    News

    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 0eb73149804ce8af7284fb2c2848156921aaed33 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 8 Jul 2023 19:43:31 +0000 Subject: [PATCH 26/30] Remove tabs. Refs #51. --- about.html | 34 ++++++++++---------- contact.html | 34 ++++++++++---------- documentation.html | 34 ++++++++++---------- download.html | 34 ++++++++++---------- home.html | 78 +++++++++++++++++++++++----------------------- index.html | 78 +++++++++++++++++++++++----------------------- 6 files changed, 146 insertions(+), 146 deletions(-) diff --git a/about.html b/about.html index 94e124d..1d849db 100644 --- a/about.html +++ b/about.html @@ -1,24 +1,24 @@ - - Copilot: about - - - - -

    - - + diff --git a/contact.html b/contact.html index 0af8d8d..3c738b5 100644 --- a/contact.html +++ b/contact.html @@ -1,24 +1,24 @@ - - Copilot: contact - - - - -
    - - + diff --git a/documentation.html b/documentation.html index 7a9e8e8..004a987 100644 --- a/documentation.html +++ b/documentation.html @@ -1,24 +1,24 @@ - - Copilot: documentation - - - - -
    - - + diff --git a/download.html b/download.html index af42ec8..57b3c7e 100644 --- a/download.html +++ b/download.html @@ -1,24 +1,24 @@ - - Copilot: download - - - - -
    - - + diff --git a/home.html b/home.html index a849025..1f9d803 100644 --- a/home.html +++ b/home.html @@ -1,42 +1,42 @@ - - Copilot: home - - - - - -
    - - + diff --git a/index.html b/index.html index a849025..1f9d803 100644 --- a/index.html +++ b/index.html @@ -1,42 +1,42 @@ - - Copilot: home - - - - - -
    - - + From 38bdb25245d2be99e504444c4420ce429f2cb8b5 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 8 Jul 2023 19:49:09 +0000 Subject: [PATCH 27/30] Update news for Copilot 3.16. Refs #50. --- home.html | 96 ++++++++++++++++++++++++++---------------------------- index.html | 96 ++++++++++++++++++++++++++---------------------------- 2 files changed, 94 insertions(+), 98 deletions(-) diff --git a/home.html b/home.html index 1f9d803..e5e99ca 100644 --- a/home.html +++ b/home.html @@ -48,54 +48,52 @@ spec = do trigger "heaton" (ctemp < 18.0) [arg ctemp] trigger "heatoff" (ctemp > 21.0) [arg ctemp] -
    -
    -
    -

    News

    - -

    Release 3.15 – 2023-05-07

    - -

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

    - -

    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.

    - -

    Licence

    - -

    Copilot is distributed under the BSD-3-Clause licence, which can be found -here.

    - -

    Acknowledgements

    - -

    We are grateful for NASA Contract NNL08AD13T to Galois, Inc. and the National -Institute of Aerospace, which partially supported this work.

    - -

    Additionally NASA Langley contracts 80LARC17C0004 and NNL09AA00A supported -further development of Copilot.

    - -

    We would like to thank Kaveh Darafsheh (NASA Langley Research Center) for his -help with testing Copilot. In addition numerous people have helped with smaller -things, reporting bugs etc. Thanks to all of them!

    -
    - +
    +
    +

    News

    +

    Release 3.16 – 2023-07-07

    +

    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), + 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.

    +

    Details are available here + and here.

    +

    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.

    +

    Licence

    +

    Copilot is distributed under the BSD-3-Clause licence, which + can be found here.

    +

    Acknowledgements

    +

    We are grateful for NASA Contract NNL08AD13T to Galois, + Inc. and the National Institute of Aerospace, which partially + supported this work.

    +

    Additionally NASA Langley contracts 80LARC17C0004 and + NNL09AA00A supported further development of Copilot.

    +

    We would like to thank Kaveh Darafsheh (NASA Langley Research + Center) for his help with testing Copilot. In addition numerous + people have helped with smaller things, reporting bugs etc. + Thanks to all of them!

    +
    +
    + diff --git a/index.html b/index.html index 1f9d803..e5e99ca 100644 --- a/index.html +++ b/index.html @@ -48,54 +48,52 @@ spec = do trigger "heaton" (ctemp < 18.0) [arg ctemp] trigger "heatoff" (ctemp > 21.0) [arg ctemp] -
    -
    -
    -

    News

    - -

    Release 3.15 – 2023-05-07

    - -

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

    - -

    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.

    - -

    Licence

    - -

    Copilot is distributed under the BSD-3-Clause licence, which can be found -here.

    - -

    Acknowledgements

    - -

    We are grateful for NASA Contract NNL08AD13T to Galois, Inc. and the National -Institute of Aerospace, which partially supported this work.

    - -

    Additionally NASA Langley contracts 80LARC17C0004 and NNL09AA00A supported -further development of Copilot.

    - -

    We would like to thank Kaveh Darafsheh (NASA Langley Research Center) for his -help with testing Copilot. In addition numerous people have helped with smaller -things, reporting bugs etc. Thanks to all of them!

    -
    - +
    +
    +

    News

    +

    Release 3.16 – 2023-07-07

    +

    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), + 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.

    +

    Details are available here + and here.

    +

    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.

    +

    Licence

    +

    Copilot is distributed under the BSD-3-Clause licence, which + can be found here.

    +

    Acknowledgements

    +

    We are grateful for NASA Contract NNL08AD13T to Galois, + Inc. and the National Institute of Aerospace, which partially + supported this work.

    +

    Additionally NASA Langley contracts 80LARC17C0004 and + NNL09AA00A supported further development of Copilot.

    +

    We would like to thank Kaveh Darafsheh (NASA Langley Research + Center) for his help with testing Copilot. In addition numerous + people have helped with smaller things, reporting bugs etc. + Thanks to all of them!

    +
    +
    + From 68085f4bc8d5a5bcc7a7cd60663e5a0d7e2fae6d Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 9 Nov 2023 07:59:35 +0000 Subject: [PATCH 28/30] Americanize the spelling of license. Refs #53. This commit replaces all occurrences of the word licence (British spelling) with license (American spelling). --- home.html | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/home.html b/home.html index e5e99ca..13f5569 100644 --- a/home.html +++ b/home.html @@ -79,8 +79,8 @@

    News

    opening issues and asking questions via our github repo.

    -

    Licence

    -

    Copilot is distributed under the BSD-3-Clause licence, which +

    License

    +

    Copilot is distributed under the BSD-3-Clause license, which can be found here.

    Acknowledgements

    From 40d2db5bf622bbaf93b2ecd1e038f9ee7842fe63 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 9 Nov 2023 08:10:30 +0000 Subject: [PATCH 29/30] Update news for Copilot 3.17. Refs #52. --- home.html | 29 ++++++++++++++--------------- 1 file changed, 14 insertions(+), 15 deletions(-) diff --git a/home.html b/home.html index 13f5569..2a50714 100644 --- a/home.html +++ b/home.html @@ -52,7 +52,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 writing and monitoring embedded C programs, with an emphasis on correctness and hard realtime requirements. @@ -62,22 +62,21 @@

    News

    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 + href="https://github.com/Copilot-Language/copilot/milestone/22?closed=1">here and here.

    -

    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 + href="https://github.com/Copilot-Language/copilot/releases/tag/v3.17">here.

    +

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

    License

    Copilot is distributed under the BSD-3-Clause license, which From b9bd0764cc3c0ee4c9aa3de11bcca87fe0d25f1c Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 9 Nov 2023 08:15:25 +0000 Subject: [PATCH 30/30] Populate changes from home.html to index.html. Refs #52. A prior commit introduced changes to home.html, but these were not passed on to index.html. This include release changes, as well as a change to the spelling of the word license. This commit updates index.html with all the changes made to home.html. --- index.html | 33 ++++++++++++++++----------------- 1 file changed, 16 insertions(+), 17 deletions(-) diff --git a/index.html b/index.html index e5e99ca..2a50714 100644 --- a/index.html +++ b/index.html @@ -52,7 +52,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 writing and monitoring embedded C programs, with an emphasis on correctness and hard realtime requirements. @@ -62,25 +62,24 @@

    News

    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 + href="https://github.com/Copilot-Language/copilot/milestone/22?closed=1">here and here.

    -

    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 + href="https://github.com/Copilot-Language/copilot/releases/tag/v3.17">here.

    +

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

    -

    Licence

    -

    Copilot is distributed under the BSD-3-Clause licence, which +

    License

    +

    Copilot is distributed under the BSD-3-Clause license, which can be found here.

    Acknowledgements