copilot: A stream DSL for writing embedded C programs.

[ bsd3, embedded, language, library ] [ Propose Tags ]

This package is the main entry-point for using Copilot.

Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in Haskell that compiles into embedded C. Copilot contains an interpreter, multiple back-end compilers, and other verification tools. A tutorial, bug reports, and todos are available at https://github.com/Copilot-Language/copilot-discussion.

Examples are available at https://github.com/Copilot-Language/Copilot/tree/master/Examples.


[Skip to Readme]
Versions [faq] 0.21, 0.22, 0.23, 0.25, 0.26, 0.27, 0.28, 1.0, 1.0.1, 1.0.2, 2.0, 2.0.1, 2.0.2, 2.0.3, 2.0.4, 2.0.5, 2.0.6, 2.0.7, 2.0.8, 2.0.9, 2.1.0, 2.1.1, 2.1.2, 2.2.0, 2.2.1, 3.0, 3.0.1
Dependencies base (>=4.9 && <5), copilot-c99 (>=3.0.1 && <3.1), copilot-core (>=3.0.1 && <3.1), copilot-language (>=3.0.1 && <3.1), copilot-libraries (==3.0.*), copilot-theorem (==3.0.*), directory (==1.3.*), filepath (==1.4.*), optparse-applicative (==0.14.*) [details]
License BSD-3-Clause
Author Frank Dedden, Nis Nordby Wegmann, Lee Pike, Robin Morisset, Sebastian Niller, Alwyn Goodloe
Maintainer Frank Dedden <dev@dedden.net>
Category Language, Embedded
Home page https://copilot-language.github.io
Source repo head: git clone https://github.com/Copilot-Language/Copilot.git
Uploaded by frankdedden at Tue Apr 9 13:10:47 UTC 2019
Distributions NixOS:3.0.1
Downloads 12061 total (568 in the last 30 days)
Rating 2.0 (votes: 1) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs available [build log]
Last success reported on 2019-04-09 [all 1 reports]

Modules

[Index] [Quick Jump]

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for copilot-3.0.1

[back to package description]

Copilot: Stream DSL for hard real-time runtime verification

Build Status Version on Hackage

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

Installation

There are two ways to install Copilot:

  • From Hackage (recommended):

    The Copilot library is cabalized. Assuming you have cabal, the GHC compiler installed (the Haskell Platform is the easiest way to obtain these), and an Internet connection, it should merely be a matter of running:

    cabal install copilot
    
  • Building from source from the GitHub repositories (typically, one would only go this route to develop Copilot):

    git clone https://github.com/Copilot-Language/Copilot.git
    cd Copilot
    git submodule update --init --remote
    make
    

Note there is a TravisCI build (linked to at the top of this README) if you have trouble building/installing.

Example

Here follows a simple example of a heating system. Other examples can be found in the Examples directory 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"

Contributions

Feel free to open new issues and send pull requests.

In order to contribute to Copilot, please use the following steps which will make the process of evaluating and including your changes much easier:

  • Create an issue for every individual change or problem with Copilot. Document the issue well.

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

  • Every commit should mention one issue and, ideally, only one.

  • Do not send a PR or commit that addresses multiple problems, unless they are related and cannot be separated.

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

This process is similar to Git Flow. The equivalent of Git Flow's master branch is our latest tag, and the equivalent of Git Flow's develop branch is our master.

Further information

For further information, including documentation and a tutorial, please visit the Copilot website: https://copilot-language.github.io.

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.

License

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

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 (maintainer)
  • Robin Morisset
  • Levent ErkÅ‘k
  • Sebastian Niller
  • Nis Wegmann
  • Chris Hathhorn
  • Eli Mendelson
  • Jonathan Laurent
  • Laura Titolo
  • Georges-Axel Jolayan
  • Macallan Cruff
  • Ryan Spring
  • Lauren Pick
  • Frank Dedden (maintainer: contact at dev@dedden.net)
  • Ivan Perez