copilot 3.13 → 3.14
raw patch · 4 files changed
+273/−125 lines, 4 filesdep +copilot-prettyprinterdep ~copilot-c99dep ~copilot-coredep ~copilot-languagePVP ok
version bump matches the API change (PVP)
Dependencies added: copilot-prettyprinter
Dependency ranges changed: copilot-c99, copilot-core, copilot-language, copilot-libraries, copilot-theorem
API changes (from Hackage documentation)
Files
- CHANGELOG +6/−0
- README.md +249/−114
- copilot.cabal +11/−10
- src/Language/Copilot/Main.hs +7/−1
CHANGELOG view
@@ -1,3 +1,9 @@+2023-03-07+ * Version bump (3.14). (#422)+ * Replace import of Copilot.Language.prettyPrint. (#412)+ * Re-structure README. (#415)+ * Update README to reflect support for GHC 9.4. (#423)+ 2023-01-07 * Version bump (3.13). (#406)
README.md view
@@ -1,89 +1,162 @@-# Copilot: Stream DSL for hard real-time runtime verification+<div align="center"> +# Copilot+ [](https://app.travis-ci.com/github/Copilot-Language/copilot) [](https://hackage.haskell.org/package/copilot) -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.-+Copilot is a runtime verification framework for hard real-time systems. Programs can be interpreted for testing, or translated into C99 code to be-incorporated in a project or as a standalone application. The C99 backend-output is constant in memory and time, making it suitable for systems with hard-realtime requirements.+incorporated in a project or standalone application. The C99 code generated+is constant in memory and time, making it suitable for systems with hard+real-time requirements. +[Installation](#installation) •+[Examples](#examples) •+[Related projects](#related-projects) •+[Documentation](#documentation) •+[Contributions](#contributions) •+[Acknowledgements](#acknowledgements) -## Using Copilot-Assuming you have GHC and cabal already installed (see [Haskell-Platform](http://hackage.haskell.org/platform/) or-[ghcup](https://www.haskell.org/ghcup/)), there are several ways to use-Copilot:+</div> -* Adding Copilot to your project+## Features - Copilot is available from- [Hackage](https://hackage.haskell.org/package/copilot). Adding `copilot`- to your project's cabal file should be enough to get going.+- Write simple, high-level specifications using a stream-based language. -* Adding Copilot to the default GHC environment+- Produce hard real-time C99 runtime monitors that run in constant memory and time. - ```bash- cabal v2-install --lib copilot- ```+- Catch errors in specifications early using expressive static type system. - After which Copilot will be available from ghci.+- Prove properties about specifications using theorem proving extensions. -* Launching a repl with Copilot+- Interpret specifications for testing and debugging purposes. - Another quick solution is to cabal to launch a repl with Copilot- available.+- Obtain proofs of correctness of the generated code. - ```bash- cabal v2-repl --build-depends copilot- ```+## Table of Contents - Cabal will download and build Copilot only to make it available in the- launched repl. The global GHC environment will not be affected.+- [Installation](#installation)+ - [Linux installation](#linux-installation)+ - [Mac installation](#mac-installation)+ - [Troubleshooting](#troubleshooting)+- [Examples](#examples)+- [Related projects](#related-projects)+- [Documentation](#documentation)+ - [API documentation and tutorials](#api-documentation-and-tutorials)+ - [Publications](#publications)+ - [Website](#website)+- [Contributions](#contributions)+- [Acknowledgements](#acknowledgements)+ - [The Copilot team](#the-copilot-team)+ - [Institutional support](#institutional-support) -* Building from source (typically done for development):+# Installation+<sup>[(Back to top)](#table-of-contents)</sup> - ```bash- git clone https://github.com/Copilot-Language/copilot.git- cd copilot- ```+## Linux installation+<sup>[(Back to top)](#table-of-contents)</sup> - Compiling can either be done in a Nix-style build, or a traditional one:+### Debian Bookworm / Ubuntu 23.04 - _Nix-Style build (Cabal >= 2.x)_+On Debian Bookworm / Ubuntu 23.04 or newer, Copilot can be installed directly+from the package repositories with: - ```bash- cabal build copilot-*/ # For Cabal 3.x- cabal v2-build copilot-*/ # For Cabal 2.x- ```+```sh+$ sudo apt-get install libghc-copilot-dev+``` - _Traditional build (Cabal 1.x)_- ```bash- cd copilot- cabal install --dependencies-only . ../copilot-*/- cabal install ../copilot-*/- cabal build- ```+To test that Copilot is available, execute the following:+```sh+$ ghci <<< 'import Language.Copilot'+``` -Note there is a TravisCI build (linked to at the top of this README) if you-have trouble building/installing.+It should end with a line like the following and not print any error messages:+```sh+ghci> ghci> Leaving GHCi.+``` +### Other Linux distributions -## Example-Here follows a simple example of a heating system. Other examples can be found+On other Linux distributions or older Debian-based distributions, to use+Copilot you must install a Haskell compiler (GHC) and the package manager+Cabal. We currently support all versions of GHC from 8.6.5 to modern versions+(9.4 as of this writing). You can install the toolchain using+[ghcup](https://www.haskell.org/ghcup/) or, if you are on Debian/Ubuntu,+directly with `apt-get`:++```sh+$ sudo apt-get install ghc cabal-install+```++Once the compiler is installed, install Copilot from+[Hackage](https://hackage.haskell.org/package/copilot) with:++```sh+cabal v2-install --lib copilot+```++To test that Copilot is available, execute the following:+```sh+$ ghci <<< 'import Language.Copilot'+```++It should end with a line like the following and not print any error messages:+```sh+ghci> ghci> Leaving GHCi.+```++## Mac installation+<sup>[(Back to top)](#table-of-contents)</sup>++To use Copilot you must have a Haskell compiler (GHC) and the package manager+Cabal. We currently support all versions of GHC from 8.6.5 to modern versions+(9.4 as of this writing). You can install the toolchain using+[ghcup](https://www.haskell.org/ghcup/), as well as with Homebrew:++```sh+$ brew install ghc cabal-install+```++Once the compiler is installed, install Copilot from+[Hackage](https://hackage.haskell.org/package/copilot) with:++```sh+$ cabal v2-install --lib copilot+```++To test that Copilot is available, execute the following:+```sh+$ ghci <<< 'import Language.Copilot'+```++It should end with a line like the following and not print any error messages:+```sh+ghci> ghci> Leaving GHCi.+```++## Troubleshooting+<sup>[(Back to top)](#table-of-contents)</sup>++Feel free to open an issue if you are unable to install Copilot following these+instructions.++There is a TravisCI file at the root of the repository that may help with+troubleshooting the installation. Our issues often include comments with+Dockerfiles listing the steps necessary to install Copilot from scratch.++## Examples+<sup>[(Back to top)](#table-of-contents)</sup>++Here follows a simple example of a heating system. More examples can be found in the [examples directory](https://github.com/Copilot-Language/copilot/tree/master/copilot/examples) of the main repository. ```haskell--- 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 Celsius.+-- This example implements a simple home heating system. The system heats+-- when the temperature gets too low, and stops when it is high enough. It read+-- temperature as a byte (range -50C to 100C) and translates this to Celsius. module Heater where @@ -92,12 +165,13 @@ import Prelude hiding ((>), (<), div) --- External temperature as a byte, range of -50C to 100C+-- External temperature as a byte, ranging from -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+-- Temperature in Celsius.+--+-- We need to cast the Word8 to a Float. This 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@@ -112,83 +186,144 @@ main = reify spec >>= compile "heater" ``` -The examples located in the `examples/` directory can be run from the root of-the project. Each example has a name. As a rule of thumb, the examples are-named after the filename (without extension) in lowercase letters, and-directory seperators replaced with a '-'. For example:+If you save this example in a file `Heater.hs` and run:+```sh+$ runhaskell Heater.hs+```+it will produce the files `heater.c`, `heater.h` and `heater_types.h`,+containing, respectively, the implementation of the monitors, the interface,+and a declaration of any types declared in the specification (empty in this+case). +If you clone the repository, the examples in the `examples/` directory can be+run from the root of the project. As a rule of thumb, each example is named+after the filename (without extension) in lowercase letters, and directory+separators replaced with a '-'. For example:+ ```sh-cabal run addmult -f examples-cabal run counter -f examples-cabal run what4-arithmetic -f examples+$ cabal run addmult -f examples+$ cabal run counter -f examples+$ cabal run what4-arithmetic -f examples ``` -## Contributions-Feel free to open new issues and send pull requests.+# Related projects+<sup>[(Back to top)](#table-of-contents)</sup> -In order to contribute to Copilot, please use the following steps which will-make the process of evaluating and including your changes much easier:+_Disclaimer: The following projects are not part of Copilot. Their mention here+does not constitute any form of endorsement._ -* Create an issue for every individual change or problem with Copilot. Document- the issue well.+- [Ogma](https://github.com/nasa/ogma) is a NASA tool to facilitate the+ integration of safe runtime monitors into other systems, including those+ built using NASA's Core Flight System or the Robot Operating System (ROS 2). -* Always comment on the issues you are addressing in every commit. Be- descriptive, and use the syntax `#<issue_number>` so that we can track- changes and issues easily.+- [arduino-copilot](https://hackage.haskell.org/package/arduino-copilot)+ facilitates building copilot applications that run on Arduino. -* Every commit should mention one issue and, ideally, only one.+- [sketch-frp-copilot](https://hackage.haskell.org/package/sketch-frp-copilot)+ extends Copilot with an FRP-like interface. -* Do not send a PR or commit that addresses multiple problems, unless they are- related and cannot be separated.+- [zephir-copilot](https://hackage.haskell.org/package/zephyr-copilot)+ facilitates building copilot applications that run on boards supported by the+ Zephyr project. -* Do not commit to master directly, except for branch merges. Make sure you- always merge onto master using `--no-ff` so that we can tell that features- were addressed separately, completed, tested, and then merged. If you are a- Copilot developer, create a branch for every issue you are addressing, complete- it, and then merge onto master. Document every commit in every branch,- including the last merge commit, stating the issues it addresses or closes.+# Documentation+<sup>[(Back to top)](#table-of-contents)</sup> -This process is similar to [Git-Flow](http://nvie.com/posts/a-successful-git-branching-model/). The equivalent-of Git Flow's master branch is our latest tag, and the equivalent of Git Flow's-develop branch is our master.+## API documentation and tutorials+<sup>[(Back to top)](#table-of-contents)</sup> +A tutorial on Copilot can be found+[here](https://copilot-language.github.io/downloads/copilot_tutorial.pdf). -## Further information-For further information, including documentation and a tutorial, please visit-the Copilot website:+The API is documented throughout the different libraries and published on+Hackage:++- [copilot](https://hackage.haskell.org/package/copilot)+- [copilot-c99](https://hackage.haskell.org/package/copilot-c99)+- [copilot-core](https://hackage.haskell.org/package/copilot-core)+- [copilot-interpreter](https://hackage.haskell.org/package/copilot-interpreter)+- [copilot-language](https://hackage.haskell.org/package/copilot-language)+- [copilot-libraries](https://hackage.haskell.org/package/copilot-libraries)+- [copilot-prettyprinter](https://hackage.haskell.org/package/copilot-prettyprinter)+- [copilot-theorem](https://hackage.haskell.org/package/copilot-theorem)++## Publications+<sup>[(Back to top)](#table-of-contents)</sup>++The best introduction to the fundamentals of Copilot apart from the tutorial+is:++- [Copilot 3](https://ntrs.nasa.gov/citations/20200003164)++Other relevant papers include:++- [Automated Translation of Natural Language Requirements to Runtime Monitors](https://link.springer.com/chapter/10.1007/978-3-030-99524-9_21)++- [Copilot: A Hard Real-Time Runtime Monitor](https://link.springer.com/chapter/10.1007/978-3-642-16612-9_26)++- [Copilot: monitoring embedded systems](https://link.springer.com/article/10.1007/s11334-013-0223-x)++- [From Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project](https://arxiv.org/abs/2012.03745)++- [Integrating FRET with Copilot: Automated Translation of Natural Language Requirements to Runtime Monitors](https://ntrs.nasa.gov/citations/20220000049)++- [Monitoring Distributed Real-Time Systems: A Survey and Future Directions](https://ntrs.nasa.gov/citations/20100027427)++- [Monitoring ROS2: from Requirements to Autonomous Robots](https://arxiv.org/abs/2209.14030)++## Website+<sup>[(Back to top)](#table-of-contents)</sup>++For further information, including links to more documentation and the+tutorial, please visit the Copilot website: [https://copilot-language.github.io](https://copilot-language.github.io). +# Contributions+<sup>[(Back to top)](#table-of-contents)</sup> -## Acknowledgements-We are grateful for NASA Contract NNL08AD13T to Galois, Inc. and the National-Institute of Aerospace, which partially supported this work.+Copilot cannot accept pull requests or code contributions from developers+outside the development team at this point. -Additionally NASA Langley contracts 80LARC17C0004 and NNL09AA00A supported-further development of Copilot.+If you have a question, find a bug, or would like to request a change, please+file an issue adding as much information as you can to help us reproduce the+error or identify the use case. Please file the issue with no labels. +# Acknowledgements+<sup>[(Back to top)](#table-of-contents)</sup> -## License-Copilot is distributed under the BSD-3-Clause license, which can be found-[here](https://raw.githubusercontent.com/Copilot-Language/copilot/master/copilot/LICENSE).+## The Copilot team+<sup>[(Back to top)](#table-of-contents)</sup> +Copilot is currently maintained by: -## 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):+* Alwyn Goodloe+* Ivan Perez -* Lee Pike-* Alwyn Goodloe (maintainer)-* Robin Morisset-* Sebastian Niller-* Nis Wegmann+Past and current team members also include (in alphabetical order):++* Macallan Cruff+* Frank Dedden * Chris Hathhorn-* Eli Mendelson-* Jonathan Laurent-* Laura Titolo * Georges-Axel Jolayan-* Macallan Cruff-* Ryan Spring+* Jonathan Laurent+* Eli Mendelson+* Robin Morisset+* Sebastian Niller * Lauren Pick-* Frank Dedden (maintainer: contact at dev@dedden.net)-* Ivan Perez (maintainer)+* Lee Pike+* Will Pogge+* Ryan Spring+* Laura Titolo+* Nis Wegmann++For a complete list of contributors, including external contributors, see:+https://github.com/Copilot-Language/copilot/graphs/contributors++## Institutional support+<sup>[(Back to top)](#table-of-contents)</sup>++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.
copilot.cabal view
@@ -1,5 +1,5 @@ name: copilot-version: 3.13+version: 3.14 cabal-version: >= 1.10 license: BSD3 license-file: LICENSE@@ -47,16 +47,17 @@ -Wall -fno-warn-orphans build-depends:- base >= 4.9 && < 5- , optparse-applicative >= 0.14 && < 0.18- , directory >= 1.3 && < 1.4- , filepath >= 1.4 && < 1.5+ base >= 4.9 && < 5+ , optparse-applicative >= 0.14 && < 0.18+ , directory >= 1.3 && < 1.4+ , filepath >= 1.4 && < 1.5 - , copilot-core >= 3.13 && < 3.14- , copilot-theorem >= 3.13 && < 3.14- , copilot-language >= 3.13 && < 3.14- , copilot-libraries >= 3.13 && < 3.14- , copilot-c99 >= 3.13 && < 3.14+ , copilot-core >= 3.14 && < 3.15+ , copilot-theorem >= 3.14 && < 3.15+ , copilot-language >= 3.14 && < 3.15+ , copilot-libraries >= 3.14 && < 3.15+ , copilot-c99 >= 3.14 && < 3.15+ , copilot-prettyprinter >= 3.14 && < 3.15 exposed-modules: Language.Copilot, Language.Copilot.Main
src/Language/Copilot/Main.hs view
@@ -3,9 +3,10 @@ module Language.Copilot.Main ( copilotMain, defaultMain ) where import qualified Copilot.Core as C (Spec)-import Copilot.Language (interpret, prettyPrint)+import Copilot.Language (interpret) import Copilot.Language.Reify (reify) import Copilot.Language (Spec)+import qualified Copilot.PrettyPrint as PP import Options.Applicative import Data.Semigroup ((<>))@@ -86,3 +87,8 @@ -- command line options. defaultMain :: Compiler -> Spec -> IO () defaultMain = copilotMain interpret prettyPrint+ where+ -- Transform a high-level Copilot Language specification into a low-level+ -- Copilot Core specification and pretty-print it to stdout.+ prettyPrint :: Spec -> IO ()+ prettyPrint e = fmap PP.prettyPrint (reify e) >>= putStr