Skip to content

Remove unused private attribute from KProve #4811

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
May 12, 2025

Conversation

tothtamas28
Copy link
Contributor

@tothtamas28 tothtamas28 commented May 12, 2025

Eliminates a (package level) circularity between pyk.kcfg and pyk.ktool.

@tothtamas28 tothtamas28 self-assigned this May 12, 2025
@tothtamas28
Copy link
Contributor Author

pydeps -o k.png -T png --no-show --cluster --max-bacon 2 --max-module-depth 2 pyk/src/pyk

Before:
before

After:
after

Base automatically changed from move-prove-rpc to develop May 12, 2025 18:03
This eliminates a (package level) circularity between `kcfg` and
`ktool`.
@tothtamas28 tothtamas28 force-pushed the remove-circular-attr branch from 63b82b0 to 2c98f55 Compare May 12, 2025 18:07
@tothtamas28 tothtamas28 marked this pull request as ready for review May 12, 2025 18:08
@tothtamas28 tothtamas28 requested a review from ehildenb May 12, 2025 18:08
@ehildenb
Copy link
Member

ehildenb commented May 12, 2025

I find it weird that ktool is included into kcfg, but I guess that's because KCFGExplore uses ktool. I'd like to have kcfg be a bit more "pure" of a datastructure, so maybe we move the explore.py and exploration.py modules into proof instead, since that's really where they are used.

We have some other work to remove the use of KPrint from kcfg class too: #4808

@automergerpr-permission-manager automergerpr-permission-manager bot merged commit 3ca88f2 into develop May 12, 2025
18 checks passed
@automergerpr-permission-manager automergerpr-permission-manager bot deleted the remove-circular-attr branch May 12, 2025 21:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants