Skip to content

Remove CVC5 binary#198

Open
mugdhadhole1 wants to merge 2 commits into
mainfrom
internal/remove-cvc5-binary
Open

Remove CVC5 binary#198
mugdhadhole1 wants to merge 2 commits into
mainfrom
internal/remove-cvc5-binary

Conversation

@mugdhadhole1

@mugdhadhole1 mugdhadhole1 commented Jun 15, 2026

Copy link
Copy Markdown
Contributor

Remove CVC5 binary

@mugdhadhole1 mugdhadhole1 requested a review from a team as a code owner June 15, 2026 12:11
@mugdhadhole1 mugdhadhole1 added the internal Affects the CI, tests or refactorings only, not relevant to the end-user label Jun 15, 2026
phiwuu
phiwuu requested changes Jun 15, 2026
View reviewed changes

@phiwuu phiwuu left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

please update CHANGELOG.md

Comment thread .github/workflows/ci.yml
Comment on lines -36 to -37
- os: windows-2022
cvc5-plat: "windows"

@phiwuu phiwuu Jun 15, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

please keep windows-2022, and remove only cvc5-plat

Comment thread documentation/TUTORIAL-LINT.md Outdated
@@ -109,7 +102,6 @@ Verified 1 model(s) and 0 check(s) and found no issues
Please keep in mind two limitations with the `--verify`

@phiwuu phiwuu Jun 15, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
Please keep in mind two limitations with the `--verify`
Please keep in mind the following limitation with the `--verify`

and remove the bullet point, but just make it a sentence.

@SurajBDeore

SurajBDeore commented Jun 19, 2026

Copy link
Copy Markdown

Do we need to update the changelog?

SurajBDeore
SurajBDeore reviewed Jun 19, 2026
View reviewed changes
Comment thread trlc/trlc.py
@@ -77,14 +76,12 @@ def __init__(self, mh,
parse_trlc = True,

@SurajBDeore SurajBDeore Jun 19, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please remove import statement on line no 36
import cvc5

@mugdhadhole1 mugdhadhole1 Jun 19, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It imports the cvc5 Python library, not the cvc5 binary.
So this in trlc.py: 36 is checking whether the Python package cvc5 is installed.

@SurajBDeore

SurajBDeore commented Jun 19, 2026

Copy link
Copy Markdown

These two docs currently tell slightly different stories about where CVC5 works.

In [TUTORIAL-CI.md:46], it says CVC5 is GNU/Linux only.
In [README.md:65], it just says CVC5 is required for verify, without that Linux-only note.
So readers can get confused.

@mugdhadhole1 mugdhadhole1 force-pushed the internal/remove-cvc5-binary branch from 967179c to aa4efa3 Compare June 19, 2026 08:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@SurajBDeore SurajBDeore SurajBDeore left review comments

@phiwuu phiwuu phiwuu requested changes

Requested changes must be addressed to merge this pull request.

Assignees

No one assigned

Labels

internal Affects the CI, tests or refactorings only, not relevant to the end-user

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@mugdhadhole1 @SurajBDeore @phiwuu