Skip to content
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

Drop pyk #2858

Merged
merged 6 commits into from
Sep 13, 2022
Merged

Drop pyk #2858

merged 6 commits into from
Sep 13, 2022

Conversation

tothtamas28
Copy link
Contributor

@tothtamas28 tothtamas28 commented Sep 7, 2022

@tothtamas28 tothtamas28 added the pyk Issues transferred from runtimeverification/pyk label Sep 7, 2022
@tothtamas28 tothtamas28 self-assigned this Sep 7, 2022
@tothtamas28 tothtamas28 force-pushed the pyk-remove branch 6 times, most recently from 06d3db3 to 7a8e3c4 Compare September 7, 2022 18:37
Jenkinsfile Outdated Show resolved Hide resolved
@radumereuta
Copy link
Contributor

lgtm, but I will give final approval when this is ready for review.

@dwightguth
Copy link
Collaborator

Sorry, if I understand this correctly, pyk isn't going to be packaged with kframework anymore? But then how are you going to make sure that the version of pyk that gets installed is compatible with the version of kframework that gets installed?

@tothtamas28
Copy link
Contributor Author

how are you going to make sure that the version of pyk that gets installed is compatible with the version of kframework that gets installed

pyk is tested on CI against a given version of K. When pyk is loaded, it could check the K version and emit a warning if there's a mismatch.

To have something more flexible though, my suggestion is to introduce semantic versioning for K so that any version with the same major version that is at least as recent is known to be compatible. And when there is a new feature in K we'd like to use, we simply bump the version we test and check against.

In practice, pyk will probably not break that often though: it would only break if K introduced a backward incompatible change in 1) the KAST JSON format 2) the KORE JSON format 3) its CLI. But those changes are relatively rare, so we decided to postpone the decision for adapting a versioning scheme until we see how things work out in practice.

@tothtamas28 tothtamas28 force-pushed the pyk-remove branch 2 times, most recently from 6139ad3 to eff55fb Compare September 12, 2022 12:32
@tothtamas28 tothtamas28 marked this pull request as ready for review September 12, 2022 13:28
@tothtamas28 tothtamas28 requested a review from a team as a code owner September 12, 2022 13:28
Copy link
Contributor

@radumereuta radumereuta left a comment

Choose a reason for hiding this comment

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

This should have at least 2 approvals.

@rv-jenkins rv-jenkins merged commit 1f61678 into master Sep 13, 2022
@rv-jenkins rv-jenkins deleted the pyk-remove branch September 13, 2022 10:17
h0nzZik pushed a commit to h0nzZik/k that referenced this pull request Nov 24, 2022
…untimeverification#2243)

* haskell-backend/src/main/native/haskell-backend: 36a8c0b3 - Update dependency: deps/k_release (runtimeverification#2858)

* haskell-backend/src/main/native/haskell-backend: f916e1ee - Convert SMT lemmas to old encoding (runtimeverification#2859)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
automerge pyk Issues transferred from runtimeverification/pyk
Projects
None yet
Development

Successfully merging this pull request may close these issues.

6 participants