copilot

<div align="center">

# Copilot

[![Build Status](https://github.com/Copilot-Language/copilot/actions/workflows/build.yml/badge.svg?branch=master)](https://github.com/Copilot-Language/copilot/actions/workflows/build.yml)
[![Version on Hackage](https://img.shields.io/hackage/v/copilot.svg)](https://hackage.haskell.org/package/copilot)

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 into 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)

</div>

## Features

- Write simple, high-level specifications using a stream-based language.

- Produce hard real-time C99 runtime monitors that run in constant memory and time.

- Catch errors in specifications early using an expressive static type system.

- Prove properties about specifications using theorem proving extensions.

- Interpret specifications for testing and debugging purposes.

- Obtain proofs of correctness of the generated code.

## Table of Contents

- [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)

# Installation
<sup>[(Back to top)](#table-of-contents)</sup>

## Linux installation
<sup>[(Back to top)](#table-of-contents)</sup>

### Debian Bookworm / Ubuntu 23.04

On Debian Bookworm / Ubuntu 23.04 or newer, Copilot can be installed directly
from the package repositories with:

```sh
$ sudo apt-get install libghc-copilot-dev
```

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

### Fedora 40

On Fedora 40 or newer, Copilot can be installed directly from the package
repositories with:

```sh
$ sudo dnf install ghc-copilot-devel
```

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

### Other Linux distributions

On other Linux distributions or older Debian-based distributions, to use
Copilot, you must install a Haskell compiler (GHC) and the pac