copilot-theorem: Extend range of versions of kind2

Description

In order to keep Copilot effectively working in the current software ecosystem, we need to extend the versions of dependencies that Copilot can be installed with. kind2 has seen release 2.3.0, but copilot-theorem requires kind2 0.7.2.

Type

Management: update versions of dependencies.

Additional context

None.

Requester

Ivan Perez.

Method to check presence of bug

Not applicable (not a bug).

Expected result

Copilot can be installed with a modern version of kind2.

Desired result

Copilot can be installed with a modern version of kind2.

Proposed solution

Modify translation of Copilot to kind2's syntax in copilot-theorem to comply with the requirements of a modern version of kind2, and, if applicable, parsing of the results produced by kind2.

Further notes

None.

Change Manager: Confirmed that the issue exists.

Technical Lead: Confirmed that the issue should be addressed.

@chathhorn-galois

Technical Lead: Issue scheduled for fixing in Copilot 4.7.2.

Fix assigned to: @chathhorn-galois .

copilot-theorem: support for Kind2 2.x. Refs Copilot-Language#734.

copilot-theorem: tests for the Kind2 backend. Refs Copilot-Language#734.

copilot-theorem: Extend range of versions of Kind2. Refs Copilot-Lang…

copilot-theorem: Tests for the Kind2 backend. Refs Copilot-Language#734.

copilot-theorem: Update README for Kind2 backend changes. Refs Copilo…

copilot-theorem: Document changes in CHANGELOG. Refs Copilot-Language…

@ivanperez-keera

Change Manager: The issue is being re-assigned due to the original author being unavailable and changes being needed.

Issue assigned to: @ivanperez-keera in addition to the original author.

copilot-theorem: Extend range of versions of Kind2. Refs Copilot-Lang…

copilot-theorem: Update README for Kind2 backend changes. Refs Copilo…

copilot-theorem: Document changes in CHANGELOG. Refs Copilot-Language…

Change Manager: Verified that:

Solution is implemented:

The code proposed compiles and passes all tests. Details:
Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/278451863

The solution proposed produces the expected result. Details:
The following Dockerfile checks that copilot-theorem works with kind2 version 2.3.0 by using both to evaluate a specification and comparing the results from Kind2 to the expectation for the specific spec, after which it prints the message "Success":

--- Dockerfile-verify-734
FROM ubuntu:focal

# Avoid interactive prompts during package installation
ENV DEBIAN_FRONTEND=noninteractive

# Install system dependencies and build tools
RUN apt-get update && apt-get install -y --no-install-recommends \
    alex \
    build-essential \
    ca-certificates \
    curl \
    git \
    git \
    happy \
    libgmp-dev \
    libz-dev \
    m4 \
    pkg-config \
    software-properties-common \
    unzip \
    wget \
    z3 \
    && rm -rf /var/lib/apt/lists/*

WORKDIR /root

# Install kind2
RUN wget -L https://github.com/kind2-mc/kind2/releases/download/v2.3.0/kind2-v2.3.0-linux-x86_64.tar.gz -O kind2-v2.3.0-linux-x86_64.tar.gz
RUN tar -zxvpf kind2-v2.3.0-linux-x86_64.tar.gz && rm kind2-v2.3.0-linux-x86_64.tar.gz
RUN mv kind2 /usr/local/bin
RUN chmod a+x /usr/local/bin/kind2

# Install GHC
RUN add-apt-repository ppa:hvr/ghc
RUN apt-get update
RUN apt-get install --yes ghc-8.6.5 cabal-install-2.4

ENV PATH=/opt/ghc/8.6.5/bin:/opt/cabal/2.4/bin:$PWD/.cabal-sandbox/bin:$PATH

# Install Copilot
RUN cabal update
RUN cabal v1-sandbox init

ARG REPO=https://github.com/copilot-language/copilot
ARG GIT_COMMIT=master

RUN git clone ${REPO} copilot
RUN cd copilot && git checkout ${GIT_COMMIT}

RUN cabal v1-install \
       copilot/copilot \
       copilot/copilot-c99 \
       copilot/copilot-core \
       copilot/copilot-interpreter \
       copilot/copilot-language \
       copilot/copilot-libraries \
       copilot/copilot-prettyprinter \
       copilot/copilot-theorem

ADD Spec.hs /tmp
RUN cabal v1-exec -- runhaskell /tmp/Spec.hs | grep -e "t1: proof failed" -e "t2: proof checked successfully"
RUN echo "Success"

--- Spec.hs
import Data.Functor
import Prelude hiding ((++))

import Copilot.Theorem.Kind2
import Copilot.Theorem.Prove
import Language.Copilot

trueThenFalses :: Stream Bool
trueThenFalses = [True] ++ constant False

spec :: Spec
spec = do
  void $ theorem "t1" (forAll trueThenFalses) (check (kind2Prover def))
  void $ theorem "t2" (exists trueThenFalses) (check (kind2Prover def))

main :: IO ()
main = void $ reify spec

Command (substitute variables based on new path after merge):

$ docker build --build-arg REPO=https://github.com/ivanperez-keera/copilot --build-arg GIT_COMMIT=b8ff2fbaa16abac1441d172fa557e727d4380e66  -t kind2 -f Dockerfile-verify-734 .

Implementation is documented. Details:
The code includes comments and the README is updated.
Change history is clear.
Commit messages are clear.
Changelogs are updated.
Examples are updated. Details:
No updates needed; the change does not affect the existing API.
Required version bumps are evaluated. Details:
Bump required; the code alter the existing API and removes public elements.

Change Manager: Implementation ready to be merged.

Merge branch 'develop-update-kind2'. Close Copilot-Language#734.

Navigation Menu

Repository navigation

`copilot-theorem`: Extend range of versions of kind2 #734

24 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

copilot-theorem: Extend range of versions of kind2 #734

Description

Activity

ivanperez-keera commented on May 25, 2026

ivanperez-keera commented on May 25, 2026

ivanperez-keera commented on May 25, 2026

24 remaining items

ivanperez-keera commented on Jul 8, 2026

ivanperez-keera commented on Jul 8, 2026

ivanperez-keera commented on Jul 8, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

`copilot-theorem`: Extend range of versions of kind2 #734