copilot

copilot copied to clipboard

**Description** The cabal file of `copilot-c99` specifies a compiler flag `--no-deprecations` that is no longer necessary. It should have been removed when modules were hidden, but the flag was left...

ivanperez-keera

`copilot-c99`: `array has incomplete element type` error when declaring stream with array of structs

22

I write a Copilot spec involving a stream of structs: ```hs -- Struct1.hs {-# LANGUAGE DataKinds #-} module Main where import qualified Prelude as P import Control.Monad (void, forM_) import...

RyanGlScott

`copilot-c99`: Can C99 generator declare stream functions as static?

11

C code output by Copilot declares variables static but functions global; e.g.: ``` static size_t s3_idx = (0); float s0_get(size_t x) { return (s0)[((s0_idx) + (x)) % (1)]; } ```...

simondlevy

`copilot-theorem`: README mentions inexisting `Driver.hs`, `lightProver`

6

**Description** `copilot-theorem`'s README mentions a file `Driver.hs` that is not part of the library: ``` As an example, the following prover is used in Driver.hs: ``` and later ``` Some...

ivanperez-keera

`copilot-theorem`: `kind2Prover` gives parse error when disproving a property

8

(In order to reproduce this bug, you'll need to install [Kind2-0.7.2](https://github.com/kind2-mc/kind2/releases/tag/v0.7.2), which is (as far as I can tell) the latest version of Kind2 that `copilot-theorem` currently supports. Note that...

RyanGlScott

Finite State Machines in Copilot

18

Is Copilot suitable for implementing Finite State Machines?

liamdiprose

**Description** The record field `uTypeType`, part of `Copilot.Core.Type.UType`, is never really used within the module or in any other part of Copilot or, as far as we know, by any...

ivanperez-keera

We now have a process that will allow us to accept contributions from external users again. The process should be described in the README, and the current notice stating that...

ivanperez-keera

In Kind2-0.7.2, disproven properties are tagged with `falsifiable` in the XML output, but the code in `copilot-theorem`'s Kind2 backend was instead searching for a tag named `invalid`. As a result,...

RyanGlScott

`copilot-theorem`: Extend range of versions `what4` to include 1.6

1

**Description** `what4` has seen a new release 1.6, but `copilot-theorem` needs versions strictly lower than 1.6. This version is API-compatible for all features used by `copilot-theorem`, but it includes support...

ivanperez-keera