diff --git a/CHANGELOG b/CHANGELOG --- a/CHANGELOG +++ b/CHANGELOG @@ -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) diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,89 +1,162 @@ -# Copilot: Stream DSL for hard real-time runtime verification +
+# Copilot + [![Build Status](https://travis-ci.com/Copilot-Language/copilot.svg?branch=master)](https://app.travis-ci.com/github/Copilot-Language/copilot) [![Version on Hackage](https://img.shields.io/hackage/v/copilot.svg)](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: +
-* 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 +[(Back to top)](#table-of-contents) - ```bash - git clone https://github.com/Copilot-Language/copilot.git - cd copilot - ``` +## Linux installation +[(Back to top)](#table-of-contents) - 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 +[(Back to top)](#table-of-contents) + +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 +[(Back to top)](#table-of-contents) + +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 +[(Back to top)](#table-of-contents) + +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 +[(Back to top)](#table-of-contents) -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 `#` 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 +[(Back to top)](#table-of-contents) -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 +[(Back to top)](#table-of-contents) +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 +[(Back to top)](#table-of-contents) + +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 +[(Back to top)](#table-of-contents) + +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 +[(Back to top)](#table-of-contents) -## 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 +[(Back to top)](#table-of-contents) -## 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 +[(Back to top)](#table-of-contents) +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 +[(Back to top)](#table-of-contents) + +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. diff --git a/copilot.cabal b/copilot.cabal --- a/copilot.cabal +++ b/copilot.cabal @@ -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 diff --git a/src/Language/Copilot/Main.hs b/src/Language/Copilot/Main.hs --- a/src/Language/Copilot/Main.hs +++ b/src/Language/Copilot/Main.hs @@ -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