Skip to content
This repository has been archived by the owner on Apr 25, 2024. It is now read-only.

Fix circular import #925

Merged
merged 9 commits into from
Feb 27, 2024
Merged

Fix circular import #925

merged 9 commits into from
Feb 27, 2024

Conversation

nwatson22
Copy link
Contributor

@nwatson22 nwatson22 commented Feb 27, 2024

#915 introduced a circular import crash which is triggered when executing pyk rpc-kast rpc.py > kprove.py > cterm > symbolic.py > rpc.py

Moves KoreExecLogFormat to kore/rpc.py

@nwatson22 nwatson22 self-assigned this Feb 27, 2024
src/pyk/cterm/__init__.py Outdated Show resolved Hide resolved
devops and others added 6 commits February 27, 2024 18:45
This PR introduces the following changes:
* Refactors `remove_useless_constraints` to take a list of constraints
rather than a `CTerm`, and reimplements the original version as a
method of `CTerm`.
* Use the new `remove_useless_constraints` to restrict the constraints
used to build a refutation proof to only those that have a dependency on
the most recent branch.
* Add a test that the refutation proof omits independent constraints.

---------

Co-authored-by: devops <devops@runtimeverification.com>
@nwatson22 nwatson22 marked this pull request as ready for review February 27, 2024 19:34
@rv-jenkins rv-jenkins merged commit a71358f into master Feb 27, 2024
11 checks passed
@rv-jenkins rv-jenkins deleted the noah/imports-fix branch February 27, 2024 19:43
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 9, 2024
#915 introduced a circular import crash which is triggered when
executing `pyk rpc-kast` `rpc.py > kprove.py > cterm > symbolic.py >
rpc.py`

Moves `KoreExecLogFormat` to `kore/rpc.py`

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: lucasmt <36549752+lucasmt@users.noreply.github.com>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 9, 2024
#915 introduced a circular import crash which is triggered when
executing `pyk rpc-kast` `rpc.py > kprove.py > cterm > symbolic.py >
rpc.py`

Moves `KoreExecLogFormat` to `kore/rpc.py`

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: lucasmt <36549752+lucasmt@users.noreply.github.com>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 10, 2024
#915 introduced a circular import crash which is triggered when
executing `pyk rpc-kast` `rpc.py > kprove.py > cterm > symbolic.py >
rpc.py`

Moves `KoreExecLogFormat` to `kore/rpc.py`

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: lucasmt <36549752+lucasmt@users.noreply.github.com>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 10, 2024
#915 introduced a circular import crash which is triggered when
executing `pyk rpc-kast` `rpc.py > kprove.py > cterm > symbolic.py >
rpc.py`

Moves `KoreExecLogFormat` to `kore/rpc.py`

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: lucasmt <36549752+lucasmt@users.noreply.github.com>
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants