copilot-verifier: Include in mainline

Description

The copilot-verifier was developed outside of this repo, but there's interest in having all Copilot projects and libraries merged into a main repo for ease of management.

Type

Management: files need to be moved between repos.

Additional context

None.

Requester

Ivan Perez.

Method to check presence of bug

Not applicable (not a bug).

Expected result

The last state of the copilot-verifier is included in this repository, disregarding history, and adjusting the changelog to make the old
issues refer to copilot-verifier#<ISSUE_NUM> so that they are not interpreted as related to the main Copilot repo.

Desired result

The last state of the copilot-verifier is included in this repository, disregarding history, and adjusting the changelog to make the old
issues refer to copilot-verifier#<ISSUE_NUM> so that they are not interpreted as related to the main Copilot repo.

Proposed solution

Copy last state of copilot-verifier as subdirectory of main repo.

Adjust Changelog in copilot-verifier to make older issues point to correct repo.

Further notes

None.

I briefly looked into this, and I have some questions about how to handle certain aspects of the copilot-verifier repo:

Should I list myself as the maintainer in copilot-verifier.cabal, or should I list you (as is done for other copilot subpackages)?
Do we still want to include the Dockerfile from the copilot-verifier repo?
There are a variety of examples under the copilot-verifier/examples subdirectory. Should I try to move these examples to copilot/examples (where the bulk of the Copilot examples are currently stored), or should I keep this examples within the copilot-verifier subdirectory?

Change Manager: Confirmed that the issue exists.

Technical Lead: Confirmed that the issue should be addressed.

@RyanGlScott

Technical Lead: Issue scheduled for fixing in Copilot 4.5.

Fix assigned to: @RyanGlScott .

@RyanGlScott

@RyanGlScott Just copy it as is, and we can make the changes later (separately).

Include the example and the Dockerfile where they are and under the copilot-verifier directory.

copilot-verifier: Adjust issue numbers in changelog. Refs Copilot-Lan…

copilot-verifier: Document changes in CHANGELOG. Refs Copilot-Languag…

Explicitly list .cabal files in cabal.project. Refs Copilot-Language#622

copilot-verifier: Include in mainline copilot repo. Refs Copilot-Lang…

copilot-verifier: Adjust issue numbers in changelog. Refs Copilot-Lan…

copilot-verifier: Document changes in CHANGELOG. Refs Copilot-Languag…

Implementor: Solution implemented, review requested.

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/275542308

The solution proposed produces the expected result. Details:
The following dockerfile checks out the latest version of copilot-verifier, v4.4, and compares it against the version being merged, ignoring differences in the CHANGELOG (which is expected to be different), checking that there are no other differences, after which it prints the message "Success":

FROM ubuntu:noble

ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update

RUN apt-get install --yes git
RUN git config --global advice.detachedHead false

CMD git clone $REPO $NAME \
    && cd $NAME \
    && git checkout $COMMIT \
    && cd .. \
    && git clone -b v4.4 https://github.com/Copilot-Language/copilot-verifier copilot-verifier-original \
    && diff --exclude 'CHANGELOG' -r $NAME/copilot-verifier copilot-verifier-original/copilot-verifier \
    && echo "Success"

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

$ docker run -e REPO=https://github.com/GaloisInc/copilot-1 -e NAME=copilot -e COMMIT=9e0dcac323f523277b1bdcb74869d823b6ad5324 copilot-verify-622

Implementation is documented. Details:
CHANGELOG updated to make old issues point to original repo. No other changes needed.
Change history is clear.
Commit messages are clear.
Changelogs are updated.
Examples are updated. Details:
No updates needed.
Required version bumps are evaluated. Details:
Bump not needed; change includes existing package without affecting API.

Change Manager: Implementation ready to be merged.

Merge branch 'develop-copilot-verifier-upstream'. Close Copilot-Langu…

Navigation Menu

Repository navigation

`copilot-verifier`: Include in mainline #622

1 remaining item

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

copilot-verifier: Include in mainline #622

Description

Activity

RyanGlScott commented on May 16, 2025

ivanperez-keera commented on May 17, 2025

ivanperez-keera commented on May 17, 2025

ivanperez-keera commented on May 17, 2025

ivanperez-keera commented on May 17, 2025

1 remaining item

RyanGlScott commented on Jun 20, 2025

ivanperez-keera commented on Jun 21, 2025

ivanperez-keera commented on Jun 21, 2025

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

`copilot-verifier`: Include in mainline #622